Documentation

CslibFrontier.Computability.Complexity.CookLevin.Encoding

Encodings for constructing the Cook–Levin tableau #

Intermediate features and variables are encoded by their existing indices in unary. The indices use a fixed nesting depth of the polynomial pairing function, so constructing features from unary times and positions has polynomial cost. States, tape numbers and symbols are fixed parameters. The final variable numbering converts the same indices to the binary encoding used by SAT.

These certificates concern construction and numbering. They do not provide a polynomial-time decoder or certify pattern matching on an arbitrary encoded feature.

Main definitions #

Main results #

References #

source
noncomputable def Cslib.Complexity.CookLevin.encFeature {k : ℕ} {State : Type} [Fintype State] :
Turing.MultiTapeTM.Feature k State ↪ List Bool

A feature is represented by its existing index in unary.

Instances For
    source
    noncomputable def Cslib.Complexity.CookLevin.encVar {k : ℕ} {State : Type} [Fintype State] :
    Var k State ↪ List Bool

    A tableau variable is represented by its existing index in unary.

    Instances For
      source
      theorem Cslib.Complexity.CookLevin.computableInPolyTime_featureIndex {k : ℕ} {State : Type} [Fintype State] :
      Turing.MultiTapeTM.ComputableInPolyTime featureIndex encFeature Turing.MultiTapeTM.encUnary

      The unary feature index is already the encoded word.

      source
      theorem Cslib.Complexity.CookLevin.computableInPolyTime_inRead {k : ℕ} {State : Type} [Fintype State] :
      Turing.MultiTapeTM.ComputableInPolyTime Turing.MultiTapeTM.Feature.inRead (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encBool) encFeature

      Construct the input-symbol feature from an optional Boolean symbol.

      source
      theorem Cslib.Complexity.CookLevin.computableInPolyTime_inPos {k : ℕ} {State : Type} [Fintype State] :
      Turing.MultiTapeTM.ComputableInPolyTime Turing.MultiTapeTM.Feature.inPos Turing.MultiTapeTM.encUnary encFeature

      Construct an input-head feature from a unary position.

      source
      theorem Cslib.Complexity.CookLevin.computableInPolyTime_head {k : ℕ} {State : Type} [Fintype State] (i : Fin k) :
      Turing.MultiTapeTM.ComputableInPolyTime (Turing.MultiTapeTM.Feature.head i) Turing.MultiTapeTM.encIntUnary encFeature

      Construct a work-head feature on a fixed tape from a signed unary position.

      source
      theorem Cslib.Complexity.CookLevin.computableInPolyTime_cell {k : ℕ} {State : Type} [Fintype State] (i : Fin k) (s : Option Bool) :
      Turing.MultiTapeTM.ComputableInPolyTime (fun (z : ℤ) => Turing.MultiTapeTM.Feature.cell i z s) Turing.MultiTapeTM.encIntUnary encFeature

      Construct a cell feature for a fixed tape and symbol from a signed unary position.

      source
      theorem Cslib.Complexity.CookLevin.computableInPolyTime_holds {k : ℕ} {State : Type} [Fintype State] :
      Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × Turing.MultiTapeTM.Feature k State) => Var.holds p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary encFeature) encVar

      Attach a unary time to an encoded feature.

      source
      theorem Cslib.Complexity.CookLevin.computableInPolyTime_cert {k : ℕ} {State : Type} [Fintype State] :
      Turing.MultiTapeTM.ComputableInPolyTime Var.cert Turing.MultiTapeTM.encUnary encVar

      Construct a certificate variable from its unary index.

      source
      theorem Cslib.Complexity.CookLevin.computableInPolyTime_index {k : ℕ} {State : Type} [Fintype State] :
      Turing.MultiTapeTM.ComputableInPolyTime Var.index encVar Turing.MultiTapeTM.encNat

      Emit the existing variable index in binary.

      source
      theorem Cslib.Complexity.CookLevin.computableInPolyTime_relabel {k : ℕ} {State : Type} [Fintype State] :
      Turing.MultiTapeTM.ComputableInPolyTime (Logic.PL.CNF.relabel Var.index) (Logic.PL.encCNFOver encVar) encCNF

      Convert a constructed tableau to the SAT encoding using its existing variable numbering.