As it is well-known, Boolean Satisfiability, SAT for short, is NP-complete.
Suppose is a formula where is a literal, i.e., the variable , or , or (when the variable does not occur in the -th clause).
Proposition: Let and let . If then is satisfiable.
proof: Evidently, the total number of possible assignments is . Also, the total number of assignments falsifying is less or equal than the number of assignments falsifying each clause of .
But the number of assignments falsifying is easily calculated as , since an assignment must falsify every occurrence of a variable in .
So, from we get , that is, the number of assignments falsifying each clause of is strictly less than the total number of assignments. Thus, there must be an assignment which does not falsify .
Checking the sum of the previous proposition is very efficient: it is linear in the size of !
Notice that the proposition is NOT an equivalence: if the sum is 1 or greater, we don’t know whether is satisfiable. It is possible to extend the proposition so to make it an equivalence, as I’ll do in another post: in this case the calculation will be exponential in the size of .