Polynomial-time clause splitting

The existing recursive splitter agrees with an indexed traversal of the input clause. The certificate charges every lookup, fresh variable, copied literal, and list delimiter. Original variables keep their supplied encoding; fresh variables use their unary clause and chain indices.

Main results

• Cslib.Logic.PL.Clause.isPolyTime_split3: efficient splitting with a certified fresh-variable routine, retaining its captured input.
• Cslib.Logic.PL.CNF.isPolyTime_to3CNF: a uniform certificate for the existing 3CNF reduction.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 2.3.1

theorem Cslib.Logic.PL.Clause.isPolyTime_splitAux {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) => splitAux (fresh x) (index x) (carry x) (rest x)) input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool)))

Split a clause tail with a certified fresh-variable routine and runtime chain index.

theorem Cslib.Logic.PL.Clause.isPolyTime_split3 {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) => split3 (fresh x) (index x) (clause x)) input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool)))

Splitting a computed clause retains the input captured by its fresh-variable routine.

theorem Cslib.Logic.PL.CNF.isPolyTime_to3CNF {V : Type} (enc : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime to3CNF (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, encoding fresh variables by unary clause and chain indices. The certificate includes relabelling, clause traversal, and all output copying.