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 definitions

• Cslib.Logic.PL.encOccurrence: encoding of a literal occurrence.

Main results

• Cslib.Logic.PL.Literal.computableInPolyTime_negate: literal negation.
• Cslib.Logic.PL.Clause.computableInPolyTime_impLits, Cslib.Logic.PL.Clause.computableInPolyTime_imp: implication clauses.
• Cslib.Logic.PL.Clause.computableInPolyTime_relabel, Cslib.Logic.PL.CNF.computableInPolyTime_relabel: renaming variables.
• Cslib.Logic.PL.CNF.computableInPolyTime_atLeastOne, Cslib.Logic.PL.CNF.computableInPolyTime_atMostOne, Cslib.Logic.PL.CNF.computableInPolyTime_exactlyOne: at-least-one, at-most-one and exactly-one constraints.
• Cslib.Logic.PL.CNF.computableInPolyTime_vars, Cslib.Logic.PL.CNF.computableInPolyTime_distinctVars, Cslib.Logic.PL.computableInPolyTime_occurrences: listing variable occurrences, distinct variables and literal occurrences.
• Cslib.Logic.PL.Clause.computableInPolyTime_length, Cslib.Logic.PL.CNF.computableInPolyTime_length, Cslib.Logic.PL.CNF.computableInPolyTime_vars_length, Cslib.Logic.PL.CNF.computableInPolyTime_numVars: clause, formula, variable-occurrence and distinct-variable counts in unary.
• Cslib.Logic.PL.CNF.computableInPolyTime_eval_bitsAssignment: evaluating a formula under a numbered assignment.
• 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_distinctVars {V : Type} [DecidableEq V] (enc : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime distinctVars (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool))) (Turing.MultiTapeTM.encList enc)

Listing the distinct variables of a formula in order of first occurrence is polynomial-time.

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

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

def Cslib.Logic.PL.encOccurrence {V : Type} (enc : V ↪ List Bool) : Occurrence V ↪ List Bool

Encoding of a literal occurrence: unary clause and position indices with an encoded literal.

theorem Cslib.Logic.PL.computableInPolyTime_occurrences {V : Type} (enc : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime occurrences (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool))) (Turing.MultiTapeTM.encList (encOccurrence enc))

Enumerating the literal occurrences of a CNF formula is polynomial-time.

theorem Cslib.Logic.PL.CNF.computableInPolyTime_eval_bitsAssignment {V : Type} [DecidableEq V] (enc : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (CNF V × List V) × ℕ) => eval (bitsAssignment p.1.2 p.2) p.1.1) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool))) (Turing.MultiTapeTM.encList enc)) Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBool

Evaluating a formula under the assignment numbered by i on a list of variables 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.