#SAT, counting the models of a CNF formula

Lax366625.CountingSat · concepts/Lax366625/CountingSat.lean · lax-366625

definition

Loading review…

Natural Language Statement

Definition

An instance is a CNF instance of the NP core. Its variables are the elements occurring in some clause, and a model is a set of variables such that every clause contains a true literal. #SAT counts the models: its value on an instance is the number of models, the elements that are not variables being always false.

Concept map

6 concepts; 12 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Mathlib.Tactic.FinCases
2	import Mathlib.Order.PiLex
3	import Mathlib.Data.Prod.Lex
4	import Mathlib.Data.Fintype.EquivFin
5	import Mathlib.ModelTheory.Order
6	import Mathlib.ModelTheory.Semantics
7	import Mathlib.ModelTheory.Complexity
8	import Mathlib.Logic.Equiv.Fin.Basic
9	import Mathlib.Data.Finite.Sigma
10	import Mathlib.Data.Fintype.Lattice
11	import Mathlib.ModelTheory.Syntax
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.Algebra.Order.BigOperators.Group.Finset
17	import Mathlib.Data.Fintype.Card
18	import Mathlib.SetTheory.Cardinal.Finite
19	import Lax904597.Sat
20	import Lax366625.CountingProblems
21
22	/-!
23	---
24	title: #SAT, counting the models of a CNF formula
25	type: definition
26	---
27	An instance is a CNF instance of the NP core. Its variables are the elements
28	occurring in some clause, and a model is a set of variables such that every
29	clause contains a true literal. #SAT counts the models: its value on an
30	instance is the number of models, the elements that are not variables being
31	always false.
32	-/
33
34	namespace Lax366625.CountingSat
35
36	open Lax904597.Sat
37
38	open FirstOrder
39
40	open Language Structure
41
42	section Sat
43
44	variable (A : Type) [sat.Structure A]
45
46	/-- The element `x` is a variable of the CNF formula: it occurs, positively or
47	negatively, in some clause. The decision problem does not need the notion –
48	an element in no clause is harmless – but everything that counts assignments
49	does, and so does any reduction that must not give such an element a truth
50	value to choose. -/
51	def SatOccurs (x : A) : Prop :=
52	∃ c : A, RelMap satIsClause ![c] ∧ (RelMap satPosIn ![c, x] ∨ RelMap satNegIn ![c, x])
53
54	end Sat
55
56	open FirstOrder
57
58	open Language Structure
59
60	section Models
61
62	variable (A : Type) [sat.Structure A]
63
64	/-- The set `ν` of true variables is a model of the CNF formula: every clause
65	contains a true literal, and `ν` consists of variables of the formula. -/
66	def SatModel (ν : A → Prop) : Prop :=
67	(∀ c : A, RelMap satIsClause ![c] →
68	∃ x : A, (RelMap satPosIn ![c, x] ∧ ν x) ∨ (RelMap satNegIn ![c, x] ∧ ¬ν x)) ∧
69	∀ x : A, ν x → SatOccurs A x
70
71	end Models
72
73	open Lax366625.CountingProblems
74
75	/-- #SAT: the number of models of a CNF formula. -/
76	noncomputable def SharpSAT : CountingProblem sat :=
77	CountingProblem.ofFun fun A _ => Nat.card {ν : A → Prop // SatModel A ν}
78
79	end Lax366625.CountingSat
80

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

#SAT, counting the models of a CNF formula

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments