Lax Lean Archive

SAT-UNSAT

Lax564036.SatUnsat · concepts/Lax564036/SatUnsat.lean · lax-564036

definition

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

    Definition

    An instance is a pair of CNF formulas on one universe: a structure with two copies of the vocabulary of CNF instances, one for each formula. It is a yes-instance of SAT-UNSAT when the first formula is satisfiable and the second is not. SAT-UNSAT is the decision problem of the structures isomorphic to such an instance.

    Concept map
    3 concepts; 16 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.ModelTheory.Semantics
    2import Lax904597.Problems
    3import Lax485149.Problems
    4
    5/-!
    6---
    7title: SAT-UNSAT
    8type: definition
    9---
    10An instance is a pair of CNF formulas on one universe: a structure with two
    11copies of the vocabulary of CNF instances, one for each formula. It is a
    12yes-instance of SAT-UNSAT when the first formula is satisfiable and the
    13second is not. SAT-UNSAT is the decision problem of the structures
    14isomorphic to such an instance.
    15-/
    16
    17namespace Lax564036.SatUnsat
    18
    19open Lax904597.Problems Lax485149.Problems
    20
    21open FirstOrder
    22
    23open FirstOrder.Language
    24
    25/-- Relation symbols of the language of *pairs* of CNF instances: two copies of
    26the symbols of CNF instances, one per side. -/
    27inductive satPairRel : ℕ → Type
    28 /-- `isClause₁ c`: `c` is a clause of the first formula. -/
    29 | isClause₁ : satPairRel 1
    30 /-- `posIn₁ c x`: `x` occurs positively in the first formula's clause `c`. -/
    31 | posIn₁ : satPairRel 2
    32 /-- `negIn₁ c x`: `x` occurs negatively in the first formula's clause `c`. -/
    33 | negIn₁ : satPairRel 2
    34 /-- `isClause₂ c`: `c` is a clause of the second formula. -/
    35 | isClause₂ : satPairRel 1
    36 /-- `posIn₂ c x`: `x` occurs positively in the second formula's clause `c`. -/
    37 | posIn₂ : satPairRel 2
    38 /-- `negIn₂ c x`: `x` occurs negatively in the second formula's clause `c`. -/
    39 | negIn₂ : satPairRel 2
    40 deriving DecidableEq
    41
    42/-- The relational vocabulary of pairs of CNF instances. -/
    43def satPair : Language :=
    44 ⟨fun _ => Empty, satPairRel⟩
    45
    46instance instIsRelationalSatPair : IsRelational satPair := fun _ =>
    47 (inferInstance : IsEmpty Empty)
    48
    49/-- “Is a clause of the first formula”. -/
    50abbrev spIsCl₁ : satPair.Relations 1 := .isClause₁
    51
    52/-- “Occurs positively in”, first formula. -/
    53abbrev spPos₁ : satPair.Relations 2 := .posIn₁
    54
    55/-- “Occurs negatively in”, first formula. -/
    56abbrev spNeg₁ : satPair.Relations 2 := .negIn₁
    57
    58/-- “Is a clause of the second formula”. -/
    59abbrev spIsCl₂ : satPair.Relations 1 := .isClause₂
    60
    61/-- “Occurs positively in”, second formula. -/
    62abbrev spPos₂ : satPair.Relations 2 := .posIn₂
    63
    64/-- “Occurs negatively in”, second formula. -/
    65abbrev spNeg₂ : satPair.Relations 2 := .negIn₂
    66
    67open FirstOrder
    68
    69open Language Structure
    70
    71section Defs
    72
    73variable (A : Type) [satPair.Structure A]
    74
    75/-- Satisfiability of the side of the instance read by the given triple of
    76symbols: some assignment of truth values makes every clause of that side
    77contain a true literal. Both sides of SAT-UNSAT are instances of this. -/
    78def SatWith (isCl : satPair.Relations 1)
    79 (pos neg : satPair.Relations 2) : Prop :=
    80 ∃ ν : A → Prop, ∀ c : A, RelMap isCl ![c] →
    81 ∃ x : A, (RelMap pos ![c, x] ∧ ν x) ∨ (RelMap neg ![c, x] ∧ ¬ν x)
    82
    83end Defs
    84
    85/-- SAT-UNSAT: the first formula of the pair is satisfiable and the second is
    86not. -/
    87def SATUNSAT : DecisionProblem satPair :=
    88 DecisionProblem.ofPred fun A _ =>
    89 SatWith A spIsCl₁ spPos₁ spNeg₁ ∧ ¬SatWith A spIsCl₂ spPos₂ spNeg₂
    90
    91end Lax564036.SatUnsat
    92
    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…