Polynomial-time instantiation of fixed CNF templates

For a fixed finite relation alphabet, every fixed family of CNF templates can be instantiated in native polynomial time. Local template positions use unary encoding for list lookup, whereas the original variable labels retain their binary encoding. Templates and their sizes are fixed independently of the input instance; no uniform complexity bound in a supplied language is asserted.

Main results

• Cslib.Complexity.CSP.computableInPolyTime_instantiateCNF: native polynomial-time template instantiation for a finite relation alphabet.

theorem Cslib.Complexity.CSP.computableInPolyTime_instantiateCNF {Rel : Type} [Finite Rel] (encRel : Rel ↪ List Bool) (template : Rel → Logic.PL.CNF ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (Logic.PL.CSP.instantiateCNF 0 template) (encCSP encRel Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encBool)))

Fixed CNF templates over a finite relation alphabet can be instantiated in polynomial time, with binary variable labels and unary local positions.