Marco Benini

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.

One comment on “A quick satisfiability check

  1. Pingback: An exact formula for satisfiability « Marco Benini

Leave a Reply

Please log in using one of these methods to post your comment: Logo

You are commenting using your account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s


This entry was posted on April 1, 2011 by in Computer Science, Mathematics, Theoretical Computer Science.
%d bloggers like this: