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_splitAux: efficient splitting of clause tails.
• 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 (encClause enc)) (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 (encCNFOver enc)

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 (encClause enc)) (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 (encCNFOver enc)

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 (encCNFOver enc) (encCNFOver (Turing.MultiTapeTM.encSum enc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary)))

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.