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.
Post a Comment