A Million Clauses, or Sixty-One

Resolution has one inference rule and it needs its input in conjunctive normal form: a conjunction of disjunctions of literals. Every propositional formula has a CNF equivalent, which is usually stated as though it settled the matter.

Here is a formula that makes the difference between "has one" and "you can afford it".

$$\varphi \;=\; (x_1 \wedge y_1) \vee (x_2 \wedge y_2) \vee \dots \vee (x_{20} \wedge y_{20}).$$

Twenty conjunctions, forty variables, one line.

A. Distributing

The textbook conversion distributes $\vee$ over $\wedge$. Each of the twenty disjuncts contributes either its $x$ or its $y$ to each clause, independently, so the result has one clause per choice:

$$2^{20} = 1{,}048{,}576 \text{ clauses},$$

each twenty literals long: 20,971,520 literals in total. For thirty disjuncts it is 1,073,741,824 clauses. The conversion is correct, terminating, and useless.

B. Naming the subformulas

The alternative is to give each conjunction a name. Introduce $t_i$ and assert $t_i \leftrightarrow (x_i \wedge y_i)$, which is three clauses:

$$(\neg t_i \vee x_i), \qquad (\neg t_i \vee y_i), \qquad (t_i \vee \neg x_i \vee \neg y_i),$$

and then say that at least one of them holds: $(t_1 \vee \dots \vee t_{20})$.

That is $3 \times 20 + 1 = \mathbf{61}$ clauses and 160 literals, against 20,971,520. A factor of 131,072 in literals, from a rewriting rule rather than from a better solver. This is the Tseitin transformation, and it is what every SAT solver's front end does.

C. What it costs

The usual summary is that the result is equisatisfiable rather than equivalent, which sounds like a concession. It is worth being precise about how small the concession is.

The new formula has twenty extra variables, so it is a formula about a different vocabulary and cannot be equivalent to $\varphi$ in the strict sense. But each $t_i$ is forced: the three clauses pin it to the truth value of $x_i \wedge y_i$, with no freedom left. Every model of $\varphi$ therefore extends to exactly one model of the encoding, and counting them confirms it:

Checked by enumerating every assignment, $2^{2n}$ of them for $\varphi$ and $2^{3n}$ for the encoding. Satisfiability is preserved, the solutions are preserved, and even the model count is preserved. What is not preserved is the variable list, and the price of that is a projection step at the end.

D. The rule itself

Resolution takes two clauses containing a complementary pair and produces their resolvent:

$$\frac{(\alpha \vee \ell) \qquad (\beta \vee \neg \ell)}{(\alpha \vee \beta)}.$$

It is not complete for deriving arbitrary consequences - from $P$ it will never derive $P \vee Q$, which is entailed - but it is refutation-complete: if a set of clauses is unsatisfiable, repeated resolution derives the empty clause. That is enough, because $\text{KB} \models \alpha$ exactly when $\text{KB} \wedge \neg\alpha$ is unsatisfiable.

On the clauses $\{P \vee Q,\; \neg P \vee R,\; \neg Q \vee R,\; \neg R\}$ a four-step refutation exists:

1. $\neg R$ with $\neg P \vee R$ gives $\neg P$
2. $\neg R$ with $\neg Q \vee R$ gives $\neg Q$
3. $P \vee Q$ with $\neg P$ gives $Q$
4. $Q$ with $\neg Q$ gives the empty clause.

Saturating blindly instead - resolving every pair until nothing new appears - derives 8 new clauses and reaches a closure of 12 before it gets there. On four clauses the difference is nothing. It is the same difference that separates a modern conflict-driven solver from the algorithm as written in a textbook, and at scale it is everything.

The figure runs the same rule on a different knowledge base, the Wumpus breeze rule $B_{1,1} \Leftrightarrow (P_{1,2} \vee P_{2,1})$ with $\neg B_{1,1}$: four clauses plus the negated query, and every answer is checked against the eight possible worlds.

E. What to take from it

• The translation is part of the algorithm. A problem that is impossible after distributing and routine after Tseitin was never a hard problem; it was a badly encoded one.
• Count literals, not clauses. The distributed form above is bad in both, but encodings that look comparable by clause count often differ by an order of magnitude in literals, which is what propagation actually walks.
• "There exists a CNF equivalent" is a statement about existence. So is "every problem in NP reduces to SAT". Both are true, and neither says anything about the size of what you get.