Not-all-equal 3SAT

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

proven

Loading review…

Sign in with ORCID

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

    NAE-3SAT is the width-three restriction of NAE-SAT: a CNF structure is a yes-instance when every clause has at most three literal occurrences, the promise 3SAT uses, and some assignment gives every clause both a true and a false literal. Both reductions are the interpretations of the SAT and 3SAT pair applied unchanged: membership through the identity-like reduction to NAE-SAT, hardness through the clause-splitting ordered reduction from NAE-SAT, whose chain of pieces also works for the not-all-equal reading. Its value in the catalog is as a reduction source, for Max Cut and for job sequencing.

    Concept map
    11 concepts
    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.

    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 Lax799700.NaeSat
    15import Lax799700.ThreeSat
    16import Lax904597.Sat
    17import Lax904597.Classes
    18import Lax799700.Problems
    19
    20/-!
    21---
    22title: Not-all-equal 3SAT
    23type: theorem
    24---
    25NAE-3SAT is the width-three restriction of NAE-SAT: a CNF structure is a
    26yes-instance when every clause has at most three literal occurrences, the
    27promise 3SAT uses, and some assignment gives every clause both a true and
    28a false literal. Both reductions are the interpretations of the SAT and
    293SAT pair applied unchanged: membership through the identity-like
    30reduction to NAE-SAT, hardness through the clause-splitting ordered
    31reduction from NAE-SAT, whose chain of pieces also works for the
    32not-all-equal reading. Its value in the catalog is as a reduction source,
    33for Max Cut and for job sequencing.
    34
    35-/
    36
    37namespace Lax799700.NaeThreeSat
    38
    39open Lax799700.NaeSat Lax799700.ThreeSat Lax904597.Sat
    40
    41open FirstOrder
    42
    43open Language Structure
    44
    45section Problem
    46
    47variable (A : Type) [sat.Structure A]
    48
    49/-- A `Language.sat`-structure is a yes-instance of NAE-3SAT if every clause
    50has at most three literal occurrences and some assignment gives every clause
    51both a true and a false literal. -/
    52def NAEThreeSatisfiable : Prop :=
    53 WidthAtMostThree A ∧ NAESatisfiable A
    54
    55end Problem
    56
    57open Lax904597.Problems Lax904597.Classes Lax799700.Problems
    58
    59/-- The property `NAEThreeSatisfiable` is isomorphism-invariant. -/
    60axiom naeThreeSatisfiable_iso : ∀ {A B : Type} [Lax904597.Sat.sat.Structure A] [Lax904597.Sat.sat.Structure B],
    61 (A ≃[Lax904597.Sat.sat] B) → (NAEThreeSatisfiable A ↔ NAEThreeSatisfiable B)
    62
    63/-- The problem NAE3SAT: does the structure satisfy `NAEThreeSatisfiable`? -/
    64def NAE3SAT : DecisionProblem Lax904597.Sat.sat :=
    65 DecisionProblem.ofPred NAEThreeSatisfiable
    66
    67/-- The yes-instances of NAE3SAT are exactly the structures satisfying
    68`NAEThreeSatisfiable`. -/
    69axiom nae3Sat_iff : ∀ (A : Type) [Lax904597.Sat.sat.Structure A], NAE3SAT A ↔ NAEThreeSatisfiable A
    70
    71/-- NAE3SAT is NP-complete. -/
    72axiom nae3Sat_NP_complete : NP.Complete NAE3SAT
    73
    74end Lax799700.NaeThreeSat
    75
    Show ProofShow ProofShow Proof

    Discussion

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

    Loading discussion…