Documentation

CslibFrontier.Computability.Complexity.Problems.ExactThreeSAT

3SAT with clauses of exactly three literals #

ExactThreeSAT is the set of satisfiable formulas in conjunctive normal form all of whose clauses are lists of exactly three literals. The literals of a clause need not be distinct, so a clause x ∨ x ∨ y is allowed. This is weaker than 3-satisfiability as defined by Garey and Johnson Garey and Johnson, Problem LO2, whose clauses are sets of three distinct literals. The stronger distinct-variable version is proved NP-complete as EUThreeSAT in CslibFrontier.Computability.Complexity.Problems.EUThreeSAT.

ExactThreeSAT is NP-complete: ThreeSAT (clauses of at most three literals) reduces to it by repeating a literal of every clause with one or two literals (Cslib.Complexity.ExactThreeSAT.padClause, Cslib.Complexity.toExactThreeSAT). Repetition does not change the value of a clause, and the empty clause stays empty, so a formula with an empty clause stays unsatisfiable.

Main definitions #

Main results #

References #

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

The satisfiable formulas all of whose clauses have exactly three literals, not necessarily distinct. The 3-satisfiability of Garey and Johnson, Problem LO2 requires them to be distinct.

Instances For
    source
    def Cslib.Complexity.ExactThreeSAT.padClause (c : Logic.PL.Clause ℕ) :
    Logic.PL.Clause ℕ

    Pad a clause of one or two literals to three literals by repeating literals; other clauses are unchanged.

    Instances For
      source
      theorem Cslib.Complexity.ExactThreeSAT.length_padClause {c : Logic.PL.Clause ℕ} (h0 : c ≠ []) (h3 : List.length c ≤ 3) :
      List.length (padClause c) = 3

      Padding a nonempty clause of at most three literals gives exactly three.

      source
      theorem Cslib.Complexity.ExactThreeSAT.eval_padClause (σ : ℕ → Bool) (c : Logic.PL.Clause ℕ) :
      Logic.PL.Clause.eval σ (padClause c) = Logic.PL.Clause.eval σ c

      Repeating literals does not change the value of a clause.

      source
      theorem Cslib.Complexity.ExactThreeSAT.computableInPolyTime_padClause :
      Turing.MultiTapeTM.ComputableInPolyTime padClause (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encBool)) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encBool))

      Padding a clause is polynomial-time.

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

      The verifier for ExactThreeSAT: check that every clause has exactly three literals and evaluate the formula under the certificate assignment.

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

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

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

        Checking the clause widths and evaluating the formula is polynomial-time.

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

        ExactThreeSAT belongs to NP.

        source
        def Cslib.Complexity.toExactThreeSAT (φ : Logic.PL.CNF ℕ) :
        Logic.PL.CNF ℕ

        The reduction from ThreeSAT to ExactThreeSAT: pad every clause.

        Instances For
          source
          theorem Cslib.Complexity.computableInPolyTime_toExactThreeSAT :
          Turing.MultiTapeTM.ComputableInPolyTime toExactThreeSAT encCNF encCNF

          Padding every clause is polynomial-time.

          source
          theorem Cslib.Complexity.mem_ExactThreeSAT_toExactThreeSAT_iff (φ : Logic.PL.CNF ℕ) :
          toExactThreeSAT φ ∈ ExactThreeSAT ↔ φ ∈ ThreeSAT

          A formula is in ThreeSAT exactly when padding its clauses puts it in ExactThreeSAT.

          source
          theorem Cslib.Complexity.polyTimeReducible_ThreeSAT_ExactThreeSAT :
          PolyTimeReducible encCNF encCNF ThreeSAT ExactThreeSAT

          ThreeSAT reduces to ExactThreeSAT in polynomial time via toExactThreeSAT.

          source
          theorem Cslib.Complexity.ExactThreeSAT_npHard :
          NPHard encCNF ExactThreeSAT

          ExactThreeSAT is NP-hard.

          source
          theorem Cslib.Complexity.ExactThreeSAT_npComplete :
          NPComplete encCNF ExactThreeSAT

          3SAT with clauses of exactly three, not necessarily distinct, literals is NP-complete.