QSAT, quantified Boolean formulas
Lax134656.Qsat · concepts/Lax134656/Qsat.lean · lax-134656
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
An instance is a fully quantified Boolean formula given as a structure: its elements are variables and clauses, with the positive and negative occurrences of variables in clauses as for CNF instances, a mark on the quantified variables, a mark on those quantified universally, and a binary relation ordering the variables as they appear in the quantifier prefix, outermost first. The instance is well formed when that relation is a strict linear order on the quantified variables. The matrix holds under a valuation when every clause contains a true literal on a quantified variable.
Truth is defined as a game on positions made of the set of variables already quantified and a valuation: a position is won when every variable is quantified and the matrix holds, when the next variable of the prefix is existential and one of its two values leads to a won position, or when it is universal and both values do. An instance is a yes-instance of QSAT when it is well formed and the initial position is won; QSAT is the decision problem of the structures isomorphic to such an instance. The number of alternations is not bounded.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.ModelTheory.Semantics |
| 2 | import Lax904597.Problems |
| 3 | import Lax485149.Problems |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: QSAT, quantified Boolean formulas |
| 8 | type: definition |
| 9 | --- |
| 10 | An instance is a fully quantified Boolean formula given as a structure: its |
| 11 | elements are variables and clauses, with the positive and negative |
| 12 | occurrences of variables in clauses as for CNF instances, a mark on the |
| 13 | quantified variables, a mark on those quantified universally, and a binary |
| 14 | relation ordering the variables as they appear in the quantifier prefix, |
| 15 | outermost first. The instance is well formed when that relation is a strict |
| 16 | linear order on the quantified variables. The matrix holds under a |
| 17 | valuation when every clause contains a true literal on a quantified |
| 18 | variable. |
| 19 | |
| 20 | Truth is defined as a game on positions made of the set of variables |
| 21 | already quantified and a valuation: a position is won when every variable |
| 22 | is quantified and the matrix holds, when the next variable of the prefix is |
| 23 | existential and one of its two values leads to a won position, or when it |
| 24 | is universal and both values do. An instance is a yes-instance of QSAT when |
| 25 | it is well formed and the initial position is won; QSAT is the decision |
| 26 | problem of the structures isomorphic to such an instance. The number of |
| 27 | alternations is not bounded. |
| 28 | -/ |
| 29 | |
| 30 | namespace Lax134656.Qsat |
| 31 | |
| 32 | open Lax904597.Problems Lax485149.Problems |
| 33 | |
| 34 | open FirstOrder |
| 35 | |
| 36 | open FirstOrder.Language |
| 37 | |
| 38 | /-- The relation symbols of the language. -/ |
| 39 | inductive qsatRel : ℕ → Type where |
| 40 | /-- `isVar x`: the element `x` is a quantified propositional variable. -/ |
| 41 | | isVar : qsatRel 1 |
| 42 | /-- `allVar x`: the variable `x` is quantified universally. -/ |
| 43 | | allVar : qsatRel 1 |
| 44 | /-- `prefixLt x y`: the variable `x` is quantified outside the variable |
| 45 | `y`. -/ |
| 46 | | prefixLt : qsatRel 2 |
| 47 | /-- `isClause c`: the element `c` is a clause of the matrix. -/ |
| 48 | | isClause : qsatRel 1 |
| 49 | /-- `posIn c x`: the variable `x` occurs positively in the clause `c`. -/ |
| 50 | | posIn : qsatRel 2 |
| 51 | /-- `negIn c x`: the variable `x` occurs negatively in the clause `c`. -/ |
| 52 | | negIn : qsatRel 2 |
| 53 | deriving DecidableEq |
| 54 | |
| 55 | /-- The relational vocabulary of fully quantified Boolean formulas: that of |
| 56 | CNF instances, together with the marks and the order describing the quantifier |
| 57 | prefix. -/ |
| 58 | def qsat : FirstOrder.Language := |
| 59 | ⟨fun _ => Empty, qsatRel⟩ |
| 60 | |
| 61 | instance instIsRelationalQsat : FirstOrder.Language.IsRelational qsat := fun _ => |
| 62 | (inferInstance : IsEmpty Empty) |
| 63 | |
| 64 | /-- `isVar x`: the element `x` is a quantified propositional variable. -/ |
| 65 | abbrev qsIsVar : qsat.Relations 1 := |
| 66 | .isVar |
| 67 | |
| 68 | /-- `allVar x`: the variable `x` is quantified universally. -/ |
| 69 | abbrev qsAllVar : qsat.Relations 1 := |
| 70 | .allVar |
| 71 | |
| 72 | /-- `prefixLt x y`: the variable `x` is quantified outside the variable |
| 73 | `y`. -/ |
| 74 | abbrev qsPrefixLt : qsat.Relations 2 := |
| 75 | .prefixLt |
| 76 | |
| 77 | /-- `isClause c`: the element `c` is a clause of the matrix. -/ |
| 78 | abbrev qsIsClause : qsat.Relations 1 := |
| 79 | .isClause |
| 80 | |
| 81 | /-- `posIn c x`: the variable `x` occurs positively in the clause `c`. -/ |
| 82 | abbrev qsPosIn : qsat.Relations 2 := |
| 83 | .posIn |
| 84 | |
| 85 | /-- `negIn c x`: the variable `x` occurs negatively in the clause `c`. -/ |
| 86 | abbrev qsNegIn : qsat.Relations 2 := |
| 87 | .negIn |
| 88 | |
| 89 | open FirstOrder |
| 90 | |
| 91 | open Language Structure |
| 92 | |
| 93 | section Reading |
| 94 | |
| 95 | variable {A : Type} [qsat.Structure A] |
| 96 | |
| 97 | /-- The element `x` is a quantified propositional variable. -/ |
| 98 | def IsQVar (x : A) : Prop := RelMap qsIsVar ![x] |
| 99 | |
| 100 | /-- The variable `x` is quantified universally. -/ |
| 101 | def IsQAll (x : A) : Prop := RelMap qsAllVar ![x] |
| 102 | |
| 103 | /-- The variable `x` is quantified outside the variable `y`. -/ |
| 104 | def QPrec (x y : A) : Prop := RelMap qsPrefixLt ![x, y] |
| 105 | |
| 106 | variable (A) in |
| 107 | /-- An instance is *well formed* when the quantifier prefix is a strict linear |
| 108 | order on the marked variables. Malformed instances are no-instances; the |
| 109 | condition is first-order, so the membership proof can check it. -/ |
| 110 | structure QsatWf : Prop where |
| 111 | /-- The prefix order only relates quantified variables. -/ |
| 112 | isVar_of_prec : ∀ x y : A, QPrec x y → IsQVar x ∧ IsQVar y |
| 113 | /-- The prefix order is irreflexive. -/ |
| 114 | irrefl : ∀ x : A, ¬QPrec x x |
| 115 | /-- The prefix order is transitive. -/ |
| 116 | trans : ∀ x y z : A, QPrec x y → QPrec y z → QPrec x z |
| 117 | /-- The prefix order is total on the quantified variables. -/ |
| 118 | total : ∀ x y : A, IsQVar x → IsQVar y → x ≠ y → QPrec x y ∨ QPrec y x |
| 119 | |
| 120 | /-- The matrix: every clause contains a literal on a *quantified* variable that |
| 121 | the valuation `τ` makes true. Elements that are not clauses impose nothing, |
| 122 | exactly as for satisfiability; an occurrence on an element that the |
| 123 | prefix does not quantify is not a literal, so the matrix depends on `τ` only |
| 124 | through its values on the variables. -/ |
| 125 | def QsatMatrix (τ : A → Prop) : Prop := |
| 126 | ∀ c : A, RelMap qsIsClause ![c] → |
| 127 | ∃ x : A, IsQVar x ∧ |
| 128 | ((RelMap qsPosIn ![c, x] ∧ τ x) ∨ (RelMap qsNegIn ![c, x] ∧ ¬τ x)) |
| 129 | |
| 130 | /-- Adding a variable to the set of already-quantified ones. -/ |
| 131 | def qAdd (D : A → Prop) (x : A) : A → Prop := fun y => y = x ∨ D y |
| 132 | |
| 133 | /-- Giving the value `b` to the variable `x` in the valuation `τ`. -/ |
| 134 | def qUpd (τ : A → Prop) (x : A) (b : Bool) : A → Prop := |
| 135 | fun y => (y = x ∧ b = true) ∨ (y ≠ x ∧ τ y) |
| 136 | |
| 137 | /-- The variable `x` is the one the position `D` quantifies next: it is the |
| 138 | `prefixLt`-least variable that `D` does not contain. -/ |
| 139 | def QLeast (D : A → Prop) (x : A) : Prop := |
| 140 | IsQVar x ∧ ¬D x ∧ ∀ y : A, IsQVar y → ¬D y → ¬QPrec y x |
| 141 | |
| 142 | end Reading |
| 143 | |
| 144 | section Game |
| 145 | |
| 146 | variable {A : Type} [qsat.Structure A] |
| 147 | |
| 148 | /-- **The quantifier game**: the existential player wins the position `(D, τ)`. |
| 149 | Either every variable is already quantified and the matrix holds, or the next |
| 150 | variable is existential and one of its two values wins, or it is universal and |
| 151 | both of its values win. -/ |
| 152 | inductive QsatWins : (A → Prop) → (A → Prop) → Prop |
| 153 | /-- Every variable has been quantified: the position is won exactly when the |
| 154 | matrix holds. -/ |
| 155 | | leaf {D τ : A → Prop} (hD : ∀ x : A, IsQVar x → D x) (hm : QsatMatrix τ) : QsatWins D τ |
| 156 | /-- The next variable is existential: the existential player picks a value |
| 157 | winning the rest of the game. -/ |
| 158 | | ex {D τ : A → Prop} {x : A} (hx : QLeast D x) (hq : ¬IsQAll x) (b : Bool) |
| 159 | (h : QsatWins (qAdd D x) (qUpd τ x b)) : QsatWins D τ |
| 160 | /-- The next variable is universal: both values must win the rest of the |
| 161 | game. -/ |
| 162 | | all {D τ : A → Prop} {x : A} (hx : QLeast D x) (hq : IsQAll x) |
| 163 | (h : ∀ b : Bool, QsatWins (qAdd D x) (qUpd τ x b)) : QsatWins D τ |
| 164 | |
| 165 | end Game |
| 166 | |
| 167 | section Problem |
| 168 | |
| 169 | variable {A : Type} [qsat.Structure A] |
| 170 | |
| 171 | variable (A) in |
| 172 | /-- **The yes-instances of QSAT**: a well-formed instance whose quantified |
| 173 | formula is true, i.e., whose initial position – nothing quantified yet, the |
| 174 | empty valuation – is won by the existential player. -/ |
| 175 | def QsatHolds : Prop := |
| 176 | QsatWf A ∧ QsatWins (fun _ : A => False) (fun _ : A => False) |
| 177 | |
| 178 | end Problem |
| 179 | |
| 180 | /-- QSAT: is the fully quantified Boolean formula described by the instance |
| 181 | true? -/ |
| 182 | def QSAT : DecisionProblem qsat := DecisionProblem.ofPred fun A _ => QsatHolds A |
| 183 | |
| 184 | end Lax134656.Qsat |
| 185 |
Builds on
Used by
Lax134656.AbiteboulVianuLax134656.AbiteboulVianuOrderedLax134656.HierarchyInPSPACELax134656.InflationaryInPartialLax134656.PartialFixedPointCaptureLax134656.PartialFixedPointClosureLax134656.PSPACEClosureLax134656.PSPACEEqCoPSPACELax134656.QsatInvarianceLax134656.QsatPSPACECompleteLax134656.SpaceBoundedMachineInvarianceLax134656.SpaceMachinesPSPACECompleteLax134656.SuccinctReachInvarianceLax134656.SuccinctReachPSPACECompleteLax134656.TransitiveClosureWithoutOrder
From Mathlib
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments