94 Complexity — SAT To3 SAT
94.1 Overview
This module formalises the classical polynomial-time reduction from SAT to 3-SAT via a chain (Tseitin-style) encoding. Given a CNF formula \(f\) over variables \(V\), the function SATTo3SAT.to3SAT produces an equisatisfiable 3-CNF formula over an extended variable type SATTo3SAT.AuxVar \(V\); the main result SATTo3SAT.SAT_to_3SAT_equivalence states that \(f\) is satisfiable if and only if its 3-CNF encoding is satisfiable.
94.2 Declarations
A clause over variable type \(V\) is a disjunction represented as a list of literals, i.e. \(\mathtt{Clause}\, V = \mathtt{List}\, (\mathtt{Literal}\, V)\).
A CNF formula over \(V\) is a conjunction of clauses, represented as a list of clauses: \(\mathtt{CNFFormula}\, V = \mathtt{List}\, (\mathtt{Clause}\, V)\).
Given an assignment \(\alpha : V \to \mathrm{Prop}\), SATTo3SAT.evalLiteral maps a literal to its truth value: a positive literal \(\mathtt{pos}\, v\) is true iff \(\alpha (v)\) holds, and a negative literal \(\mathtt{neg}\, v\) is true iff \(\alpha (v)\) does not hold.
A clause \(c\) is satisfied by assignment \(\alpha \) if at least one literal in \(c\) evaluates to true under \(\alpha \), i.e. \(\exists \, l \in c,\; \texttt{SATTo3SAT.evalLiteral}\, \alpha \, l\).
A CNF formula \(f\) is satisfied by assignment \(\alpha \) if every clause in \(f\) is satisfied by \(\alpha \).
A CNF formula \(f\) is satisfiable if there exists an assignment \(\alpha \) such that \(\texttt{SATTo3SAT.formulaSatisfied}\, \alpha \, f\) holds.
A 3-clause over \(V\) is a structure carrying exactly three literals \(l_1, l_2, l_3 : \mathtt{Literal}\, V\); a 3-clause is satisfied when at least one of the three literals is true.
A 3-CNF formula over \(V\) is a list of 3-clauses: \(\mathtt{Formula3}\, V = \mathtt{List}\, (\mathtt{Clause3}\, V)\).
A 3-clause \(c\) is satisfied by assignment \(\alpha \) if at least one of its three literals \(c.l_1\), \(c.l_2\), \(c.l_3\) evaluates to true under \(\alpha \).
A 3-CNF formula \(f\) is satisfied by assignment \(\alpha \) if every 3-clause in \(f\) is satisfied by \(\alpha \).
A 3-CNF formula \(f\) is 3-satisfiable if there exists an assignment \(\alpha \) such that \(\texttt{SATTo3SAT.formula3Satisfied}\, \alpha \, f\) holds.
The inductive type \(\mathtt{AuxVar}\, V\) extends a variable type \(V\) with two constructors: \(\mathtt{orig}\, v\) wraps an original variable \(v : V\), and \(\mathtt{extra}\, i\, j\) introduces a fresh auxiliary variable \(y_{i,j}\) used as a chain link when encoding clause \(i\) of length greater than three.
SATTo3SAT.liftLit maps a literal over \(V\) to the corresponding literal over \(\mathtt{AuxVar}\, V\) by wrapping each variable with \(\mathtt{orig}\), preserving polarity.
Given a clause index \(c\_ idx\), a lifting map \(ml\), a suffix list of literals \(\mathit{lits}\), and a chain counter \(j \ge 1\), SATTo3SAT.buildChain produces the middle and final 3-clauses of the chain encoding. Each middle step emits \(\langle \lnot y_{j-1},\, l_i,\, y_j\rangle \); the final step emits \(\langle \lnot y_{j-1},\, l_{n-1},\, l_n\rangle \) when only two literals remain.
SATTo3SAT.transformClause maps a single clause (at index \(c\_ idx\)) to a list of 3-clauses: the empty clause becomes two contradictory 3-clauses (unsatisfiable), a 1-literal clause becomes \(\langle l_1,l_1,l_1\rangle \), a 2-literal clause becomes \(\langle l_1,l_2,l_2\rangle \), a 3-literal clause is copied as-is, and any longer clause \(l_1 :: l_2 :: \mathit{rest}\) becomes \(\langle l_1, l_2, y_0\rangle \) followed by \(\texttt{SATTo3SAT.buildChain}\) on \(\mathit{rest}\).
The auxiliary recursive function SATTo3SAT.to3SATAux iterates SATTo3SAT.transformClause over a list of clauses, threading a clause index counter to ensure each clause uses distinct auxiliary variables.
SATTo3SAT.to3SAT converts a CNF formula \(f\) over \(V\) into a 3-CNF formula over \(\mathtt{AuxVar}\, V\) by calling SATTo3SAT.to3SATAux starting at index \(0\).
For a list of literals \(\mathit{lits}\) and index \(j\), \(\texttt{SATTo3SAT.extraVal}\, \alpha \, \mathit{lits}\, j\) holds iff every literal in \(\mathit{lits}.\mathtt{take}(j + 2)\) is false under \(\alpha \). This is the intended truth value of the auxiliary chain variable \(y_j\) in the encoding of \(\mathit{lits}\).
Provided \(j + 2 \le |\mathit{lits}|\), SATTo3SAT.extraVal \(\alpha \) \(\mathit{lits}\) \(j\) is logically equivalent to the condition that every element of \(\mathit{lits}.\mathtt{take}(j+2)\) is false under \(\alpha \).
Given \(\alpha : \mathtt{Assignment}\, V\) and a formula \(f\), SATTo3SAT.globalAssignment \(\alpha \, f\) is the assignment on \(\mathtt{AuxVar}\, V\) that maps each original variable \(\mathtt{orig}\, v\) to \(\alpha (v)\) and each auxiliary variable \(\mathtt{extra}\, i\, j\) to \(\texttt{SATTo3SAT.extraVal}\, \alpha \, (f.\mathtt{get}\, i)\, j\), i.e. the chain invariant “the first \(j+2\) literals of clause \(i\) are all false.”
A 3-clause \(c_3\) belongs to \(\texttt{SATTo3SAT.to3SATAux}\, \mathit{cs}\, \mathit{idx}\) if and only if there exists \(i \lt |\mathit{cs}|\) such that \(c_3\) belongs to \(\texttt{SATTo3SAT.transformClause}\, (\mathit{idx} + i)\, (\mathit{cs}_i)\).
A 3-clause \(c_3\) belongs to \(\texttt{SATTo3SAT.to3SAT}\, f\) if and only if there exists \(i \lt |f|\) such that \(c_3\) belongs to \(\texttt{SATTo3SAT.transformClause}\, i\, (f_i)\).
If \(l.\mathtt{drop}\, n = a :: \mathit{rest}\), then \(l.\mathtt{take}\, (n+1) = l.\mathtt{take}\, n \mathbin {+\! \! +} [a]\).
Let \(\alpha \) be an assignment satisfying at least one literal of a clause, and let \(\alpha _3\) be an assignment on \(\mathtt{AuxVar}\, V\) that evaluates auxiliary variables via SATTo3SAT.extraVal and lifted literals faithfully. Then every 3-clause produced by \(\texttt{SATTo3SAT.buildChain}\, c\_ idx\, ml\, \mathit{lits}\, j\) (with \(j \ge 1\) and \(\mathit{lits} = \mathit{clause}.\mathtt{drop}(j+1)\)) is satisfied by \(\alpha _3\).
A literal \(l\) in \(\mathtt{Literal}\, (\mathtt{AuxVar}\, V)\) is local to index \(i\) if every auxiliary variable appearing in \(l\) carries index \(i\). Literals over original variables are always local.
For a literal \(l\) local to index \(i\), the evaluation of \(l\) under the global assignment SATTo3SAT.globalAssignment \(\alpha \, f\) agrees with its evaluation under the local assignment that maps \(\mathtt{extra}\, i\, j \mapsto \texttt{SATTo3SAT.extraVal}\, \alpha \, (f_i)\, j\).
Every literal in any 3-clause produced by \(\texttt{SATTo3SAT.buildChain}\, i\, ml\, \ldots \) is local to index \(i\), provided the lifting map \(ml\) itself produces only literals local to \(i\).
Every literal in any 3-clause produced by \(\texttt{SATTo3SAT.transformClause}\, i\, \mathit{clause}\) is local to index \(i\).
For a 3-clause \(c_3\) produced by \(\texttt{SATTo3SAT.transformClause}\, i\, \mathit{clause}\) (where \(\mathit{clause} = f_i\)), satisfaction of \(c_3\) under the global assignment SATTo3SAT.globalAssignment \(\alpha \, f\) is equivalent to satisfaction under the local assignment \(\mathtt{extra}\, i\, j \mapsto \texttt{SATTo3SAT.extraVal}\, \alpha \, \mathit{clause}\, j\).
If a clause has at least one true literal under \(\alpha \), then every 3-clause in its encoding \(\texttt{SATTo3SAT.transformClause}\, c\_ idx\, \mathit{clause}\) is satisfied by the local assignment \(\mathtt{extra}\, c\_ idx\, j \mapsto \texttt{SATTo3SAT.extraVal}\, \alpha \, \mathit{clause}\, j\).
If a CNF formula \(f\) is satisfiable, then \(\texttt{SATTo3SAT.to3SAT}\, f\) is 3-satisfiable. The witnessing 3-SAT assignment is SATTo3SAT.globalAssignment \(\alpha \, f\), where \(\alpha \) is the original satisfying assignment.
If \(y_{j-1}\) is true, every \(ml\)-lifted literal in \(\mathit{lits}\) is false under \(\alpha _3\), and every 3-clause in \(\texttt{SATTo3SAT.buildChain}\, c\_ idx\, ml\, \mathit{lits}\, j\) is satisfied by \(\alpha _3\) (with \(j \ge 1\) and \(|\mathit{lits}| \ge 2\)), then a contradiction follows: the auxiliary variables are forced true one by one until the final chain clause has all three disjuncts false.
If every 3-clause in \(\texttt{SATTo3SAT.transformClause}\, c\_ idx\, \mathit{clause}\) is satisfied by \(\alpha _3\), then the original clause has at least one true literal under the restriction \(v \mapsto \alpha _3(\mathtt{orig}\, v)\).
If \(\texttt{SATTo3SAT.to3SAT}\, f\) is 3-satisfiable, then the original CNF formula \(f\) is satisfiable. The witnessing assignment for \(f\) is the restriction of any 3-SAT satisfying assignment \(\alpha _3\) to original variables, \(v \mapsto \alpha _3(\mathtt{orig}\, v)\).
A CNF formula \(f\) over \(V\) is satisfiable if and only if the 3-CNF formula \(\texttt{SATTo3SAT.to3SAT}\, f\) (over \(\mathtt{AuxVar}\, V\)) is 3-satisfiable. This combines SATTo3SAT.SAT_to_3SAT_completeness and SATTo3SAT.SAT_to_3SAT_soundness into a single biconditional.