Lax Lean Archive

1-in-SAT

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

    EXACTLY-ONE SATISFIABILITY: is there a truth assignment giving every clause exactly one true literal? It lives on the vocabulary of SAT with its own notion of satisfaction (OneInProper). Membership is by an existential second-order definition, SAT's kernel plus uniqueness, one clause per pattern of signs; hardness is an ordered first-order reduction from 3SAT. The catalog states it at unrestricted width because it is the source for Exact Cover, where a 1-in-SAT instance becomes an exact cover with no gadget at all.

    Concept map
    9 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.

    1 oneInSat_iff proven

    2 oneInSat_NP_complete proven

    3 oneInSatisfiable_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: 1-in-SAT
    21type: theorem
    22---
    23EXACTLY-ONE SATISFIABILITY: is there a truth assignment giving every
    24clause exactly one true literal? It lives on the vocabulary of SAT with
    25its own notion of satisfaction (OneInProper). Membership is by an
    26existential second-order definition, SAT's kernel plus uniqueness, one
    27clause per pattern of signs; hardness is an ordered first-order reduction
    28from 3SAT. The catalog states it at unrestricted width because it is the
    29source for Exact Cover, where a 1-in-SAT instance becomes an exact cover
    30with no gadget at all.
    31
    32-/
    33
    34namespace Lax799700.OneInSat
    35
    36open Lax799700.Common Lax904597.Sat
    37
    38open FirstOrder
    39
    40open Language Structure Lax904597.SecondOrder.SOBlock
    41
    42section Semantics
    43
    44variable {A : Type} [sat.Structure A]
    45
    46/-- An assignment is *exactly-one proper* when every clause has exactly one
    47true literal occurrence. -/
    48def OneInProper (ν : A → Prop) : Prop :=
    49 ∀ c : A, SatOcc.IsCl c → ∃ x s, SatOcc.OccIn c x s ∧ SatOcc.LitTrue ν x s ∧
    50 ∀ y t, SatOcc.OccIn c y t → SatOcc.LitTrue ν y t → y = x ∧ t = s
    51
    52end Semantics
    53
    54section Problem
    55
    56variable (A : Type) [sat.Structure A]
    57
    58/-- A `Language.sat`-structure is exactly-one satisfiable if some assignment
    59gives every clause exactly one true literal. -/
    60def OneInSatisfiable : Prop := ∃ ν : A → Prop, OneInProper ν
    61
    62end Problem
    63
    64open Lax904597.Problems Lax904597.Classes Lax799700.Problems
    65
    66/-- The property `OneInSatisfiable` is isomorphism-invariant. -/
    67axiom oneInSatisfiable_iso : ∀ {A B : Type} [Lax904597.Sat.sat.Structure A] [Lax904597.Sat.sat.Structure B],
    68 (A ≃[Lax904597.Sat.sat] B) → (OneInSatisfiable A ↔ OneInSatisfiable B)
    69
    70/-- The problem OneInSAT: does the structure satisfy `OneInSatisfiable`? -/
    71def OneInSAT : DecisionProblem Lax904597.Sat.sat :=
    72 DecisionProblem.ofPred OneInSatisfiable
    73
    74/-- The yes-instances of OneInSAT are exactly the structures satisfying
    75`OneInSatisfiable`. -/
    76axiom oneInSat_iff : ∀ (A : Type) [Lax904597.Sat.sat.Structure A], OneInSAT A ↔ OneInSatisfiable A
    77
    78/-- OneInSAT is NP-complete. -/
    79axiom oneInSat_NP_complete : NP.Complete OneInSAT
    80
    81end Lax799700.OneInSat
    82
    Show ProofShow ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    Discussion

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

    Loading discussion…