Tseitin splitting from CNF to exact 3-CNF

This definitions layer gives a total fresh-variable-threaded transformation from the existing unbounded-width SAT.CNF representation to exact 3-CNF.

Short nonempty clauses are padded by repeating literals. An empty clause is replaced by a contradictory pair of width-three unit clauses. A clause of width at least four is split by the standard chain

(a ∨ b ∨ z) ∧ (¬z ∨ rest).

Fresh counters are threaded across clauses, beginning above the largest source variable. Correctness and size theorems live in the internal and public layers.

def Complexity.SAT.Lit.neg (ℓ : Lit) : Lit

Negate a literal without changing its variable.

Equations

• ℓ.neg = { sign := !ℓ.sign, var := ℓ.var }

def Complexity.SAT.Lit.pos (v : ℕ) : Lit

Positive literal on variable v.

Equations

• Complexity.SAT.Lit.pos v = { sign := true, var := v }

def Complexity.SAT.Lit.negVar (v : ℕ) : Lit

Negative literal on variable v.

Equations

• Complexity.SAT.Lit.negVar v = { sign := false, var := v }

def Complexity.SAT.Clause.tseitinFreshCount (c : Clause) : ℕ

Number of fresh variables consumed while splitting one clause. Empty clauses use one variable for a contradictory gadget; a clause of width k ≥ 4 uses k - 3 chain variables.

Equations

• c.tseitinFreshCount = if c = [] then 1 else List.length c - 3

@[irreducible]

def Complexity.SAT.Clause.to3CNF (next : ℕ) : Clause → CNF

Split one clause into exact-width-three clauses, drawing auxiliary variables consecutively from next.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.SAT.Clause.to3CNF next [a] = [[a, a, a]]
• Complexity.SAT.Clause.to3CNF next [a, b] = [[a, b, b]]
• Complexity.SAT.Clause.to3CNF next [a, b, c] = [[a, b, c]]
• Complexity.SAT.Clause.to3CNF next (a :: b :: c :: d :: rest) = [a, b, Complexity.SAT.Lit.pos next] :: Complexity.SAT.Clause.to3CNF (next + 1) (Complexity.SAT.Lit.negVar next :: c :: d :: rest)

def Complexity.SAT.CNF.literalCount (φ : CNF) : ℕ

Total number of literal occurrences in a CNF.

Equations

• φ.literalCount = List.foldr (fun (c : Complexity.SAT.Clause) (total : ℕ) => List.length c + total) 0 φ

def Complexity.SAT.CNF.tseitinFreshCount (φ : CNF) : ℕ

Total number of fresh variables consumed by all clause splitters.

Equations

• φ.tseitinFreshCount = List.foldr (fun (c : Complexity.SAT.Clause) (total : ℕ) => c.tseitinFreshCount + total) 0 φ

def Complexity.SAT.CNF.to3Aux : ℕ → CNF → CNF × ℕ

Split every clause while threading the fresh-variable counter. The second component is the first unused variable after the transformation.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.SAT.CNF.to3Aux x✝ [] = ([], x✝)

def Complexity.SAT.CNF.to3 (φ : CNF) : CNF

Convert an arbitrary CNF to exact 3-CNF. Auxiliary variables begin one past the largest variable occurring in the source.

Equations

• φ.to3 = (Complexity.SAT.CNF.to3Aux (φ.maxVar + 1) φ).1