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”

Pingback: An exact formula for satisfiability « Marco Benini

Enter your comment here...

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

Email (required) (Address never made public)

Name (required)

Website

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

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

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

Cancel

Connecting to %s

Marco Benini

A quick satisfiability check

One comment on “A quick satisfiability check”

Leave a Reply

Information

Shortlink

Navigation

Marco Benini

A quick satisfiability check

Rate this:

Like this:

Related

One comment on “A quick satisfiability check”

Leave a Reply

Information

Shortlink

Navigation