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.