Counting the models of 3-CNF and 1-in-CNF formulas

Lax280166.CountingSatVariants · concepts/Lax280166/CountingSatVariants.lean · lax-280166

definition

Loading review…

Natural Language Statement

Definition

The instances are the CNF instances of the NP core. #3SAT counts the models of an instance whose clauses have at most three literals each, and is $0$ on the others. #1-in-SAT counts the 1-in-models: the sets of variables such that every clause contains exactly one true literal.

Concept map

13 concepts; 25 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.Fintype.Lattice
10	import Mathlib.Data.Finite.Sigma
11	import Mathlib.Order.Lattice.Nat
12	import Mathlib.Data.Set.Card
13	import Mathlib.Data.Fintype.Pigeonhole
14	import Mathlib.Dynamics.FixedPoints.Basic
15	import Mathlib.ModelTheory.Syntax
16	import Mathlib.Algebra.Order.BigOperators.Group.Finset
17	import Mathlib.Data.Fintype.Card
18	import Mathlib.SetTheory.Cardinal.Finite
19	import Mathlib.Data.Set.Finite.Lemmas
20	import Lax366625.CountingSat
21	import Lax799700.OneInSat
22	import Lax904597.Sat
23	import Mathlib.SetTheory.Cardinal.Finite
24	import Lax366625.CountingProblems
25	import Lax366625.CountingSat
26	import Lax799700.ThreeSat
27
28	/-!
29	---
30	title: Counting the models of 3-CNF and 1-in-CNF formulas
31	type: definition
32	---
33	The instances are the CNF instances of the NP core. #3SAT counts the models
34	of an instance whose clauses have at most three literals each, and is $0$ on
35	the others. #1-in-SAT counts the 1-in-models: the sets of variables such
36	that every clause contains exactly one true literal.
37	-/
38
39	namespace Lax280166.CountingSatVariants
40
41	open Lax366625.CountingSat Lax799700.OneInSat Lax904597.Sat
42
43	open FirstOrder
44
45	open Language Structure
46
47	/-- The set `ν` of true variables is an exactly-one model of the CNF formula:
48	every clause has exactly one true literal, and `ν` consists of variables of
49	the formula. -/
50	def OneInModel (A : Type) [sat.Structure A] (ν : A → Prop) : Prop :=
51	OneInProper ν ∧ ∀ x : A, ν x → SatOccurs A x
52
53	open Lax366625.CountingProblems Lax366625.CountingSat Lax799700.ThreeSat
54
55	/-- #3SAT, as a counting problem. -/
56	noncomputable def SharpThreeSAT : CountingProblem Lax904597.Sat.sat :=
57	CountingProblem.ofFun fun A _ =>
58	Nat.card {ν : A → Prop // WidthAtMostThree A ∧ SatModel A ν}
59
60	/-- #1-in-SAT, as a counting problem. -/
61	noncomputable def SharpOneInSAT : CountingProblem Lax904597.Sat.sat :=
62	CountingProblem.ofFun fun A _ =>
63	Nat.card {ν : A → Prop // OneInModel A ν}
64
65	end Lax280166.CountingSatVariants
66

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

Counting the models of 3-CNF and 1-in-CNF formulas

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments