Marco Benini

An exact formula for satisfiability

Let \phi = \bigwedge_{i = 1}^m \bigvee_{j = 1}^n l_{i,j} be an instance of SAT. As in a previous post, let c_i denote the i-th clause. Moreover, let F(c_i) = \{ \sigma \colon \{ x_1, \dots, x_n\} \to \{ \top, \bot \} \colon \sigma( \bigvee_{j = 1}^n l_{i,j} ) = \bot \}. We know that |F(c_i)| = 2^{n - |c_i|}.

Evidently, \bigcup_{i = 1}^m F(c_i) is the set of assignments falsifying \phi. But, by the Inclusion-Exclusion principle, \left| \bigcup_{i = 1}^m F(c_i)\right| = \sum_{i = 1}^m (-1)^{i - 1} \sum_{I \subseteq \{1,\dots,n\}, |I| = j} \left| \bigcap_{j \in I} F(c_j)\right|.

Since \phi is satisfiable if and only if \left|\bigcup_{i = 1}^m F(c_i)\right| < 2^n, considering \phi as the set of its clauses, easy calculations will lead to

Theorem: The formula \phi is satisfiable if and only if \sum_{I \subseteq \phi} (-1)^{|I|} \left| \bigcap_{c \in I} F(c) \right| > 0.

One comment on “An exact formula for satisfiability”

  1. Pingback: A quick satisfiability check « Marco Benini

Leave a Reply

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

Gravatar
WordPress.com Logo

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

Google+ photo

You are commenting using your Google+ 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 )

Cancel

Connecting to %s

Information

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

Shortlink

https://wp.me/p1rYpC-27

Navigation

Categories

Powered by WordPress.com.

%d bloggers like this: