# A quick satisfiability check

As it is well-known, Boolean Satisfiability, SAT for short, is NP-complete.

Suppose $\phi = \bigwedge_{i = 1}^m\bigvee_{j = 1}^n l_{i,j}$ is a formula where $l_{i,j}$ is a literal, i.e., the variable $x_j$, or $\neg x_j$, or $\bot$ (when the variable does not occur in the $i$-th clause).

Proposition: Let $\phi = \bigwedge_{i = 1}^m\bigvee_{j = 1}^n l_{i,j}$ and let $c_i = \{ l_{i,j} \colon 1 \leq j \leq n, l_{i,j} \not= \bot\}$. If $\sum_{i = 1}^m (1/2)^{|c_i|} < 1$ then $\phi$ is satisfiable.

proof: Evidently, the total number of possible assignments $\sigma \colon \{x_1, \dots, d_n \} \to \{ \top, \bot \}$ is $2^n$. Also, the total number of assignments falsifying $\phi$ is less or equal than the number of assignments falsifying each clause $c_i$ of $\phi$.

But the number of assignments falsifying $c_i$ is easily calculated as $2^{n - |c_i|}$, since an assignment must falsify every occurrence of a variable in $c_i$.

So, from $\sum_{i = 1}^m (1/2)^{|c_i|} < 1$ we get $\sum_{i = 1}^m 2^{n - |c_i|} < 2^n$, that is, the number of assignments falsifying each clause $c_i$ of $\phi$ is strictly less than the total number of assignments. Thus, there must be an assignment which does not falsify $\phi$. $\Box$

Checking the sum of the previous proposition is very efficient: it is linear in the size of $\phi$!

Notice that the proposition is NOT an equivalence: if the sum is 1 or greater, we don’t know whether $\phi$ 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 $\phi$.

### Information

This entry was posted on April 1, 2011 by in Computer Science, Mathematics, Theoretical Computer Science.