Polynomial-time count-preserving clause splitting

The recursive OR-gate chain agrees with an indexed traversal of the input clause, with three clauses per gate. The certificate charges every lookup, fresh variable, copied literal and list delimiter. Original variables keep their supplied encoding; gate variables use their unary clause and gate indices. This mirrors the certificate for Cslib.Logic.PL.CNF.to3CNF.

Main results

• Cslib.Logic.PL.Clause.isPolyTime_orChainAux: efficient OR-gate chains of clause tails.
• Cslib.Logic.PL.Clause.isPolyTime_orSplit3: efficient chains with a certified fresh-variable routine, retaining its captured input.
• Cslib.Logic.PL.CNF.isPolyTime_toExact3CNF: a uniform certificate for the count-preserving 3CNF reduction.

References

• OpenAI, The Exponential Time Hypothesis is False

theorem Cslib.Logic.PL.Clause.isPolyTime_orChainAux {W Input : Type} {input : Input ↪ List Bool} {enc : W ↪ List Bool} {fresh : Input → ℕ → W} {index : Input → ℕ} {carry : Input → Literal W} {rest : Input → Clause W} (hrest : Turing.MultiTapeTM.ComputableInPolyTime rest input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool))) (hcarry : Turing.MultiTapeTM.ComputableInPolyTime carry input (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool)) (hindex : Turing.MultiTapeTM.ComputableInPolyTime index input Turing.MultiTapeTM.encUnary) (hfresh : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Input × ℕ) => fresh p.1 p.2) (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encUnary) enc) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : Input) => orChainAux (fresh x) (index x) (carry x) (rest x)) input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool)))

The OR-gate chain of a clause tail, with a certified fresh-variable routine and runtime gate index.

theorem Cslib.Logic.PL.Clause.isPolyTime_orSplit3 {W Input : Type} {input : Input ↪ List Bool} {enc : W ↪ List Bool} {fresh : Input → ℕ → W} {index : Input → ℕ} {clause : Input → Clause W} (hclause : Turing.MultiTapeTM.ComputableInPolyTime clause input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool))) (hindex : Turing.MultiTapeTM.ComputableInPolyTime index input Turing.MultiTapeTM.encUnary) (hfresh : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Input × ℕ) => fresh p.1 p.2) (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encUnary) enc) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : Input) => orSplit3 (fresh x) (index x) (clause x)) input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool)))

The OR-gate chain of a computed clause retains the input captured by its fresh-variable routine.

theorem Cslib.Logic.PL.CNF.isPolyTime_toExact3CNF {V : Type} (enc : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime toExact3CNF (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encSum enc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary)) Turing.MultiTapeTM.encBool)))

Convert an arbitrary CNF formula to 3CNF with the same number of models, encoding gate variables by unary clause and gate indices. The certificate includes relabelling, clause traversal and all output copying.