Quantified Boolean formulas with a bounded number of alternations

Lax564036.QuantifiedBooleanFormulas · concepts/Lax564036/QuantifiedBooleanFormulas.lean · lax-564036

definition

Loading review…

Natural Language Statement

Definition

An instance with $k$ quantifier blocks is a structure over the vocabulary of CNF instances extended by $k$ unary marks, the $i$ -th marking the variables of the $i$ -th block. A tuple of $k$ truth assignments, one per block, gives a variable the value true when some block marking it assigns it true. The matrix is read conjunctively, every clause containing a true literal, or disjunctively, some term having all its literals true. The assignments are quantified in the order of the blocks with alternating quantifiers, the outermost being existential or universal.

QBF $_k$ is the problem with $k$ alternating blocks starting with an existential one, and QBF $^\forall_k$ the problem starting with a universal one. In both the matrix follows the innermost quantifier: conjunctive when it is existential, disjunctive when it is universal. Each problem is the decision problem of the structures isomorphic to a true instance.

Concept map

3 concepts; 16 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Mathlib.ModelTheory.Semantics
2	import Mathlib.Data.Fin.Tuple.Basic
3	import Lax904597.Problems
4	import Lax485149.Problems
5
6	/-!
7	---
8	title: Quantified Boolean formulas with a bounded number of alternations
9	type: definition
10	---
11	An instance with $k$ quantifier blocks is a structure over the vocabulary
12	of CNF instances extended by $k$ unary marks, the $i$ -th marking the
13	variables of the $i$ -th block. A tuple of $k$ truth assignments, one per
14	block, gives a variable the value true when some block marking it assigns it
15	true. The matrix is read conjunctively, every clause containing a true
16	literal, or disjunctively, some term having all its literals true. The
17	assignments are quantified in the order of the blocks with alternating
18	quantifiers, the outermost being existential or universal.
19
20	QBF $_k$ is the problem with $k$ alternating blocks starting with an
21	existential one, and QBF $^\forall_k$ the problem starting with a universal
22	one. In both the matrix follows the innermost quantifier: conjunctive when
23	it is existential, disjunctive when it is universal. Each problem is the
24	decision problem of the structures isomorphic to a true instance.
25	-/
26
27	namespace Lax564036.QuantifiedBooleanFormulas
28
29	open Lax904597.Problems Lax485149.Problems
30
31	open FirstOrder
32
33	open FirstOrder.Language
34
35	/-- Relation symbols of the language of quantified Boolean formulas with `k`
36	quantifier blocks. -/
37	inductive qbfRel (k : ℕ) : ℕ → Type
38	/-- `isClause c`: the element `c` is a clause (a term, for a disjunctive
39	matrix). -/
40	\| isClause : qbfRel k 1
41	/-- `posIn c x`: the variable `x` occurs positively in the clause `c`. -/
42	\| posIn : qbfRel k 2
43	/-- `negIn c x`: the variable `x` occurs negatively in the clause `c`. -/
44	\| negIn : qbfRel k 2
45	/-- `block i x`: the variable `x` belongs to the `i`-th quantifier block. -/
46	\| block : Fin k → qbfRel k 1
47	deriving DecidableEq
48
49	/-- The relational vocabulary of quantified Boolean formulas with `k`
50	quantifier blocks: that of CNF instances, together with `k` unary predicates
51	marking the variables of each quantifier block. -/
52	def qbf (k : ℕ) : Language :=
53	⟨fun _ => Empty, qbfRel k⟩
54
55	instance instIsRelationalQbf (k : ℕ) : IsRelational (qbf k) :=
56	fun _ => ⟨fun f => Empty.elim f⟩
57
58	variable {k : ℕ}
59
60	/-- The symbol for “is a clause”. -/
61	abbrev qbfIsClause : (qbf k).Relations 1 := .isClause
62
63	/-- The symbol for “occurs positively in”. -/
64	abbrev qbfPosIn : (qbf k).Relations 2 := .posIn
65
66	/-- The symbol for “occurs negatively in”. -/
67	abbrev qbfNegIn : (qbf k).Relations 2 := .negIn
68
69	/-- The symbol marking the variables of the `i`-th quantifier block. -/
70	abbrev qbfBlock (i : Fin k) : (qbf k).Relations 1 := .block i
71
72	open FirstOrder
73
74	open Language Structure
75
76	/-- Alternating quantification over `k` truth assignments on `A`: the
77	assignment of index `0` is quantified outermost, existentially if `pol` is
78	`true`, and the polarities alternate inwards. -/
79	def altQuant (A : Type) : ∀ (k : ℕ), ((Fin k → A → Prop) → Prop) → Bool → Prop
80	\| 0, P, _ => P Fin.elim0
81	\| k + 1, P, true => ∃ ν : A → Prop, altQuant A k (fun νs => P (Fin.cons ν νs)) false
82	\| k + 1, P, false => ∀ ν : A → Prop, altQuant A k (fun νs => P (Fin.cons ν νs)) true
83
84	section Matrix
85
86	variable {k : ℕ} {A : Type} [(qbf k).Structure A]
87
88	/-- The truth value of the variable `x` under a tuple of block assignments:
89	`x` is true when some block marking it assigns it the value true. (In a
90	well-formed instance the block marks partition the variables, so exactly one
91	assignment is consulted.) -/
92	def qbfVal (νs : Fin k → A → Prop) (x : A) : Prop :=
93	∃ i : Fin k, RelMap (qbfBlock i) ![x] ∧ νs i x
94
95	/-- Conjunctive satisfaction, with the sign of every literal flipped when
96	`swap` is `true`: every clause then has to contain a literal that the block
97	assignments make false. -/
98	def CnfSatWith (swap : Bool) (νs : Fin k → A → Prop) : Prop :=
99	∀ c : A, RelMap (qbfIsClause (k := k)) ![c] →
100	∃ x : A,
101	(RelMap (if swap then qbfNegIn (k := k) else qbfPosIn (k := k)) ![c, x] ∧ qbfVal νs x) ∨
102	(RelMap (if swap then qbfPosIn (k := k) else qbfNegIn (k := k)) ![c, x] ∧ ¬qbfVal νs x)
103
104	/-- The conjunctive matrix: every clause contains a literal made true by the
105	block assignments. -/
106	abbrev CnfSat (νs : Fin k → A → Prop) : Prop := CnfSatWith false νs
107
108	/-- The disjunctive matrix: some term has all of its literals made true by the
109	block assignments. -/
110	def DnfSat (νs : Fin k → A → Prop) : Prop :=
111	∃ c : A, RelMap (qbfIsClause (k := k)) ![c] ∧
112	∀ x : A, (RelMap (qbfPosIn (k := k)) ![c, x] → qbfVal νs x) ∧
113	(RelMap (qbfNegIn (k := k)) ![c, x] → ¬qbfVal νs x)
114
115	/-- The matrix of a quantified Boolean formula: conjunctive when `cnf` is
116	`true`, disjunctive when it is `false`. -/
117	def QbfMatrix (cnf : Bool) (νs : Fin k → A → Prop) : Prop :=
118	match cnf with
119	\| true => CnfSat νs
120	\| false => DnfSat νs
121
122	end Matrix
123
124	/-- Quantified Boolean formulas with `k` alternating quantifier blocks: the
125	prefix starts with an existential block when `start` is `true`, and the matrix
126	is conjunctive when `cnf` is `true`. -/
127	def QbfProblem (k : ℕ) (start cnf : Bool) : DecisionProblem (qbf k) :=
128	DecisionProblem.ofPred fun A _ => altQuant A k (fun νs => QbfMatrix cnf νs) start
129
130	/-- QBF with `k` alternating blocks, existential first: the matrix is
131	conjunctive when the innermost quantifier is existential (`k` odd), disjunctive
132	when it is universal (`k` even). -/
133	def QBF (k : ℕ) : DecisionProblem (qbf k) :=
134	QbfProblem k true (k % 2 == 1)
135
136	/-- The dual family, with a universal outermost block. -/
137	def QBFPi (k : ℕ) : DecisionProblem (qbf k) :=
138	QbfProblem k false (k % 2 == 0)
139
140	end Lax564036.QuantifiedBooleanFormulas
141

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

Quantified Boolean formulas with a bounded number of alternations

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments