#2SAT, #HORN-SAT, and #Monotone-2SAT

Lax859101.CountingRestrictedSat · concepts/Lax859101/CountingRestrictedSat.lean · lax-859101

definition

Loading review…

Natural Language Statement

Definition

The restricted versions of #SAT count the models of a CNF instance in a class of formulas, and are $0$ on the other instances: #2SAT on the formulas with at most two literals per clause, #HORN-SAT on the formulas with at most one positive literal per clause, and #Monotone-2SAT on the formulas with at most two literals per clause and no negative literal.

Concept map

11 concepts; 13 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.Data.Set.Finite.Lemmas
13	import Mathlib.ModelTheory.Graph
14	import Mathlib.SetTheory.Cardinal.Finite
15	import Mathlib.Order.Lattice.Nat
16	import Mathlib.Data.Set.Card
17	import Mathlib.Data.Fintype.Pigeonhole
18	import Mathlib.Dynamics.FixedPoints.Basic
19	import Mathlib.Algebra.Order.BigOperators.Group.Finset
20	import Mathlib.Data.Fintype.Card
21	import Mathlib.Algebra.BigOperators.Ring.Finset
22	import Mathlib.Data.Fintype.BigOperators
23	import Mathlib.Algebra.Group.Action.Defs
24	import Mathlib.Tactic.Ring
25	import Mathlib.Logic.Equiv.Prod
26	import Mathlib.Data.Fintype.Sort
27	import Mathlib.Order.Hom.Set
28	import Lax799700.Common
29	import Lax904597.Sat
30	import Lax366625.CountingProblems
31	import Lax366625.CountingSat
32
33	/-!
34	---
35	title: #2SAT, #HORN-SAT, and #Monotone-2SAT
36	type: definition
37	---
38	The restricted versions of #SAT count the models of a CNF instance in a
39	class of formulas, and are $0$ on the other instances: #2SAT on the formulas
40	with at most two literals per clause, #HORN-SAT on the formulas with at most
41	one positive literal per clause, and #Monotone-2SAT on the formulas with at
42	most two literals per clause and no negative literal.
43	-/
44
45	namespace Lax859101.CountingRestrictedSat
46
47	open Lax799700.Common Lax904597.Sat
48
49	open FirstOrder
50
51	open Language Structure
52
53	section HornSat
54
55	variable (A : Type) [sat.Structure A]
56
57	/-- Every clause of a `Language.sat`-structure has at most one positive
58	literal: any two variables occurring positively in the same clause coincide. -/
59	def AtMostOnePositive : Prop :=
60	∀ c x y : A, RelMap satIsClause ![c] → RelMap satPosIn ![c, x] →
61	RelMap satPosIn ![c, y] → x = y
62
63	end HornSat
64
65	open FirstOrder
66
67	open Language Structure
68
69	section TwoSat
70
71	variable (A : Type) [sat.Structure A]
72
73	/-- Every clause of a `Language.sat`-structure has at most two literal
74	occurrences: among any three occurrences of a clause, two coincide (as signed
75	occurrences). -/
76	def WidthAtMostTwo : Prop :=
77	∀ (c : A) (x : Fin 3 → A) (s : Fin 3 → Bool),
78	(∀ i, SatOcc.OccIn c (x i) (s i)) → ∃ i j, i ≠ j ∧ x i = x j ∧ s i = s j
79
80	end TwoSat
81
82	open FirstOrder
83
84	open Language Structure
85
86	section Sentences
87
88	variable {α : Type}
89
90	variable {A : Type} [sat.Structure A]
91
92	/-- No clause has a negative literal. -/
93	def NoNegative (A : Type) [sat.Structure A] : Prop :=
94	∀ c x : A, RelMap satIsClause ![c] → ¬RelMap satNegIn ![c, x]
95
96	end Sentences
97
98	open Lax366625.CountingProblems Lax366625.CountingSat
99
100	/-- #2SAT, as a counting problem. -/
101	noncomputable def SharpTwoSAT : CountingProblem Lax904597.Sat.sat :=
102	CountingProblem.ofFun fun A _ =>
103	Nat.card {ν : A → Prop // WidthAtMostTwo A ∧ SatModel A ν}
104
105	/-- #HORN-SAT, as a counting problem. -/
106	noncomputable def SharpHornSAT : CountingProblem Lax904597.Sat.sat :=
107	CountingProblem.ofFun fun A _ =>
108	Nat.card {ν : A → Prop // AtMostOnePositive A ∧ SatModel A ν}
109
110	/-- #Monotone-2SAT, as a counting problem. -/
111	noncomputable def SharpMonotoneTwoSAT : CountingProblem Lax904597.Sat.sat :=
112	CountingProblem.ofFun fun A _ =>
113	Nat.card {ν : A → Prop // (WidthAtMostTwo A ∧ NoNegative A) ∧ SatModel A ν}
114
115	end Lax859101.CountingRestrictedSat
116

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

#2SAT, #HORN-SAT, and #Monotone-2SAT

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments