Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

(3,4)-satisfiability is NP-hard

Lax345332.ThreeFourSat · concepts/Lax345332/ThreeFourSat.lean · lax-345332

open

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    (3,4)-SAT is satisfiability restricted to formulas in which every clause contains exactly three literals and every variable occurs at most four times. Tovey proved that it is NP-hard: every language in NP has a polynomial-time many-one reduction to it.

    Concept map
    8 concepts; 1 descendant hidden
    100%
    Proven claimOpen claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax429075.Reductions
    2import Lax429075.Satisfiability
    3
    4/-!
    5---
    6title: (3,4)-satisfiability is NP-hard
    7type: theorem
    8---
    9*(3,4)-SAT* is satisfiability restricted to formulas in which every clause contains
    10exactly three literals and every variable occurs at most four times. Tovey proved that it
    11is NP-hard: every language in NP has a polynomial-time many-one reduction to it.
    12
    13# Formalization notes
    14
    15The restriction is a predicate on the CNF formulas of the archive's Cook–Levin submission,
    16so the encoding and the notion of satisfiability are shared with unrestricted SAT.
    17Occurrences are counted with multiplicity.
    18-/
    19
    20namespace Lax345332.ThreeFourSat
    21
    22open Lax429075.CNF Lax434930.PolynomialTime
    23
    24/-- The number of occurrences of the variable `i` in the formula `F`. -/
    25def occurrences (F : Formula) (i : ℕ) : ℕ :=
    26 (F.flatMap fun C => C.filter fun l => l.index == i).length
    27
    28/-- `F` is a *(3,4)* formula: every clause has exactly three literals, and every variable
    29occurs at most four times. -/
    30def IsThreeFour (F : Formula) : Prop :=
    31 (∀ C ∈ F, C.length = 3) ∧ ∀ i, occurrences F i ≤ 4
    32
    33/-- **(3,4)-SAT** as a language: the encodings of satisfiable (3,4) formulas. -/
    34def SAT34 : Language :=
    35 {w | ∃ F : Formula, Lax429075.Encoding.encodeCNF F = w ∧ IsThreeFour F ∧ Satisfiable F}
    36
    37/-- **Theorem 2.3 (Tovey).** (3,4)-SAT is NP-hard. -/
    38axiom npHard :
    39 ∀ A : Language, A ∈ Lax434930.NondeterministicPolynomialTime.NP →
    40 Lax429075.Reductions.ManyOne A SAT34
    41
    42end Lax345332.ThreeFourSat
    43
    Show Proof
    Formalization notes

    The restriction is a predicate on the CNF formulas of the archive's Cook–Levin submission, so the encoding and the notion of satisfiability are shared with unrestricted SAT. Occurrences are counted with multiplicity.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…