Documentation

CslibFrontier.Computability.Complexity.Problems.ThreeSATThree

3SAT with at most three occurrences per variable #

ThreeSATThree uses clauses of width at most three, allowing binary clauses. Every variable has at most three literal occurrences, including repeated literals within a clause Papadimitriou, Proposition 9.3. Only the variable-occurrence restriction of that proposition is formalized; its additional bound of two occurrences per signed literal is not part of ThreeSATThree or the completeness theorem. The reduction splits occurrences and connects the copies by binary implication cycles. It is total on all CNF inputs: a formula having a clause longer than three maps to the unsatisfiable formula [[]]. Original natural labels stay binary throughout; only syntactic positions use unary counters.

The construction is adapted from lean-trominoes revision 6d5b36c15cec6cb18d30137b7f1c7fb92ea24332, PeriodicThreeSATThree.lean, PeriodicThreeSATThreeCorrectness.lean, and PeriodicThreeSATThreeExactSize.lean. This endpoint imposes no planarity condition.

Main definitions #

Main results #

References #

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

Satisfiable CNF formulas of width at most three, with at most three literal occurrences per variable. Repetitions count, and binary clauses are permitted.

Instances For
    source
    def Cslib.Complexity.ThreeSATThree.numberCopy (x : ℕ × ℕ × ℕ) :
    ℕ

    Injectively encode an original binary label and its two occurrence indices.

    Instances For
      source
      theorem Cslib.Complexity.ThreeSATThree.numberCopy_injective :
      Function.Injective numberCopy

      Numbering copies is injective, independently of whether they occur in a formula.

      source
      theorem Cslib.Complexity.ThreeSATThree.computableInPolyTime_numberCopy :
      Turing.MultiTapeTM.ComputableInPolyTime numberCopy (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary)) Turing.MultiTapeTM.encNat

      Numbering copies is polynomial-time without expanding the original binary label.

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

      Check clause widths, literal-occurrence bounds, and a satisfying assignment.

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

        The occurrence restriction is a polynomial-time guard on the usual SAT verifier.

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

        The width/occurrence tests and SAT evaluation run in native polynomial time.

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

        3SAT-3 belongs to NP under the ordinary binary CNF encoding.

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

        Reject non-width-three inputs, and otherwise split occurrences and number the copies.

        Instances For
          source
          theorem Cslib.Complexity.length_toThreeSATThree (φ : Logic.PL.CNF ℕ) (hφ : ∀ c ∈ φ, List.length c ≤ 3) :
          List.length (toThreeSATThree φ) = List.length φ + φ.vars.length

          For a width-three input, numbering preserves the splitter's exact clause count.

          source
          theorem Cslib.Complexity.length_vars_toThreeSATThree (φ : Logic.PL.CNF ℕ) (hφ : ∀ c ∈ φ, List.length c ≤ 3) :
          (toThreeSATThree φ).vars.length = 3 * φ.vars.length

          For a width-three input, numbering preserves the exact literal-occurrence count.

          source
          theorem Cslib.Complexity.modelCount_toThreeSATThree (φ : Logic.PL.CNF ℕ) (hφ : ∀ c ∈ φ, List.length c ≤ 3) :
          (toThreeSATThree φ).modelCount = φ.modelCount

          For a width-three input, occurrence splitting and injective numbering preserve the number of satisfying assignments on occurring variables.

          source
          theorem Cslib.Complexity.computableInPolyTime_toThreeSATThree :
          Turing.MultiTapeTM.ComputableInPolyTime toThreeSATThree encCNF encCNF

          The total splitter is polynomial-time under binary encCNF.

          source
          theorem Cslib.Complexity.mem_ThreeSATThree_toThreeSATThree_iff (φ : Logic.PL.CNF ℕ) :
          toThreeSATThree φ ∈ ThreeSATThree ↔ φ ∈ ThreeSAT

          Correctness holds for all CNF inputs, including those outside the width-three restriction.

          source
          theorem Cslib.Complexity.polyTimeReducible_ThreeSAT_ThreeSATThree :
          PolyTimeReducible encCNF encCNF ThreeSAT ThreeSATThree

          ThreeSAT reduces to 3SAT-3.

          source
          theorem Cslib.Complexity.ThreeSATThree_npHard :
          NPHard encCNF ThreeSATThree

          3SAT-3 is NP-hard.

          source
          theorem Cslib.Complexity.ThreeSATThree_npComplete :
          NPComplete encCNF ThreeSATThree

          3SAT with at most three occurrences per variable is NP-complete Papadimitriou, Proposition 9.3. The additional per-signed-literal bound in that proposition is not part of this statement.