> 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

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