Lax Lean Archive

3SAT

Lax799700.ThreeSat · concepts/Lax799700/ThreeSat.lean · lax-799700

proven

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

    3SAT on the vocabulary of SAT: a CNF structure is a yes-instance when every clause has at most three literal occurrences (WidthAtMostThree) and the CNF is satisfiable (ThreeSatisfiable). The width bound is part of the yes-instances rather than of the vocabulary, which is what makes 3SAT a decision problem on arbitrary CNF structures; it is expressed without counting, as “among any four literal occurrences of a clause, two coincide”.

    Membership in NP is by the identity-like first-order reduction to SAT; hardness is the classical clause splitting, an ordered first-order reduction from SAT in which the chain of fresh variables of a clause follows the order on its occurrences.

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

    This concept declares 3 statements. Each proof establishes one of them relative to its assumptions.

    1 threeSat_iff proven

    2 threeSat_NP_complete proven

    3 threeSatisfiable_iso proven

    Lean source view on GitHub

    1import Mathlib.Data.Set.Finite.Lemmas
    2import Mathlib.Tactic.FinCases
    3import Mathlib.Order.PiLex
    4import Mathlib.Data.Prod.Lex
    5import Mathlib.Data.Fintype.EquivFin
    6import Mathlib.ModelTheory.Order
    7import Mathlib.ModelTheory.Semantics
    8import Mathlib.ModelTheory.Complexity
    9import Mathlib.Logic.Equiv.Fin.Basic
    10import Mathlib.Data.Finite.Sigma
    11import Mathlib.Data.Fintype.Lattice
    12import Mathlib.ModelTheory.Syntax
    13import Lax799700.Common
    14import Lax904597.Sat
    15import Lax904597.Classes
    16import Lax799700.Problems
    17
    18/-!
    19---
    20title: 3SAT
    21type: theorem
    22---
    233SAT on the vocabulary of SAT: a CNF structure is a yes-instance when
    24every clause has at most three literal occurrences (WidthAtMostThree) and
    25the CNF is satisfiable (ThreeSatisfiable). The width bound is part of the
    26yes-instances rather than of the vocabulary, which is what makes 3SAT a
    27decision problem on arbitrary CNF structures; it is expressed without
    28counting, as “among any four literal occurrences of a clause, two
    29coincide”.
    30
    31Membership in NP is by the identity-like first-order reduction to SAT;
    32hardness is the classical clause splitting, an ordered first-order
    33reduction from SAT in which the chain of fresh variables of a clause
    34follows the order on its occurrences.
    35
    36-/
    37
    38namespace Lax799700.ThreeSat
    39
    40open Lax799700.Common Lax904597.Sat
    41
    42open FirstOrder
    43
    44open Language Structure
    45
    46section ThreeSat
    47
    48variable (A : Type) [sat.Structure A]
    49
    50/-- Every clause of a `Language.sat`-structure has at most three literal
    51occurrences: among any four occurrences of a clause, two coincide (as signed
    52occurrences). -/
    53def WidthAtMostThree : Prop :=
    54 ∀ (c : A) (x : Fin 4 → A) (s : Fin 4 → Bool),
    55 (∀ i, SatOcc.OccIn c (x i) (s i)) → ∃ i j, i ≠ j ∧ x i = x j ∧ s i = s j
    56
    57/-- A `Language.sat`-structure is a yes-instance of 3SAT if every clause has
    58at most three literal occurrences and the CNF is satisfiable. -/
    59def ThreeSatisfiable : Prop :=
    60 WidthAtMostThree A ∧ Satisfiable A
    61
    62end ThreeSat
    63
    64open Lax904597.Problems Lax904597.Classes Lax799700.Problems
    65
    66/-- The property `ThreeSatisfiable` is isomorphism-invariant. -/
    67axiom threeSatisfiable_iso : ∀ {A B : Type} [Lax904597.Sat.sat.Structure A] [Lax904597.Sat.sat.Structure B],
    68 (A ≃[Lax904597.Sat.sat] B) → (ThreeSatisfiable A ↔ ThreeSatisfiable B)
    69
    70/-- The problem ThreeSAT: does the structure satisfy `ThreeSatisfiable`? -/
    71def ThreeSAT : DecisionProblem Lax904597.Sat.sat :=
    72 DecisionProblem.ofPred ThreeSatisfiable
    73
    74/-- The yes-instances of ThreeSAT are exactly the structures satisfying
    75`ThreeSatisfiable`. -/
    76axiom threeSat_iff : ∀ (A : Type) [Lax904597.Sat.sat.Structure A], ThreeSAT A ↔ ThreeSatisfiable A
    77
    78/-- ThreeSAT is NP-complete. -/
    79axiom threeSat_NP_complete : NP.Complete ThreeSAT
    80
    81end Lax799700.ThreeSat
    82
    Show ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…