Lax Lean Archive

Not-all-equal SAT

Lax799700.NaeSat · concepts/Lax799700/NaeSat.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

    NOT-ALL-EQUAL SAT: is there a truth assignment giving every clause both a true and a false literal? It lives on the vocabulary of SAT, and only its notion of satisfaction differs (NAEProper), which is closed under flipping the assignment. That symmetry is what the hardness proof uses: adding one fresh variable, positive in every clause, turns a satisfying assignment into a not-all-equal one and back, once the fresh variable is normalized to false. The fresh variable is picked out as the minimum of its copy of the universe, so the reduction from SAT is an ordered first-order reduction. Membership is by an existential second-order definition, SAT's kernel conjoined with its mirror image.

    Concept map
    8 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 naeSat_iff proven

    2 naeSat_NP_complete proven

    3 naeSatisfiable_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 Mathlib.Data.Set.Card
    14import Lax904597.Sat
    15import Lax904597.Classes
    16import Lax799700.Problems
    17
    18/-!
    19---
    20title: Not-all-equal SAT
    21type: theorem
    22---
    23NOT-ALL-EQUAL SAT: is there a truth assignment giving every clause both a
    24true and a false literal? It lives on the vocabulary of SAT, and only its
    25notion of satisfaction differs (NAEProper), which is closed under
    26flipping the assignment. That symmetry is what the hardness proof uses:
    27adding one fresh variable, positive in every clause, turns a satisfying
    28assignment into a not-all-equal one and back, once the fresh variable is
    29normalized to false. The fresh variable is picked out as the minimum of
    30its copy of the universe, so the reduction from SAT is an ordered
    31first-order reduction. Membership is by an existential second-order
    32definition, SAT's kernel conjoined with its mirror image.
    33
    34-/
    35
    36namespace Lax799700.NaeSat
    37
    38open Lax904597.Sat
    39
    40open FirstOrder
    41
    42open Language Structure Lax904597.SecondOrder.SOBlock BoundedFormula
    43
    44section Semantics
    45
    46variable {A : Type} [sat.Structure A]
    47
    48/-- An assignment is *not-all-equal proper* when every clause contains both a
    49true and a false literal. -/
    50def NAEProper (ν : A → Prop) : Prop :=
    51 ∀ c : A, RelMap satIsClause ![c] →
    52 (∃ x : A, (RelMap satPosIn ![c, x] ∧ ν x) ∨ (RelMap satNegIn ![c, x] ∧ ¬ν x)) ∧
    53 ∃ x : A, (RelMap satPosIn ![c, x] ∧ ¬ν x) ∨ (RelMap satNegIn ![c, x] ∧ ν x)
    54
    55end Semantics
    56
    57section Problem
    58
    59variable (A : Type) [sat.Structure A]
    60
    61/-- A `Language.sat`-structure is not-all-equal satisfiable if some assignment
    62gives every clause both a true and a false literal. -/
    63def NAESatisfiable : Prop := ∃ ν : A → Prop, NAEProper ν
    64
    65end Problem
    66
    67open Lax904597.Problems Lax904597.Classes Lax799700.Problems
    68
    69/-- The property `NAESatisfiable` is isomorphism-invariant. -/
    70axiom naeSatisfiable_iso : ∀ {A B : Type} [Lax904597.Sat.sat.Structure A] [Lax904597.Sat.sat.Structure B],
    71 (A ≃[Lax904597.Sat.sat] B) → (NAESatisfiable A ↔ NAESatisfiable B)
    72
    73/-- The problem NAESAT: does the structure satisfy `NAESatisfiable`? -/
    74def NAESAT : DecisionProblem Lax904597.Sat.sat :=
    75 DecisionProblem.ofPred NAESatisfiable
    76
    77/-- The yes-instances of NAESAT are exactly the structures satisfying
    78`NAESatisfiable`. -/
    79axiom naeSat_iff : ∀ (A : Type) [Lax904597.Sat.sat.Structure A], NAESAT A ↔ NAESatisfiable A
    80
    81/-- NAESAT is NP-complete. -/
    82axiom naeSat_NP_complete : NP.Complete NAESAT
    83
    84end Lax799700.NaeSat
    85
    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…