Documentation

Complexitylib.SAT.ThreeSAT.Verifier

Exact-3 syntax on paired verifier inputs #

The SAT verifier receives pair(z, α), where every bit of z is doubled and the pair separator is 01. This module gives a small finite-state scanner that feeds the decoded left component into ThreeSAT.Syntax and ignores the witness suffix. It recognizes pair(z, α) exactly when z passes the exact-3 syntax checker.

Main results #

source
inductive Complexity.SAT.ThreeSAT.PairSyntax.State :
Type

State of the paired-input scanner. first and second decode the doubled left component, right ignores the witness suffix, and reject is absorbing.

Instances For
    source
    def Complexity.SAT.ThreeSAT.PairSyntax.instDecidableEqState.decEq (x✝ x✝¹ : State) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[implicit_reducible]
      instance Complexity.SAT.ThreeSAT.PairSyntax.instDecidableEqState :
      DecidableEq State
      Equations
      source
      @[implicit_reducible]
      instance Complexity.SAT.ThreeSAT.PairSyntax.instFintypeState :
      Fintype State
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Complexity.SAT.ThreeSAT.PairSyntax.initial :
      State

      Initial paired-input scanner state.

      Equations
      Instances For
        source
        def Complexity.SAT.ThreeSAT.PairSyntax.step :
        State → Bool → State

        Consume one concrete bit of a paired verifier input.

        Equations
        Instances For
          source
          def Complexity.SAT.ThreeSAT.PairSyntax.accept :
          State → Bool

          Accept after seeing the pair separator with an exact-3 left component.

          Equations
          Instances For
            source
            def Complexity.SAT.ThreeSAT.PairSyntax.language :
            Language

            Regular language of paired words whose left component has exact-3 syntax.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem Complexity.SAT.ThreeSAT.PairSyntax.pair_mem_language_iff (z witness : List Bool) :
              pair z witness ∈ language ↔ z ∈ Syntax.language

              A canonical pair belongs to the paired syntax language exactly when its left component belongs to the exact-3 syntax language.

              source
              def Complexity.SAT.ThreeSAT.PairSyntax.pairSyntaxTM :
              TM 0

              Zero-work-tape scanner for exact-3 syntax on paired inputs.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem Complexity.SAT.ThreeSAT.PairSyntax.pairSyntaxTM_decidesInTime :
                pairSyntaxTM.DecidesInTime language fun (n : ℕ) => n + 2

                The paired syntax scanner decides its language in exactly n + 2 steps.

                source
                theorem Complexity.SAT.ThreeSAT.PairSyntax.language_mem_P :
                language ∈ P

                Exact-3 syntax on paired inputs is decidable in linear time.