Polynomial-time CNF construction

The clause and formula constructors used by reductions to satisfiability are polynomial-time for any fixed encoding of their variables. Literals use encPair, and clauses and formulas use encList. Specializing the variable encoding to binary naturals gives the encoding of SAT.

These results certify the existing constructors, including the ordered-pair implementation of exactly-one constraints. They apply to empty lists and lists with repeated variables. Relabelling requires a polynomial-time renaming function, but does not require injectivity; injectivity is needed separately when transferring satisfiability.

Main results

• Cslib.Logic.PL.Clause.computableInPolyTime_impLits, .computableTidilyInPolyTime_imp: implication clauses.
• Cslib.Logic.PL.Clause.computableInPolyTime_relabel, Cslib.Logic.PL.CNF.computableInPolyTime_relabel: renaming variables.
• Cslib.Logic.PL.CNF.computableInPolyTime_exactlyOne: exactly-one constraints.
• Cslib.Logic.PL.CNF.computableInPolyTime_vars: listing variable occurrences.
• Cslib.Logic.PL.Clause.computableInPolyTime_length, Cslib.Logic.PL.CNF.computableInPolyTime_length, Cslib.Logic.PL.CNF.computableInPolyTime_vars_length: clause, formula and variable-occurrence counts in unary.
• Cslib.Logic.PL.CNF.isPolyTime_compact: compact unary indices for arbitrary variable names.

References

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

theorem Cslib.Logic.PL.Literal.computableInPolyTime_negate {V : Type} (enc : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime Std.Sat.Literal.negate (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool) (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool)

Negating a literal changes only its polarity.

theorem Cslib.Logic.PL.Clause.computableInPolyTime_impLits {V : Type} (enc : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List (Literal V) × V) => impLits p.1 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool)) enc) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool))

Construct an implication from literals, with a positive conclusion.

theorem Cslib.Logic.PL.Clause.computableInPolyTime_imp {V : Type} (enc : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List V × V) => imp p.1 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList enc) enc) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool))

Construct an implication from positive hypotheses and a positive conclusion.

theorem Cslib.Logic.PL.Clause.computableInPolyTime_relabel {V W : Type} {encV : V ↪ List Bool} {encW : W ↪ List Bool} {f : V → W} (hf : Turing.MultiTapeTM.ComputableInPolyTime f encV encW) : Turing.MultiTapeTM.ComputableInPolyTime (relabel f) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool)) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encW Turing.MultiTapeTM.encBool))

Relabelling a clause is polynomial-time whenever the renaming function is.

theorem Cslib.Logic.PL.CNF.computableInPolyTime_relabel {V W : Type} {encV : V ↪ List Bool} {encW : W ↪ List Bool} {f : V → W} (hf : Turing.MultiTapeTM.ComputableInPolyTime f encV encW) : Turing.MultiTapeTM.ComputableInPolyTime (relabel f) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encW Turing.MultiTapeTM.encBool)))

Relabelling a formula is polynomial-time whenever the renaming function is.

theorem Cslib.Logic.PL.CNF.computableInPolyTime_vars {V : Type} (enc : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime vars (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool))) (Turing.MultiTapeTM.encList enc)

List the variables of a formula in order, including repetitions.

theorem Cslib.Logic.PL.Clause.computableInPolyTime_length {V : Type} {encV : V ↪ List Bool} {α : Type} {input : α ↪ List Bool} {c : α → Clause V} (hc : Turing.MultiTapeTM.ComputableInPolyTime c input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => List.length (c a)) input Turing.MultiTapeTM.encUnary

The number of literals in a polynomial-time clause, in unary, is polynomial-time.

theorem Cslib.Logic.PL.CNF.computableInPolyTime_length {V : Type} {encV : V ↪ List Bool} {α : Type} {input : α ↪ List Bool} {φ : α → CNF V} (hφ : Turing.MultiTapeTM.ComputableInPolyTime φ input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool)))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => List.length (φ a)) input Turing.MultiTapeTM.encUnary

The number of clauses in a polynomial-time formula, in unary, is polynomial-time.

theorem Cslib.Logic.PL.CNF.computableInPolyTime_vars_length {V : Type} {encV : V ↪ List Bool} {α : Type} {input : α ↪ List Bool} {φ : α → CNF V} (hφ : Turing.MultiTapeTM.ComputableInPolyTime φ input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool)))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => (φ a).vars.length) input Turing.MultiTapeTM.encUnary

The number of variable occurrences in a polynomial-time formula, in unary, is polynomial-time.

theorem Cslib.Logic.PL.CNF.computableInPolyTime_atLeastOne {V : Type} (enc : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime atLeastOne (Turing.MultiTapeTM.encList enc) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool)))

Construct the clause requiring at least one listed variable to hold.

theorem Cslib.Logic.PL.CNF.computableInPolyTime_atMostOne {V : Type} [DecidableEq V] (enc : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime atMostOne (Turing.MultiTapeTM.encList enc) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool)))

Construct the clauses forbidding two distinct listed variables from both holding. The list may contain repeated variables.

theorem Cslib.Logic.PL.CNF.computableInPolyTime_exactlyOne {V : Type} [DecidableEq V] (enc : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime exactlyOne (Turing.MultiTapeTM.encList enc) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool)))

Construct exactly-one constraints in polynomial time, including for empty or repeated lists.

theorem Cslib.Logic.PL.CNF.isPolyTime_compact {V : Type} [DecidableEq V] (enc : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime compact (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool)))

The entire input-dependent renaming is polynomial-time for any original variable encoding. Its output indices use unary encoding and are bounded by the input's number of occurrences.