> 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.
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.