Saturday, June 30, 2012

Minimal unsatisfiable 3-SAT example

The 3-SAT problem defined here is a stricter version than elsewhere, in the sense that each clause must contain exactly three literals. Some versions permit 1 or 2 literals.

To obtain a minimal unsatisfiable 3-SAT example, we start with a two-clause contradiction representing \( u_1 \wedge \neg u_1 \) as the base case. This base case is not 3-SAT. We then grow the clause as follows: suppose \( C_{i-1} \) containing \( i-1 \) variables is unsatisfiable, then let \( C_i = \left\{ c \vee u_i, c \vee \neg u_i \mid c \in C_{i-1} \right\} \), and \( C_i \) is also unsatisfiable.

To carry out the algorithm, we start with the base case.
  • \( u_1 \)
  • \( \neg u_1 \)
Then we add another variable to each clause:
  • For \( u_1 \):
    • \( u_1 \vee u_2 \)
    • \( u_1 \vee \neg u_2 \)
  • For \( \neg u_1 \):
    • \( \neg u_1 \vee u_2 \)
    • \( \neg u_1 \vee \neg u_2 \)
Then we add another variable to each clause:
  • For \( u_1 \vee u_2 \)
    • \( u_1 \vee u_2 \vee u_3 \)
    • \( u_1 \vee u_2 \vee \neg u_3 \)
  • For \( u_1 \vee \neg u_2 \)
    • \( u_1 \vee \neg u_2 \vee u_3 \)
    • \( u_1 \vee \neg u_2 \vee \neg u_3 \)
  • For  \( \neg u_1 \vee u_2 \)
    • \( \neg u_1 \vee u_2 \vee u_3 \)
    • \( \neg u_1 \vee u_2 \vee \neg u_3 \)
  • For \( \neg u_1 \vee \neg u_2 \)
    • \( \neg u_1 \vee \neg u_2 \vee u_3 \)
    • \( \neg u_1 \vee \neg u_2 \vee \neg u_3 \)
And here we have an unsatisfiable 3SAT example with 3 variables and 8 clauses.


Unknown said...

Actually you can repeat the same varyable multiple times in each clause. So the shortest one is (x|x|x)&(!x|!x|!x).

Likai Liu said...

It depends on how you define your 3-SAT problem. I didn't state the formal definition I was using. It comes from Computers and Intractability—A Guide to the Theory of NP-Completeness by Garey and Johnson, which uses set to express the clauses. As a set, \( \{a, a\} \) = \( \{a\} \), so if you repeat a variable, it would no longer be 3-SAT by this definition.

Anonymous said...

Thanks! I like working with my hands on simple examples, but I was having a hard time coming up with simple examples of unsatisfiable 3-SAT problems.