Documentation

DescriptiveComplexity.Problems.Qsat.Defs

QSAT: quantified Boolean formulas with an unbounded prefix #

The vocabulary and semantics of the canonical PSPACE-complete problem (DescriptiveComplexity.QSAT, also known as TQBF or QBF): is a fully quantified Boolean formula in prenex conjunctive normal form true? Unlike the bounded families DescriptiveComplexity.QBF k of DescriptiveComplexity.Problems.Qbf – where the number of alternations is fixed by the problem and only the matrix comes with the instance – here the quantifier prefix is part of the instance, so a single problem carries arbitrarily many alternations. That is exactly the step from the polynomial hierarchy to PSPACE.

The instance #

An instance is a FirstOrder.Language.qsat-structure. As in FirstOrder.Language.sat, its elements are propositional variables and clauses at once, with

isVar x: the element x is a quantified propositional variable;
allVar x: the variable x is quantified universally (existentially otherwise);
prefixLt x y: the variable x is quantified outside the variable y;
isClause c, posIn c x, negIn c x: the clauses of the matrix and the literal occurrences, exactly as for SAT.

An instance is well formed (DescriptiveComplexity.QsatWf) when prefixLt is a strict linear order on the marked variables; a malformed instance is a no-instance. Well-formedness is a first-order condition, which is what lets the membership proof check it inside the walk.

The semantics #

Reading a quantifier prefix means recursing along prefixLt, and the recursion is over a set of remaining variables rather than over a syntactic list. It is packaged as an inductive predicate DescriptiveComplexity.QsatWins: a position is a pair (D, τ) of a set D of already-quantified variables and a valuation τ, and QsatWins D τ says that the existential player wins the game that quantifies the variables outside D, innermost-first, and ends in the matrix. An inductive definition is used rather than a recursion so that the semantics is available on an arbitrary (possibly infinite) structure, as DescriptiveComplexity.DecisionProblem requires; on a finite well-formed structure it is the usual game value, since the three rules are then mutually exclusive and exhaustive (DescriptiveComplexity.qsatWins_all_iff, DescriptiveComplexity.qsatWins_ex_iff, DescriptiveComplexity.qsatWins_leaf_iff, proved by inversion alone).

The quantified variable at a position is the prefixLt-least one not yet in D (DescriptiveComplexity.QLeast), so the prefix is read outermost-first and the players move in the order the instance prescribes.

inductive FirstOrder.Language.qsatRel :

Relation symbols of the language of fully quantified Boolean formulas with an unbounded quantifier prefix.

isVar : qsatRel 1
isVar x: the element x is a quantified propositional variable.
allVar : qsatRel 1
allVar x: the variable x is quantified universally.
prefixLt : qsatRel 2
prefixLt x y: the variable x is quantified outside the variable y.
isClause : qsatRel 1
isClause c: the element c is a clause of the matrix.
posIn : qsatRel 2
posIn c x: the variable x occurs positively in the clause c.
negIn : qsatRel 2
negIn c x: the variable x occurs negatively in the clause c.

Instances For

Dependency graph

def FirstOrder.Language.instDecidableEqQsatRel.decEq {a✝ : ℕ} (x✝ x✝¹ : qsatRel a✝) :

Decidable (x✝ = x✝¹)

Equations

Instances For

Dependency graph

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqQsatRel {a✝ : ℕ} :

DecidableEq (qsatRel a✝)

Equations

FirstOrder.Language.instDecidableEqQsatRel = FirstOrder.Language.instDecidableEqQsatRel.decEq

Dependency graph

def FirstOrder.Language.qsat :

The relational vocabulary of fully quantified Boolean formulas: that of CNF instances, together with the marks and the order describing the quantifier prefix.

Equations

FirstOrder.Language.qsat = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.qsatRel }

Instances For

Dependency graph

instance FirstOrder.Language.instIsRelationalQsat :

Language.qsat.IsRelational

Dependency graph

@[reducible, inline]

abbrev FirstOrder.Language.qsIsVar :

Language.qsat.Relations 1

The symbol for “is a quantified variable”.

Equations

FirstOrder.Language.qsIsVar = FirstOrder.Language.qsatRel.isVar

Instances For

Dependency graph

@[reducible, inline]

abbrev FirstOrder.Language.qsAllVar :

Language.qsat.Relations 1

The symbol for “is universally quantified”.

Equations

FirstOrder.Language.qsAllVar = FirstOrder.Language.qsatRel.allVar

Instances For

Dependency graph

@[reducible, inline]

abbrev FirstOrder.Language.qsPrefixLt :

Language.qsat.Relations 2

The symbol for “is quantified outside”.

Equations

FirstOrder.Language.qsPrefixLt = FirstOrder.Language.qsatRel.prefixLt

Instances For

Dependency graph

@[reducible, inline]

abbrev FirstOrder.Language.qsIsClause :

Language.qsat.Relations 1

The symbol for “is a clause”.

Equations

FirstOrder.Language.qsIsClause = FirstOrder.Language.qsatRel.isClause

Instances For

Dependency graph

@[reducible, inline]

abbrev FirstOrder.Language.qsPosIn :

Language.qsat.Relations 2

The symbol for “occurs positively in”.

Equations

FirstOrder.Language.qsPosIn = FirstOrder.Language.qsatRel.posIn

Instances For

Dependency graph

@[reducible, inline]

abbrev FirstOrder.Language.qsNegIn :

Language.qsat.Relations 2

The symbol for “occurs negatively in”.

Equations

FirstOrder.Language.qsNegIn = FirstOrder.Language.qsatRel.negIn

Instances For

Dependency graph

Reading an instance #

def DescriptiveComplexity.IsQVar {A : Type} [FirstOrder.Language.qsat.Structure A] (x : A) :

The element x is a quantified propositional variable.

Equations

DescriptiveComplexity.IsQVar x = FirstOrder.Language.Structure.RelMap FirstOrder.Language.qsIsVar ![x]

Instances For

Dependency graph

def DescriptiveComplexity.IsQAll {A : Type} [FirstOrder.Language.qsat.Structure A] (x : A) :

The variable x is quantified universally.

Equations

DescriptiveComplexity.IsQAll x = FirstOrder.Language.Structure.RelMap FirstOrder.Language.qsAllVar ![x]

Instances For

Dependency graph

def DescriptiveComplexity.QPrec {A : Type} [FirstOrder.Language.qsat.Structure A] (x y : A) :

The variable x is quantified outside the variable y.

Equations

DescriptiveComplexity.QPrec x y = FirstOrder.Language.Structure.RelMap FirstOrder.Language.qsPrefixLt ![x, y]

Instances For

Dependency graph

structure DescriptiveComplexity.QsatWf (A : Type) [FirstOrder.Language.qsat.Structure A] :

An instance is well formed when the quantifier prefix is a strict linear order on the marked variables. Malformed instances are no-instances; the condition is first-order, so the membership proof can check it.

isVar_of_prec (x y : A) : QPrec x y → IsQVar x ∧ IsQVar y
The prefix order only relates quantified variables.
irrefl (x : A) : ¬QPrec x x
The prefix order is irreflexive.
trans (x y z : A) : QPrec x y → QPrec y z → QPrec x z
The prefix order is transitive.
total (x y : A) : IsQVar x → IsQVar y → x ≠ y → QPrec x y ∨ QPrec y x
The prefix order is total on the quantified variables.

Instances For

Dependency graph

def DescriptiveComplexity.QsatMatrix {A : Type} [FirstOrder.Language.qsat.Structure A] (τ : A → Prop) :

The matrix: every clause contains a literal on a quantified variable that the valuation τ makes true. Elements that are not clauses impose nothing, exactly as in DescriptiveComplexity.Satisfiable; an occurrence on an element that the prefix does not quantify is not a literal, so the matrix depends on τ only through its values on the variables.

Equations

One or more equations did not get rendered due to their size.

Instances For

Dependency graph

theorem DescriptiveComplexity.qsatMatrix_congr {A : Type} [FirstOrder.Language.qsat.Structure A] {τ τ' : A → Prop} (h : ∀ (y : A), IsQVar y → (τ y ↔ τ' y)) (hm : QsatMatrix τ) :

The matrix only depends on the valuation through its values on the quantified variables.

Dependency graph

def DescriptiveComplexity.qAdd {A : Type} (D : A → Prop) (x : A) :

A → Prop

Adding a variable to the set of already-quantified ones.

Equations

DescriptiveComplexity.qAdd D x y = (y = x ∨ D y)

Instances For

Dependency graph

def DescriptiveComplexity.qUpd {A : Type} (τ : A → Prop) (x : A) (b : Bool) :

A → Prop

Giving the value b to the variable x in the valuation τ.

Equations

DescriptiveComplexity.qUpd τ x b y = (y = x ∧ b = true ∨ y ≠ x ∧ τ y)

Instances For

Dependency graph

@[simp]

theorem DescriptiveComplexity.qAdd_self {A : Type} (D : A → Prop) (x : A) :

qAdd D x x

Dependency graph

theorem DescriptiveComplexity.qAdd_of {A : Type} (D : A → Prop) {x y : A} (h : D y) :

qAdd D x y

Dependency graph

@[simp]

theorem DescriptiveComplexity.qUpd_self {A : Type} (τ : A → Prop) (x : A) (b : Bool) :

qUpd τ x b x ↔ b = true

Dependency graph

theorem DescriptiveComplexity.qUpd_ne {A : Type} (τ : A → Prop) {x y : A} (b : Bool) (h : y ≠ x) :

qUpd τ x b y ↔ τ y

Dependency graph

def DescriptiveComplexity.QLeast {A : Type} [FirstOrder.Language.qsat.Structure A] (D : A → Prop) (x : A) :

The variable x is the one the position D quantifies next: it is the prefixLt-least variable that D does not contain.

Equations

DescriptiveComplexity.QLeast D x = (DescriptiveComplexity.IsQVar x ∧ ¬D x ∧ ∀ (y : A), DescriptiveComplexity.IsQVar y → ¬D y → ¬DescriptiveComplexity.QPrec y x)

Instances For

Dependency graph

theorem DescriptiveComplexity.QLeast.unique {A : Type} [FirstOrder.Language.qsat.Structure A] (hwf : QsatWf A) {D : A → Prop} {x y : A} (hx : QLeast D x) (hy : QLeast D y) :

x = y

The next variable to quantify is unique, by totality of the prefix order.

Dependency graph

The game #

QsatWins D τ is the value of the position in which the variables of D have already been given their values by τ and the remaining ones are still to be quantified, innermost-first along the prefix order.

inductive DescriptiveComplexity.QsatWins {A : Type} [FirstOrder.Language.qsat.Structure A] :

(A → Prop) → (A → Prop) → Prop

The quantifier game: the existential player wins the position (D, τ). Either every variable is already quantified and the matrix holds, or the next variable is existential and one of its two values wins, or it is universal and both of its values win.

leaf {A : Type} [FirstOrder.Language.qsat.Structure A] {D τ : A → Prop} (hD : ∀ (x : A), IsQVar x → D x) (hm : QsatMatrix τ) : QsatWins D τ
Every variable has been quantified: the position is won exactly when the matrix holds.
ex {A : Type} [FirstOrder.Language.qsat.Structure A] {D τ : A → Prop} {x : A} (hx : QLeast D x) (hq : ¬IsQAll x) (b : Bool) (h : QsatWins (qAdd D x) (qUpd τ x b)) : QsatWins D τ
The next variable is existential: the existential player picks a value winning the rest of the game.
all {A : Type} [FirstOrder.Language.qsat.Structure A] {D τ : A → Prop} {x : A} (hx : QLeast D x) (hq : IsQAll x) (h : ∀ (b : Bool), QsatWins (qAdd D x) (qUpd τ x b)) : QsatWins D τ
The next variable is universal: both values must win the rest of the game.

Instances For

Dependency graph

theorem DescriptiveComplexity.qsatWins_congr {A : Type} [FirstOrder.Language.qsat.Structure A] {D τ : A → Prop} (h : QsatWins D τ) (τ' : A → Prop) :

(∀ (y : A), D y → (τ y ↔ τ' y)) → QsatWins D τ'

A position only depends on the values already given: two valuations agreeing on the quantified part D win the same positions. This is what makes (D, τ) a position rather than a full state: the values of τ outside D are about to be overwritten by the quantifiers.

Dependency graph

The three rules read backwards #

Together with DescriptiveComplexity.QLeast.unique the constructors are mutually exclusive, so each of them is an equivalence: the inductive predicate is the game value, and no induction is needed to see it.

theorem DescriptiveComplexity.qsatWins_leaf_iff {A : Type} [FirstOrder.Language.qsat.Structure A] {D τ : A → Prop} (hD : ∀ (x : A), IsQVar x → D x) :

QsatWins D τ ↔ QsatMatrix τ

At a position where every variable is quantified, winning is satisfying the matrix.

Dependency graph

theorem DescriptiveComplexity.qsatWins_ex_iff {A : Type} [FirstOrder.Language.qsat.Structure A] (hwf : QsatWf A) {D τ : A → Prop} {x : A} (hx : QLeast D x) (hq : ¬IsQAll x) :

QsatWins D τ ↔ ∃ (b : Bool), QsatWins (qAdd D x) (qUpd τ x b)

At a position whose next variable is existential, winning is winning after one of its two values.

Dependency graph

theorem DescriptiveComplexity.qsatWins_all_iff {A : Type} [FirstOrder.Language.qsat.Structure A] (hwf : QsatWf A) {D τ : A → Prop} {x : A} (hx : QLeast D x) (hq : IsQAll x) :

QsatWins D τ ↔ ∀ (b : Bool), QsatWins (qAdd D x) (qUpd τ x b)

At a position whose next variable is universal, winning is winning after both of its values.

Dependency graph

Isomorphism-invariance #

The decision problem #

def DescriptiveComplexity.QsatHolds (A : Type) [FirstOrder.Language.qsat.Structure A] :

The yes-instances of QSAT: a well-formed instance whose quantified formula is true, i.e. whose initial position – nothing quantified yet, the empty valuation – is won by the existential player.

Equations

DescriptiveComplexity.QsatHolds A = (DescriptiveComplexity.QsatWf A ∧ DescriptiveComplexity.QsatWins (fun (x : A) => False) fun (x : A) => False)

Instances For

Dependency graph

def DescriptiveComplexity.QSAT :

DecisionProblem FirstOrder.Language.qsat

QSAT, as a problem on FirstOrder.Language.qsat-structures: is the fully quantified Boolean formula described by the instance true?

Equations

One or more equations did not get rendered due to their size.

Instances For

Dependency graph