SAT, propositional satisfiability
Lax904597.Sat · concepts/Lax904597/Sat.lean · lax-904597
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
A CNF instance is a structure over a vocabulary with a unary symbol and two binary symbols: the elements the unary symbol marks are the clauses, and the binary symbols record that an element occurs positively, or negatively, in a clause. It is satisfiable when some assignment of truth values to the elements makes every clause contain a true literal; elements that are neither clauses nor variables of the formula are harmless, since no clause mentions them. SAT is the decision problem of satisfiability; its isomorphism-invariance, which makes it a decision problem, is proved in place by transporting the assignment.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.ModelTheory.Semantics |
| 2 | import Lax904597.Problems |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: SAT, propositional satisfiability |
| 7 | type: definition |
| 8 | --- |
| 9 | A CNF instance is a structure over a vocabulary with a unary symbol and |
| 10 | two binary symbols: the elements the unary symbol marks are the clauses, |
| 11 | and the binary symbols record that an element occurs positively, or |
| 12 | negatively, in a clause. It is satisfiable when some |
| 13 | assignment of truth values to the elements makes every clause contain a true |
| 14 | literal; elements that are neither clauses nor variables of the formula are |
| 15 | harmless, since no clause mentions them. SAT is the decision problem of |
| 16 | satisfiability; its isomorphism-invariance, which makes it a decision |
| 17 | problem, is proved in place by transporting the assignment. |
| 18 | -/ |
| 19 | |
| 20 | namespace Lax904597.Sat |
| 21 | |
| 22 | open FirstOrder FirstOrder.Language FirstOrder.Language.Structure Lax904597.Problems |
| 23 | |
| 24 | /-- The relation symbols of CNF instances. -/ |
| 25 | inductive satRel : ℕ → Type where |
| 26 | /-- `isClause c`: the element `c` is a clause. -/ |
| 27 | | isClause : satRel 1 |
| 28 | /-- `posIn c x`: the variable `x` occurs positively in the clause `c`. -/ |
| 29 | | posIn : satRel 2 |
| 30 | /-- `negIn c x`: the variable `x` occurs negatively in the clause `c`. -/ |
| 31 | | negIn : satRel 2 |
| 32 | deriving DecidableEq |
| 33 | |
| 34 | /-- The relational language of CNF instances: a unary predicate singling out |
| 35 | clauses, and two binary predicates for positive and negative occurrences of a |
| 36 | variable in a clause. -/ |
| 37 | def sat : Language := |
| 38 | ⟨fun _ => Empty, satRel⟩ |
| 39 | |
| 40 | instance instIsRelationalSat : IsRelational sat := fun _ => (inferInstance : IsEmpty Empty) |
| 41 | |
| 42 | /-- `isClause c`: the element `c` is a clause. -/ |
| 43 | abbrev satIsClause : sat.Relations 1 := .isClause |
| 44 | |
| 45 | /-- `posIn c x`: the variable `x` occurs positively in the clause `c`. -/ |
| 46 | abbrev satPosIn : sat.Relations 2 := .posIn |
| 47 | |
| 48 | /-- `negIn c x`: the variable `x` occurs negatively in the clause `c`. -/ |
| 49 | abbrev satNegIn : sat.Relations 2 := .negIn |
| 50 | |
| 51 | /-- A CNF instance is satisfiable if some assignment of truth values to its |
| 52 | elements makes every clause contain a true literal. -/ |
| 53 | def Satisfiable (A : Type) [sat.Structure A] : Prop := |
| 54 | ∃ ν : A → Prop, ∀ c : A, RelMap satIsClause ![c] → |
| 55 | ∃ x : A, (RelMap satPosIn ![c, x] ∧ ν x) ∨ (RelMap satNegIn ![c, x] ∧ ¬ν x) |
| 56 | |
| 57 | /-- SAT: is the CNF instance satisfiable? Invariance transports the |
| 58 | assignment along the isomorphism, atom by atom. -/ |
| 59 | def SAT : DecisionProblem sat where |
| 60 | Holds := fun A inst => @Satisfiable A inst |
| 61 | iso_invariant := fun {A B} _ _ e => by |
| 62 | have rel₁ : ∀ {A B : Type} [sat.Structure A] [sat.Structure B] (e : A ≃[sat] B) |
| 63 | (r : sat.Relations 1) (a : A), RelMap r ![a] ↔ RelMap r ![e a] := by |
| 64 | intro A B _ _ e r a |
| 65 | have h := StrongHomClass.map_rel e r ![a] |
| 66 | have hv : e ∘ ![a] = ![e a] := funext fun i => Fin.cases rfl (fun j => j.elim0) i |
| 67 | rw [hv] at h |
| 68 | exact h.symm |
| 69 | have rel₂ : ∀ {A B : Type} [sat.Structure A] [sat.Structure B] (e : A ≃[sat] B) |
| 70 | (r : sat.Relations 2) (a b : A), RelMap r ![a, b] ↔ RelMap r ![e a, e b] := by |
| 71 | intro A B _ _ e r a b |
| 72 | have h := StrongHomClass.map_rel e r ![a, b] |
| 73 | have hv : e ∘ ![a, b] = ![e a, e b] := |
| 74 | funext fun i => Fin.cases rfl (fun j => Fin.cases rfl (fun j => j.elim0) j) i |
| 75 | rw [hv] at h |
| 76 | exact h.symm |
| 77 | have fwd : ∀ {A B : Type} [sat.Structure A] [sat.Structure B] (e : A ≃[sat] B), |
| 78 | Satisfiable A → Satisfiable B := by |
| 79 | intro A B _ _ e hA |
| 80 | obtain ⟨ν, hν⟩ := hA |
| 81 | refine ⟨fun b => ν (e.symm b), fun c hc => ?_⟩ |
| 82 | obtain ⟨x, hx⟩ := hν (e.symm c) ((rel₁ e.symm satIsClause c).mp hc) |
| 83 | refine ⟨e x, ?_⟩ |
| 84 | exact hx.elim |
| 85 | (fun hp => Or.inl ⟨by simpa using (rel₂ e satPosIn (e.symm c) x).mp hp.1, |
| 86 | by simpa using hp.2⟩) |
| 87 | (fun hn => Or.inr ⟨by simpa using (rel₂ e satNegIn (e.symm c) x).mp hn.1, |
| 88 | by simpa using hn.2⟩) |
| 89 | exact ⟨fwd e, fwd e.symm⟩ |
| 90 | |
| 91 | end Lax904597.Sat |
| 92 |
Builds on
From Mathlib
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments