Documentation

Complexitylib.SAT.ThreeSAT.Syntax

Regular syntax checker for exact 3-CNF encodings #

Exact-3 shape is a regular property of the concrete CNF encoding. This module gives a finite-state left-to-right scanner for it and proves that the scanner accepts an encoded CNF exactly when every clause has three literals. The syntax language deliberately need not reject every malformed word: intersecting it with CNFSAT.language supplies well-formedness, which keeps this checker small and makes the intended 3SAT decomposition explicit.

Main results #

source
inductive Complexity.SAT.ThreeSAT.Syntax.TokenState :
Type

Parser state after consuming whole two-bit encoding tokens. between k means that k complete literals have been seen in the current clause.

Instances For
    source
    def Complexity.SAT.ThreeSAT.Syntax.instDecidableEqTokenState.decEq (x✝ x✝¹ : TokenState) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[implicit_reducible]
      instance Complexity.SAT.ThreeSAT.Syntax.instDecidableEqTokenState :
      DecidableEq TokenState
      Equations
      source
      @[implicit_reducible]
      instance Complexity.SAT.ThreeSAT.Syntax.instFintypeTokenState :
      Fintype TokenState
      Equations
      source
      def Complexity.SAT.ThreeSAT.Syntax.tokenStart :
      TokenState

      Initial token parser state: between clauses with no current literals.

      Equations
      Instances For
        source
        def Complexity.SAT.ThreeSAT.Syntax.tokenStep :
        TokenState → EncToken → TokenState

        One transition of the exact-3 grammar at token granularity.

        Equations
        Instances For
          source
          inductive Complexity.SAT.ThreeSAT.Syntax.BitState :
          Type

          Bit-level scanner state. half state b remembers the first bit of the next two-bit encoding token.

          Instances For
            source
            def Complexity.SAT.ThreeSAT.Syntax.instDecidableEqBitState.decEq (x✝ x✝¹ : BitState) :
            Decidable (x✝ = x✝¹)
            Equations
            Instances For
              source
              @[implicit_reducible]
              instance Complexity.SAT.ThreeSAT.Syntax.instDecidableEqBitState :
              DecidableEq BitState
              Equations
              source
              @[implicit_reducible]
              instance Complexity.SAT.ThreeSAT.Syntax.instFintypeBitState :
              Fintype BitState
              Equations
              • One or more equations did not get rendered due to their size.
              source
              def Complexity.SAT.ThreeSAT.Syntax.bitStart :
              BitState

              Initial bit-level scanner state.

              Equations
              Instances For
                source
                def Complexity.SAT.ThreeSAT.Syntax.tokenOfBits :
                Bool → Bool → EncToken

                Decode one of the four two-bit concrete token patterns.

                Equations
                Instances For
                  source
                  def Complexity.SAT.ThreeSAT.Syntax.bitStep :
                  BitState → Bool → BitState

                  One input-bit transition of the exact-3 syntax scanner.

                  Equations
                  Instances For
                    source
                    def Complexity.SAT.ThreeSAT.Syntax.accept (state : BitState) :
                    Bool

                    The scanner accepts precisely at a token boundary between clauses.

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

                      The regular language recognized by the exact-3 syntax scanner.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        @[simp]
                        theorem Complexity.SAT.ThreeSAT.Syntax.encode_mem_language_iff (formula : CNF) :
                        formula.encode ∈ language ↔ formula.Is3CNF

                        A typed CNF's bit encoding is accepted exactly when it is exact 3-CNF.

                        source
                        def Complexity.SAT.ThreeSAT.Syntax.syntaxTM :
                        TM 0

                        Concrete zero-work-tape finite-state checker for exact-3 syntax.

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

                          The syntax checker decides its regular language in exactly n + 2 steps.

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

                          The exact-3 syntax language is decidable in linear time.

                          source
                          theorem Complexity.SAT.ThreeSAT.language_eq_cnfsat_inter_syntax :
                          language = CNFSAT.language ∩ Syntax.language

                          3SAT is CNF-SAT intersected with the regular exact-3 syntax language.