Documentation

Complexitylib.SAT.ThreeSAT

Encoded CNF-SAT and 3SAT languages #

This module names the existing encoded SAT problem as CNFSAT and defines ThreeSAT by restricting decoded CNFs to clauses of exactly three literals. It is a semantic and codec interface only; no complexity-class membership or reduction claim is made here.

Main definitions and results #

source
def Complexity.SAT.CNF.decode3? (z : List Bool) :
Option CNF

Decode a concrete SAT bit string and accept it only when every decoded clause contains exactly three literals.

Equations
Instances For
    source
    @[simp]
    theorem Complexity.SAT.CNF.decode3?_encode {φ : CNF} (h3 : φ.Is3CNF) :
    decode3? φ.encode = some φ

    An exact 3-CNF survives encoding followed by restricted decoding.

    source
    theorem Complexity.SAT.CNF.decode3?_sound {z : List Bool} {φ : CNF} (h : decode3? z = some φ) :
    z = φ.encode ∧ φ.Is3CNF

    Restricted decoding is sound for both the concrete encoding and the exact-three-literal shape.

    source
    theorem Complexity.SAT.CNF.decode3?_eq_some_iff {z : List Bool} {φ : CNF} :
    decode3? z = some φ ↔ z = φ.encode ∧ φ.Is3CNF

    Characterization of successful exact-3 decoding.

    source
    theorem Complexity.SAT.CNF.encode_injective :
    Function.Injective encode

    The concrete CNF encoding is injective.

    CNF-SAT compatibility surface #

    source
    @[reducible, inline]
    abbrev Complexity.SAT.CNFSAT.language :
    Language

    Compatibility name for the library's existing SAT language, whose inputs are concrete encodings of satisfiable CNF formulas.

    Equations
    Instances For
      source
      theorem Complexity.SAT.CNFSAT.language_eq_sat :
      language = SAT.language

      The compatibility name denotes exactly the existing SAT language.

      source
      @[simp]
      theorem Complexity.SAT.CNFSAT.mem_language_iff_sat (z : List Bool) :
      z ∈ language ↔ z ∈ SAT.language

      Membership through the compatibility name is definitionally the existing SAT membership predicate.

      source
      theorem Complexity.SAT.CNFSAT.mem_language_iff_decode (z : List Bool) :
      z ∈ language ↔ ∃ (φ : CNF), CNF.decode? z = some φ ∧ φ.Satisfiable

      A bit string is in CNF-SAT exactly when it decodes to a satisfiable CNF.

      source
      @[simp]
      theorem Complexity.SAT.CNFSAT.encode_mem_language_iff (φ : CNF) :
      φ.encode ∈ language ↔ φ.Satisfiable

      Encoding a typed CNF is in CNF-SAT exactly when that formula is satisfiable.

      3SAT #

      source
      def Complexity.SAT.ThreeSAT.language :
      Language

      3SAT consists of concrete encodings of satisfiable CNFs in which every clause has exactly three literals.

      Equations
      Instances For
        source
        theorem Complexity.SAT.ThreeSAT.mem_language_iff_decode3 (z : List Bool) :
        z ∈ language ↔ ∃ (φ : CNF), CNF.decode3? z = some φ ∧ φ.Satisfiable

        A bit string is in 3SAT exactly when restricted decoding succeeds with a satisfiable formula.

        source
        @[simp]
        theorem Complexity.SAT.ThreeSAT.encode_mem_language_iff (φ : CNF) :
        φ.encode ∈ language ↔ φ.Is3CNF ∧ φ.Satisfiable

        Encoding a typed CNF belongs to 3SAT exactly when it is an exact 3-CNF and is satisfiable.

        source
        theorem Complexity.SAT.ThreeSAT.language_subset_cnfsat :
        language ⊆ CNFSAT.language

        Every 3SAT instance is, after forgetting the shape restriction, a CNF-SAT instance.

        source
        def Complexity.SAT.ThreeSAT.falseFormula :
        CNF

        A fixed unsatisfiable exact 3-CNF: one clause forces x₀, while the other forces ¬x₀. Repeated literals make both clauses have width exactly three.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem Complexity.SAT.ThreeSAT.falseFormula_is3CNF :
          falseFormula.Is3CNF

          falseFormula has exactly three literals in each clause.

          source
          theorem Complexity.SAT.ThreeSAT.falseFormula_not_satisfiable :
          ¬falseFormula.Satisfiable

          falseFormula is unsatisfiable.

          source
          def Complexity.SAT.ThreeSAT.fallbackEncoding :
          List Bool

          A valid encoded 3-CNF no-instance suitable as the target of malformed or otherwise invalid source inputs in later total reductions.

          Equations
          Instances For
            source
            @[simp]
            theorem Complexity.SAT.ThreeSAT.decode3?_fallbackEncoding :
            CNF.decode3? fallbackEncoding = some falseFormula

            The fallback encoding decodes successfully as falseFormula.

            source
            theorem Complexity.SAT.ThreeSAT.fallbackEncoding_not_mem_language :
            fallbackEncoding ∉ language

            The fallback encoding is not a member of 3SAT.