Satisfiability decided by counting models

Lax175070.SelectedSat · concepts/Lax175070/SelectedSat.lean · lax-175070

definition

Loading review…

Natural Language Statement

Definition

⊕SAT asks whether a CNF instance of the NP core has an odd number of models, and Mod $_k$ -SAT whether that number is not a multiple of $k$ .

An instance with a selected variable is a CNF instance together with a mark on its variables. #SelSAT $_b$ counts the models in which every selected variable has the value $b$ . SelMajSAT asks whether the selected variable is true in more models than it is false, and SelEqSAT whether it is true in exactly as many models as it is false.

Concept map

13 concepts; 6 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Mathlib.Data.Fintype.Lattice
2	import Mathlib.ModelTheory.Order
3	import Mathlib.ModelTheory.Semantics
4	import Mathlib.ModelTheory.Complexity
5	import Mathlib.Tactic.FinCases
6	import Mathlib.SetTheory.Cardinal.Finite
7	import Mathlib.Order.PiLex
8	import Mathlib.Data.Prod.Lex
9	import Mathlib.Data.Fintype.EquivFin
10	import Mathlib.Logic.Equiv.Fin.Basic
11	import Mathlib.Data.Finite.Sigma
12	import Mathlib.Order.Lattice.Nat
13	import Mathlib.Data.Set.Card
14	import Mathlib.Data.Fintype.Pigeonhole
15	import Mathlib.Dynamics.FixedPoints.Basic
16	import Mathlib.ModelTheory.Syntax
17	import Mathlib.Algebra.Order.BigOperators.Group.Finset
18	import Mathlib.Data.Fintype.Card
19	import Mathlib.Data.Set.Finite.Lemmas
20	import Mathlib.Algebra.BigOperators.Finprod
21	import Mathlib.Logic.Equiv.Prod
22	import Lax366625.CountingSat
23	import Lax904597.Sat
24	import Lax485149.Problems
25	import Lax366625.CountingProblems
26	import Lax175070.CountDefinability
27
28	/-!
29	---
30	title: Satisfiability decided by counting models
31	type: definition
32	---
33	⊕SAT asks whether a CNF instance of the NP core has an odd number of models,
34	and Mod $_k$ -SAT whether that number is not a multiple of $k$ .
35
36	An instance with a selected variable is a CNF instance together with a mark
37	on its variables. #SelSAT $_b$ counts the models in which every selected
38	variable has the value $b$ . SelMajSAT asks whether the selected variable is
39	true in more models than it is false, and SelEqSAT whether it is true in
40	exactly as many models as it is false.
41	-/
42
43	namespace Lax175070.SelectedSat
44
45	open Lax366625.CountingSat Lax904597.Sat
46
47	open FirstOrder
48
49	open FirstOrder.Language
50
51	/-- The relation symbols of the language. -/
52	inductive selMarkRel : ℕ → Type where
53	/-- `sel x`: the variable `x` is selected. -/
54	\| sel : selMarkRel 1
55	deriving DecidableEq
56
57	/-- The symbol selecting a variable. -/
58	def selMark : FirstOrder.Language :=
59	⟨fun _ => Empty, selMarkRel⟩
60
61	instance instIsRelationalSelMark : FirstOrder.Language.IsRelational selMark := fun _ =>
62	(inferInstance : IsEmpty Empty)
63
64	/-- `sel x`: the variable `x` is selected. -/
65	abbrev smSel : selMark.Relations 1 :=
66	.sel
67
68	/-- The relational language of CNF formulas with a selected variable. -/
69	abbrev satSel : Language.{0, 0} := sat.sum selMark
70
71	open FirstOrder
72
73	open Language Structure
74
75	/-- “Is selected”, in the vocabulary of CNF formulas with a selected
76	variable. -/
77	abbrev ssSel : satSel.Relations 1 := Sum.inr smSel
78
79	/-- A CNF formula with a selected variable is a CNF formula. -/
80	instance satSelStructure (A : Type) [satSel.Structure A] :
81	sat.Structure A :=
82	(LHom.sumInl : sat →ᴸ satSel).reduct A
83
84	section Counts
85
86	variable (A : Type) [satSel.Structure A]
87
88	/-- A model of the formula in which every selected variable has the value
89	`b`. -/
90	def SelModel (b : Bool) (ν : A → Prop) : Prop :=
91	SatModel A ν ∧ ∀ x : A, RelMap ssSel ![x] → (ν x ↔ b = true)
92
93	end Counts
94
95	open Lax904597.Problems Lax485149.Problems Lax366625.CountingProblems Lax175070.CountDefinability
96
97	/-- ⊕SAT: the number of models of a CNF formula is odd. -/
98	noncomputable def ParitySAT : DecisionProblem sat :=
99	decide Odd SharpSAT
100
101	/-- Mod_k-SAT: the number of models of a CNF formula is not a multiple of
102	`k`. -/
103	noncomputable def ModSAT (k : ℕ) : DecisionProblem sat :=
104	decide (fun c => ¬ k ∣ c) SharpSAT
105
106	/-- #SelSAT: the number of models in which every selected variable has the
107	value `b`. -/
108	noncomputable def SharpSelSAT (b : Bool) : CountingProblem satSel :=
109	CountingProblem.ofFun fun A _ => Nat.card {ν : A → Prop // SelModel A b ν}
110
111	/-- SelMajSAT: the selected variable is true in more models than it is
112	false. -/
113	noncomputable def SelMajSAT : DecisionProblem satSel :=
114	DecisionProblem.ofPred fun A _ => SharpSelSAT false A < SharpSelSAT true A
115
116	/-- SelEqSAT: the selected variable is true in exactly as many models as it
117	is false. -/
118	noncomputable def SelEqSAT : DecisionProblem satSel :=
119	DecisionProblem.ofPred fun A _ => SharpSelSAT true A = SharpSelSAT false A
120
121	end Lax175070.SelectedSat
122

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…

Lax Lean Archive

Satisfiability decided by counting models

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments