Not-all-equal 3SAT
Lax799700.NaeThreeSat · concepts/Lax799700/NaeThreeSat.lean · lax-799700
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural 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
Evidence
Lean source view on GitHub
| 1 | import Mathlib.Data.Set.Finite.Lemmas |
| 2 | import Mathlib.Tactic.FinCases |
| 3 | import Mathlib.Order.PiLex |
| 4 | import Mathlib.Data.Prod.Lex |
| 5 | import Mathlib.Data.Fintype.EquivFin |
| 6 | import Mathlib.ModelTheory.Order |
| 7 | import Mathlib.ModelTheory.Semantics |
| 8 | import Mathlib.ModelTheory.Complexity |
| 9 | import Mathlib.Logic.Equiv.Fin.Basic |
| 10 | import Mathlib.Data.Finite.Sigma |
| 11 | import Mathlib.Data.Fintype.Lattice |
| 12 | import Mathlib.ModelTheory.Syntax |
| 13 | import Mathlib.Data.Set.Card |
| 14 | import Lax799700.NaeSat |
| 15 | import Lax799700.ThreeSat |
| 16 | import Lax904597.Sat |
| 17 | import Lax904597.Classes |
| 18 | import Lax799700.Problems |
| 19 | |
| 20 | /-! |
| 21 | --- |
| 22 | title: Not-all-equal 3SAT |
| 23 | type: theorem |
| 24 | --- |
| 25 | NAE-3SAT is the width-three restriction of NAE-SAT: a CNF structure is a |
| 26 | yes-instance when every clause has at most three literal occurrences, the |
| 27 | promise 3SAT uses, and some assignment gives every clause both a true and |
| 28 | a false literal. Both reductions are the interpretations of the SAT and |
| 29 | 3SAT pair applied unchanged: membership through the identity-like |
| 30 | reduction to NAE-SAT, hardness through the clause-splitting ordered |
| 31 | reduction from NAE-SAT, whose chain of pieces also works for the |
| 32 | not-all-equal reading. Its value in the catalog is as a reduction source, |
| 33 | for Max Cut and for job sequencing. |
| 34 | |
| 35 | -/ |
| 36 | |
| 37 | namespace Lax799700.NaeThreeSat |
| 38 | |
| 39 | open Lax799700.NaeSat Lax799700.ThreeSat Lax904597.Sat |
| 40 | |
| 41 | open FirstOrder |
| 42 | |
| 43 | open Language Structure |
| 44 | |
| 45 | section Problem |
| 46 | |
| 47 | variable (A : Type) [sat.Structure A] |
| 48 | |
| 49 | /-- A `Language.sat`-structure is a yes-instance of NAE-3SAT if every clause |
| 50 | has at most three literal occurrences and some assignment gives every clause |
| 51 | both a true and a false literal. -/ |
| 52 | def NAEThreeSatisfiable : Prop := |
| 53 | WidthAtMostThree A ∧ NAESatisfiable A |
| 54 | |
| 55 | end Problem |
| 56 | |
| 57 | open Lax904597.Problems Lax904597.Classes Lax799700.Problems |
| 58 | |
| 59 | /-- The property `NAEThreeSatisfiable` is isomorphism-invariant. -/ |
| 60 | axiom 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`? -/ |
| 64 | def NAE3SAT : DecisionProblem Lax904597.Sat.sat := |
| 65 | DecisionProblem.ofPred NAEThreeSatisfiable |
| 66 | |
| 67 | /-- The yes-instances of NAE3SAT are exactly the structures satisfying |
| 68 | `NAEThreeSatisfiable`. -/ |
| 69 | axiom nae3Sat_iff : ∀ (A : Type) [Lax904597.Sat.sat.Structure A], NAE3SAT A ↔ NAEThreeSatisfiable A |
| 70 | |
| 71 | /-- NAE3SAT is NP-complete. -/ |
| 72 | axiom nae3Sat_NP_complete : NP.Complete NAE3SAT |
| 73 | |
| 74 | end Lax799700.NaeThreeSat |
| 75 |
Used by
none
From Mathlib
Mathlib.Data.Finite.SigmaMathlib.Data.Fintype.EquivFinMathlib.Data.Fintype.LatticeMathlib.Data.Prod.LexMathlib.Data.Set.CardMathlib.Data.Set.Finite.LemmasMathlib.Logic.Equiv.Fin.BasicMathlib.ModelTheory.ComplexityMathlib.ModelTheory.OrderMathlib.ModelTheory.SemanticsMathlib.ModelTheory.SyntaxMathlib.Order.PiLexMathlib.Tactic.FinCases
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments