Documentation

CslibFrontier.Computability.Complexity.Problems.ThreeSAT

3SAT #

ThreeSAT is the set of satisfiable formulas in conjunctive normal form whose clauses have at most three literals Arora and Barak, Section 2.3.1. toThreeSAT maps a formula to an equisatisfiable one of width three, by splitting its clauses (Cslib.Logic.PL.CNF.to3CNF) and numbering the variables injectively. Combining CNF.isPolyTime_to3CNF with binary variable relabelling and the Cook–Levin theorem proves that ThreeSAT is NP-complete.

Main definitions #

Main results #

References #

source
def Cslib.Complexity.ThreeSAT :
Set (Logic.PL.CNF ℕ)

The satisfiable formulas whose clauses have at most three literals [Kar72], Arora and Barak, Section 2.3.1.

Instances For
    source
    def Cslib.Complexity.splitVarToNat :
    ℕ ⊕ ℕ × ℕ → ℕ

    An injective numbering of the variables of a split formula: original variables at even numbers, auxiliary variables at odd numbers through Nat.pair.

    Instances For
      source
      theorem Cslib.Complexity.splitVarToNat_injective :
      Function.Injective splitVarToNat
      source
      def Cslib.Complexity.toThreeSAT (φ : Logic.PL.CNF ℕ) :
      Logic.PL.CNF ℕ

      The reduction from SAT to ThreeSAT: split the clauses, then number the variables.

      Instances For
        source
        theorem Cslib.Complexity.mem_ThreeSAT_toThreeSAT_iff (φ : Logic.PL.CNF ℕ) :
        toThreeSAT φ ∈ ThreeSAT ↔ φ ∈ SAT

        Correctness of the reduction: toThreeSAT φ is in ThreeSAT exactly when φ is in SAT.

        Polynomial-time reduction and NP-completeness #

        source
        theorem Cslib.Complexity.computableInPolyTime_splitVarToNat :
        Turing.MultiTapeTM.ComputableInPolyTime splitVarToNat (Turing.MultiTapeTM.encSum Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary)) Turing.MultiTapeTM.encNat

        Variable numbering after clause splitting is polynomial-time: original binary variables shift by one bit, and unary fresh-variable pairs are paired and converted to odd binary numbers.

        source
        theorem Cslib.Complexity.computableInPolyTime_toThreeSAT :
        Turing.MultiTapeTM.ComputableInPolyTime toThreeSAT encCNF encCNF

        The reduction toThreeSAT is computable in polynomial time under encCNF.

        source
        def Cslib.Complexity.ThreeSAT.verifier (x : Logic.PL.CNF ℕ × List Bool) :
        Bool

        The verifier for ThreeSAT: check that every clause has at most three literals and evaluate the formula under the certificate assignment.

        Instances For
          source
          theorem Cslib.Complexity.ThreeSAT.isVerifier :
          IsVerifier encCNF Polynomial.X verifier ThreeSAT

          ThreeSAT.verifier verifies ThreeSAT with certificates as long as the encoded formula: it is SAT.verifier guarded by the clause-width test.

          source
          theorem Cslib.Complexity.ThreeSAT.computableInPolyTime_verifier :
          Turing.MultiTapeTM.ComputableInPolyTime verifier (Turing.MultiTapeTM.encPair encCNF Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

          Checking the clause-width bound and evaluating the formula is polynomial-time.

          source
          theorem Cslib.Complexity.ThreeSAT.mem_NP :
          ThreeSAT ∈ NP encCNF

          ThreeSAT belongs to NP.

          source
          theorem Cslib.Complexity.polyTimeReducible_SAT_ThreeSAT :
          PolyTimeReducible encCNF encCNF SAT ThreeSAT

          SAT reduces to ThreeSAT in polynomial time via toThreeSAT.

          source
          theorem Cslib.Complexity.ThreeSAT_npHard :
          NPHard encCNF ThreeSAT

          ThreeSAT is NP-hard.

          source
          theorem Cslib.Complexity.ThreeSAT_npComplete :
          NPComplete encCNF ThreeSAT

          3SAT is NP-complete [Kar72].