# A quick satisfiability check

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 .

### Like this:

Like Loading...

*Related*

Pingback: An exact formula for satisfiability « Marco Benini