The number written by unit propagation

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

definition

Loading review…

Natural Language Statement

Definition

An instance is a CNF instance of the NP core together with a mark on the output variables and a binary relation comparing them. A variable is forced when unit propagation derives it: when it is the positive literal of a clause all of whose negative literals are forced earlier. When the instance is a satisfiable Horn formula and the comparison is a linear order on the output variables, the number written is $\sum 2^{r(x)}$ over the forced output variables $x$ , $r(x)$ being the number of output variables below $x$ ; otherwise it is $0$ .

Concept map

9 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.Order.Lattice.Nat
2	import Mathlib.Data.Fintype.Card
3	import Mathlib.Data.Fintype.Lattice
4	import Mathlib.Data.Set.Card
5	import Mathlib.Tactic.FinCases
6	import Mathlib.Order.PiLex
7	import Mathlib.Data.Prod.Lex
8	import Mathlib.Data.Fintype.EquivFin
9	import Mathlib.ModelTheory.Order
10	import Mathlib.ModelTheory.Semantics
11	import Mathlib.ModelTheory.Complexity
12	import Mathlib.Logic.Equiv.Fin.Basic
13	import Mathlib.Data.Finite.Sigma
14	import Mathlib.ModelTheory.Syntax
15	import Mathlib.Algebra.BigOperators.Finprod
16	import Mathlib.Data.Fintype.Pigeonhole
17	import Mathlib.Dynamics.FixedPoints.Basic
18	import Lax535992.HornSat
19	import Lax904597.Sat
20	import Lax904597.SecondOrder
21	import Lax366625.CountingProblems
22
23	/-!
24	---
25	title: The number written by unit propagation
26	type: definition
27	---
28	An instance is a CNF instance of the NP core together with a mark on the
29	output variables and a binary relation comparing them. A variable is forced
30	when unit propagation derives it: when it is the positive literal of a
31	clause all of whose negative literals are forced earlier. When the instance
32	is a satisfiable Horn formula and the comparison is a linear order on the
33	output variables, the number written is $\sum 2^{r(x)}$ over the forced
34	output variables $x$ , $r(x)$ being the number of output variables below
35	$x$ ; otherwise it is $0$ .
36	-/
37
38	namespace Lax366625.HornNumbers
39
40	open Lax535992.HornSat Lax904597.Sat
41
42	open FirstOrder
43
44	open Language Structure Lax904597.SecondOrder.SOBlock
45
46	section LeastModel
47
48	variable {A : Type} [sat.Structure A]
49
50	/-- The stages of unit propagation: `ForcedIn n x` says that `x` is the
51	positive literal of a clause whose negative literals are all forced in fewer
52	than `n` rounds. -/
53	def ForcedIn : ℕ → A → Prop
54	\| 0, _ => False
55	\| n + 1, x => ∃ c : A, RelMap satIsClause ![c] ∧ RelMap satPosIn ![c, x] ∧
56	∀ y : A, RelMap satNegIn ![c, y] → ForcedIn n y
57
58	/-- A variable is forced when some stage forces it. On a Horn formula this
59	is the least model of the implications. -/
60	def Forced (x : A) : Prop := ∃ n, ForcedIn n x
61
62	end LeastModel
63
64	open FirstOrder
65
66	open FirstOrder.Language
67
68	/-- The relation symbols of the language. -/
69	inductive digitOrderRel : ℕ → Type where
70	/-- `out x`: the element `x` holds one digit. -/
71	\| out : digitOrderRel 1
72	/-- `below y x`: the digit of `y` is at most as significant as the one of
73	`x`. -/
74	\| below : digitOrderRel 2
75	deriving DecidableEq
76
77	/-- The symbols reading a number off a set of marked elements. -/
78	def digitOrder : FirstOrder.Language :=
79	⟨fun _ => Empty, digitOrderRel⟩
80
81	instance instIsRelationalDigitOrder : FirstOrder.Language.IsRelational digitOrder := fun _ =>
82	(inferInstance : IsEmpty Empty)
83
84	/-- `out x`: the element `x` holds one digit. -/
85	abbrev dgoOut : digitOrder.Relations 1 :=
86	.out
87
88	/-- `below y x`: the digit of `y` is at most as significant as the one of
89	`x`. -/
90	abbrev dgoBelow : digitOrder.Relations 2 :=
91	.below
92
93	/-- The relational language of Horn formulas writing a number. -/
94	abbrev satOut : Language.{0, 0} := sat.sum digitOrder
95
96	open FirstOrder
97
98	open Language Structure
99
100	/-- “Is an output variable”. -/
101	abbrev hnOut : satOut.Relations 1 := Sum.inr dgoOut
102
103	/-- The comparison of the output variables. -/
104	abbrev hnBelow : satOut.Relations 2 := Sum.inr dgoBelow
105
106	/-- A Horn formula writing a number is a CNF instance. -/
107	instance satOutStructure (A : Type) [satOut.Structure A] :
108	sat.Structure A :=
109	(LHom.sumInl : sat →ᴸ satOut).reduct A
110
111	section Semantics
112
113	variable {A : Type} [satOut.Structure A]
114
115	/-- The output variable `x` is forced. -/
116	def ForcedDigit (x : A) : Prop :=
117	RelMap hnOut ![x] ∧ Forced x
118
119	/-- `y` is an output variable strictly below `x`. -/
120	def LowerVar (x y : A) : Prop :=
121	RelMap hnOut ![y] ∧ y ≠ x ∧ RelMap hnBelow ![y, x]
122
123	/-- The rank of a variable among the outputs: the number of output variables
124	strictly below it. -/
125	noncomputable def varRank (x : A) : ℕ :=
126	Nat.card {y : A // LowerVar x y}
127
128	variable (A) in
129	/-- The comparison of the outputs is a linear order on them: reflexive,
130	transitive, antisymmetric and total among the output variables. -/
131	def VarOrder : Prop :=
132	(∀ p : A, RelMap hnOut ![p] → RelMap hnBelow ![p, p]) ∧
133	(∀ p q r : A, RelMap hnOut ![p] → RelMap hnOut ![q] → RelMap hnOut ![r] →
134	RelMap hnBelow ![p, q] → RelMap hnBelow ![q, r] → RelMap hnBelow ![p, r]) ∧
135	(∀ p q : A, RelMap hnOut ![p] → RelMap hnOut ![q] →
136	RelMap hnBelow ![p, q] → RelMap hnBelow ![q, p] → p = q) ∧
137	∀ p q : A, RelMap hnOut ![p] → RelMap hnOut ![q] →
138	RelMap hnBelow ![p, q] ∨ RelMap hnBelow ![q, p]
139
140	variable (A) in
141	open Classical in
142	/-- The number written by unit propagation: each forced output variable
143	contributes two to the power of its rank among the outputs. Instances that are
144	not satisfiable Horn formulas, or whose outputs are not linearly ordered,
145	write `0`. -/
146	noncomputable def hornNumber : ℕ :=
147	if HornSatisfiable A ∧ VarOrder A then ∑ᶠ x : A, if ForcedDigit x then 2 ^ varRank x else 0
148	else 0
149
150	end Semantics
151
152	open Lax366625.CountingProblems
153
154	/-- The number written by unit propagation, as a counting problem. -/
155	noncomputable def HornNumber : CountingProblem satOut :=
156	CountingProblem.ofFun fun A _ => hornNumber A
157
158	end Lax366625.HornNumbers
159

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

The number written by unit propagation

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments