Polynomial-time variable occurrences of CSP instances

The variable occurrences F.vars of a CSP instance, their number, and the auxiliary formula F.varCNF are computable in polynomial time from the framed encoding encCSP.

Main results

• Cslib.Complexity.CSP.computableInPolyTime_vars: the occurrence list F.vars.
• Cslib.Complexity.CSP.computableInPolyTime_length_vars: its length, in unary.
• Cslib.Complexity.CSP.computableInPolyTime_varCNF: the auxiliary formula F.varCNF.
• Cslib.Complexity.CSP.computableInPolyTime_unary_to_binary: re-encoding natural-number variables from unary to binary.

theorem Cslib.Complexity.CSP.computableInPolyTime_vars {Rel V : Type} (encRel : Rel ↪ List Bool) (encV : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime Logic.PL.CSP.vars (encCSP encRel encV) (Turing.MultiTapeTM.encList encV)

Extracting the variable-occurrence list CSP.vars is computable in polynomial time.

theorem Cslib.Complexity.CSP.computableInPolyTime_length_vars {Rel V : Type} (encRel : Rel ↪ List Bool) (encV : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime (fun (F : Logic.PL.CSP Rel V) => F.vars.length) (encCSP encRel encV) Turing.MultiTapeTM.encUnary

The number F.vars.length of variable occurrences, in unary, is computable in polynomial time.

theorem Cslib.Complexity.CSP.computableInPolyTime_varCNF {Rel V : Type} (encRel : Rel ↪ List Bool) (encV : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime Logic.PL.CSP.varCNF (encCSP encRel encV) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool)))

Constructing the auxiliary positive-clause CNF CSP.varCNF is computable in polynomial time.

theorem Cslib.Complexity.CSP.computableInPolyTime_unary_to_binary {Rel : Type} (encRel : Rel ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime (fun (F : Logic.PL.CSP Rel ℕ) => F) (encCSP encRel Turing.MultiTapeTM.encUnary) (encCSP encRel Turing.MultiTapeTM.encNat)

Re-encoding the natural-number variables of a CSP instance from unary to binary is computable in polynomial time.