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 (Cslib.Logic.PL.encClause, Cslib.Logic.PL.encCNFOver). 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.Literal.computableInPolyTime_eval, Cslib.Logic.PL.Clause.computableInPolyTime_eval, Cslib.Logic.PL.CNF.computableInPolyTime_eval: evaluating literals, clauses and formulas under a polynomial-time assignment, as fun_prop rules.
• 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 (encClause enc) enc) (encClause enc)

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

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) (encClause encV) (encClause encW)

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) (encCNFOver encV) (encCNFOver encW)

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 (encCNFOver enc) (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 (encClause encV)) : 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 (encCNFOver encV)) : 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 (encCNFOver encV)) : 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 (encCNFOver enc) (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 (encCNFOver enc) 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 (encCNFOver enc) (Turing.MultiTapeTM.encList (encOccurrence enc))

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

theorem Cslib.Logic.PL.Literal.computableInPolyTime_eval {V : Type} {encV : V ↪ List Bool} {α : Type} {input : α ↪ List Bool} {σ : α → V → Bool} {l : α → Literal V} (hl : Turing.MultiTapeTM.ComputableInPolyTime l input (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool)) (hσ : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : α × V) => σ p.1 p.2) (Turing.MultiTapeTM.encPair input encV) Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => eval (σ a) (l a)) input Turing.MultiTapeTM.encBool

Evaluating a computed literal is polynomial-time under an assignment that is polynomial-time in the input and the variable. The literal's certificate comes first, so that it fixes the variable encoding before fun_prop certifies the assignment.

theorem Cslib.Logic.PL.Clause.computableInPolyTime_eval {V : Type} {encV : V ↪ List Bool} {α : Type} {input : α ↪ List Bool} {σ : α → V → Bool} {c : α → Clause V} (hc : Turing.MultiTapeTM.ComputableInPolyTime c input (encClause encV)) (hσ : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : α × V) => σ p.1 p.2) (Turing.MultiTapeTM.encPair input encV) Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => eval (σ a) (c a)) input Turing.MultiTapeTM.encBool

Evaluating a computed clause is polynomial-time under an assignment that is polynomial-time in the input and the variable.

theorem Cslib.Logic.PL.CNF.computableInPolyTime_eval {V : Type} {encV : V ↪ List Bool} {α : Type} {input : α ↪ List Bool} {σ : α → V → Bool} {φ : α → CNF V} (hφ : Turing.MultiTapeTM.ComputableInPolyTime φ input (encCNFOver encV)) (hσ : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : α × V) => σ p.1 p.2) (Turing.MultiTapeTM.encPair input encV) Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => eval (σ a) (φ a)) input Turing.MultiTapeTM.encBool

Evaluating a computed formula is polynomial-time under an assignment that is polynomial-time in the input and the variable.

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

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

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

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

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.