> he standard representation of such a formula is the conjunctive normal form, or simply: AND-of-ORs. Our previous example would look like this when transformed:
A and B and (A or B) and (!A or !B)
There is another normal form, the disjunctive normal form. This is in the form of An OR of ANDs. Interestingly, every formula can be represented in this form. And SAT is rather easy to determine for this form.
The catch is that taking a logical formula, and placing it in Disjunctive normal form is actually a rather arduous, non polynomial process.
> And SAT is rather easy to determine for this form.
Gave me a chuckle, as that's quite an understatement, as the decision procedure is only: is there a single clause and is it just "False"?
> The catch is that taking a logical formula, and placing it in Disjunctive normal form is actually a rather arduous, non polynomial process.
Basically writing out all assignments that make the formula true. Potentially exponentially many, as there are 2^n possible assignments of n variables. So this transformation is basically just solving and writing down all models.
The conjunctive normal form can be exponentially large in the worst case as well, though, see the footnote in the article. In practice that is not a problem, since it suffices to find a formula in CNF that is satisfiable precisely when the original formula is satisfiable, even though it might not be equivalent.
The catch is that taking a logical formula, and placing it in Disjunctive normal form is actually a rather arduous, non polynomial process.