Polynomial-time occurrence splitting

The occurrence-splitting construction of Papadimitriou, Proposition 9.3 is polynomial-time. Original variable labels keep their supplied encoding. The new clause and literal positions use unary encodings bounded by the input's literal and clause counts. In particular, binary natural labels are never expanded into unary labels.

Main results

• Cslib.Logic.PL.CNF.computableInPolyTime_implicationCycle: constructing binary cycles.
• Cslib.Logic.PL.CNF.computableInPolyTime_toThreeOccurrence: certified splitting.

References

• C. H. Papadimitriou, Computational Complexity, Proposition 9.3

theorem Cslib.Logic.PL.CNF.computableInPolyTime_implicationCycle {V : Type} (enc : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime implicationCycle (Turing.MultiTapeTM.encList enc) (encCNFOver enc)

Building binary implication cycles is polynomial-time for any variable encoding.

theorem Cslib.Logic.PL.CNF.computableInPolyTime_occurrenceClauses {V : Type} (enc : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime occurrenceClauses (encCNFOver enc) (encCNFOver (Turing.MultiTapeTM.encPair enc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary)))

Separating occurrences uses unary positions and preserves the original variable encoding.

theorem Cslib.Logic.PL.CNF.computableInPolyTime_toThreeOccurrence {V : Type} (enc : V ↪ List Bool) [DecidableEq V] : Turing.MultiTapeTM.ComputableInPolyTime toThreeOccurrence (encCNFOver enc) (encCNFOver (Turing.MultiTapeTM.encPair enc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary)))

Splitting is polynomial-time, with no unary expansion of original variable labels.