QBF: quantified Boolean formulas with bounded alternation

The problems QBF k – quantified Boolean formulas with k alternating blocks of propositional quantifiers – as decision problems on first-order structures. The vocabulary FirstOrder.Language.qbf k is that of SAT (FirstOrder.Language.sat: clauses, positive and negative occurrences) together with k unary block marks qbfBlock i splitting the propositional variables into the k quantifier blocks.

The semantics is the alternating quantification DescriptiveComplexity.altQuant: block 0 is quantified outermost, block k - 1 innermost, and the polarities alternate starting from start. Each quantifier picks a truth assignment for its own block; the combined truth value of a variable (DescriptiveComplexity.qbfVal) is given by the assignment of a block that marks it.

The innermost quantifier-free matrix comes in two shapes, selected by a Boolean parameter:

• DescriptiveComplexity.CnfSat – conjunctive: every clause contains a true literal;
• DescriptiveComplexity.DnfSat – disjunctive: some term has all its literals true.

Both shapes are needed. The hardness proof (DescriptiveComplexity.Problems.Qbf.Hardness) encodes the first-order kernel of a second-order definition by a Tseitin translation (Tseitin 1968), which introduces auxiliary gate variables; these are functionally determined by the block variables, so they can be absorbed into the innermost quantifier only when that quantifier is existential. For a prefix starting existentially the innermost quantifier is existential exactly when k is odd, which is why DescriptiveComplexity.QBF takes a conjunctive matrix for odd k and a disjunctive one for even k – the standard form of the Σₖᵖ-complete quantified Boolean formula problems (Stockmeyer 1976; Wrathall 1976).

inductive FirstOrder.Language.qbfRel (k : ℕ) : ℕ → Type

Relation symbols of the language of quantified Boolean formulas with k quantifier blocks.

• isClause {k : ℕ} : qbfRel k 1

  isClause c: the element c is a clause (a term, for a disjunctive matrix).

• posIn {k : ℕ} : qbfRel k 2

  posIn c x: the variable x occurs positively in the clause c.

• negIn {k : ℕ} : qbfRel k 2

  negIn c x: the variable x occurs negatively in the clause c.

• block {k : ℕ} : Fin k → qbfRel k 1

  block i x: the variable x belongs to the i-th quantifier block.

def FirstOrder.Language.instDecidableEqQbfRel.decEq {k✝ a✝ : ℕ} (x✝ x✝¹ : qbfRel k✝ a✝) : Decidable (x✝ = x✝¹)

Equations

• FirstOrder.Language.instDecidableEqQbfRel.decEq FirstOrder.Language.qbfRel.isClause FirstOrder.Language.qbfRel.isClause = isTrue ⋯
• FirstOrder.Language.instDecidableEqQbfRel.decEq FirstOrder.Language.qbfRel.isClause (FirstOrder.Language.qbfRel.block a_1) = isFalse ⋯
• FirstOrder.Language.instDecidableEqQbfRel.decEq FirstOrder.Language.qbfRel.posIn FirstOrder.Language.qbfRel.posIn = isTrue ⋯
• FirstOrder.Language.instDecidableEqQbfRel.decEq FirstOrder.Language.qbfRel.posIn FirstOrder.Language.qbfRel.negIn = isFalse ⋯
• FirstOrder.Language.instDecidableEqQbfRel.decEq FirstOrder.Language.qbfRel.negIn FirstOrder.Language.qbfRel.posIn = isFalse ⋯
• FirstOrder.Language.instDecidableEqQbfRel.decEq FirstOrder.Language.qbfRel.negIn FirstOrder.Language.qbfRel.negIn = isTrue ⋯
• FirstOrder.Language.instDecidableEqQbfRel.decEq (FirstOrder.Language.qbfRel.block a_1) FirstOrder.Language.qbfRel.isClause = isFalse ⋯
• FirstOrder.Language.instDecidableEqQbfRel.decEq (FirstOrder.Language.qbfRel.block a_1) (FirstOrder.Language.qbfRel.block b) = if h : a_1 = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqQbfRel {k✝ a✝ : ℕ} : DecidableEq (qbfRel k✝ a✝)

Equations

• FirstOrder.Language.instDecidableEqQbfRel = FirstOrder.Language.instDecidableEqQbfRel.decEq

def FirstOrder.Language.qbf (k : ℕ) : Language

The relational vocabulary of quantified Boolean formulas with k quantifier blocks: that of CNF instances, together with k unary predicates marking the variables of each quantifier block.

Equations

• FirstOrder.Language.qbf k = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.qbfRel k }

instance FirstOrder.Language.instIsRelationalQbf (k : ℕ) : (Language.qbf k).IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.qbfIsClause {k : ℕ} : (Language.qbf k).Relations 1

The symbol for “is a clause”.

Equations

• FirstOrder.Language.qbfIsClause = FirstOrder.Language.qbfRel.isClause

@[reducible, inline]

abbrev FirstOrder.Language.qbfPosIn {k : ℕ} : (Language.qbf k).Relations 2

The symbol for “occurs positively in”.

Equations

• FirstOrder.Language.qbfPosIn = FirstOrder.Language.qbfRel.posIn

@[reducible, inline]

abbrev FirstOrder.Language.qbfNegIn {k : ℕ} : (Language.qbf k).Relations 2

The symbol for “occurs negatively in”.

Equations

• FirstOrder.Language.qbfNegIn = FirstOrder.Language.qbfRel.negIn

@[reducible, inline]

abbrev FirstOrder.Language.qbfBlock {k : ℕ} (i : Fin k) : (Language.qbf k).Relations 1

The symbol marking the variables of the i-th quantifier block.

Equations

• FirstOrder.Language.qbfBlock i = FirstOrder.Language.qbfRel.block i

Alternating quantification over truth assignments

def DescriptiveComplexity.altQuant (A : Type) (k : ℕ) : ((Fin k → A → Prop) → Prop) → Bool → Prop

Alternating quantification over k truth assignments on A: the assignment of index 0 is quantified outermost, existentially if pol is true, and the polarities alternate inwards.

Equations

• DescriptiveComplexity.altQuant A 0 P x✝ = P Fin.elim0
• DescriptiveComplexity.altQuant A k.succ P true = ∃ (ν : A → Prop), DescriptiveComplexity.altQuant A k (fun (νs : Fin k → A → Prop) => P (Fin.cons ν νs)) false
• DescriptiveComplexity.altQuant A k.succ P false = ∀ (ν : A → Prop), DescriptiveComplexity.altQuant A k (fun (νs : Fin k → A → Prop) => P (Fin.cons ν νs)) true

theorem DescriptiveComplexity.altQuant_congr {A : Type} (k : ℕ) (P Q : (Fin k → A → Prop) → Prop) : (∀ (νs : Fin k → A → Prop), P νs ↔ Q νs) → ∀ (pol : Bool), altQuant A k P pol ↔ altQuant A k Q pol

Alternating quantification only depends on the quantified predicate up to pointwise equivalence.

theorem DescriptiveComplexity.altQuant_equiv {A B : Type} (e : A ≃ B) (k : ℕ) (P : (Fin k → A → Prop) → Prop) (pol : Bool) : altQuant B k (fun (νs : Fin k → B → Prop) => P fun (i : Fin k) (a : A) => νs i (e a)) pol ↔ altQuant A k P pol

Transport of alternating quantification along an equivalence of universes: quantifying over assignments on B and reading them back through e is quantifying over assignments on A.

The matrix of a quantified Boolean formula

def DescriptiveComplexity.qbfVal {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] (νs : Fin k → A → Prop) (x : A) : Prop

The truth value of the variable x under a tuple of block assignments: x is true when some block marking it assigns it the value true. (In a well-formed instance the block marks partition the variables, so exactly one assignment is consulted.)

Equations

• DescriptiveComplexity.qbfVal νs x = ∃ (i : Fin k), FirstOrder.Language.Structure.RelMap (FirstOrder.Language.qbfBlock i) ![x] ∧ νs i x

def DescriptiveComplexity.CnfSatWith {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] (swap : Bool) (νs : Fin k → A → Prop) : Prop

Conjunctive satisfaction, with the sign of every literal flipped when swap is true: every clause then has to contain a literal that the block assignments make false.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.CnfSat {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] (νs : Fin k → A → Prop) : Prop

The conjunctive matrix: every clause contains a literal made true by the block assignments.

Equations

• DescriptiveComplexity.CnfSat νs = DescriptiveComplexity.CnfSatWith false νs

def DescriptiveComplexity.DnfSat {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] (νs : Fin k → A → Prop) : Prop

The disjunctive matrix: some term has all of its literals made true by the block assignments.

Equations

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

def DescriptiveComplexity.QbfMatrix {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] (cnf : Bool) (νs : Fin k → A → Prop) : Prop

The matrix of a quantified Boolean formula: conjunctive when cnf is true, disjunctive when it is false.

Equations

• DescriptiveComplexity.QbfMatrix true νs = DescriptiveComplexity.CnfSat νs
• DescriptiveComplexity.QbfMatrix false νs = DescriptiveComplexity.DnfSat νs

theorem DescriptiveComplexity.dnfSat_iff_not_cnfSatWith_true {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] (νs : Fin k → A → Prop) : DnfSat νs ↔ ¬CnfSatWith true νs

Propositional duality: the disjunctive matrix is the negation of the conjunctive one with the sign of every literal swapped. This is what lets a single Tseitin translation serve both parities of k: at even k the innermost quantifier is universal, and it absorbs the gate variables through this negation.

def DescriptiveComplexity.xorP (b : Bool) (P : Prop) : Prop

Optional negation, indexed by a Boolean.

Equations

• DescriptiveComplexity.xorP true P = ¬P
• DescriptiveComplexity.xorP false P = P

theorem DescriptiveComplexity.xorP_congr (b : Bool) {P Q : Prop} (h : P ↔ Q) : xorP b P ↔ xorP b Q

theorem DescriptiveComplexity.qbfMatrix_eq_xorP {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] (sw : Bool) (νs : Fin k → A → Prop) : QbfMatrix (!sw) νs ↔ xorP sw (CnfSatWith sw νs)

The two matrix shapes, uniformly: whichever matrix QBF uses at a given parity is the conjunctive one with the corresponding sign swap, negated exactly when the swap happens. This is what lets the hardness proof treat both parities at once.

Isomorphism-invariance

The decision problems

def DescriptiveComplexity.QbfProblem (k : ℕ) (start cnf : Bool) : DecisionProblem (FirstOrder.Language.qbf k)

Quantified Boolean formulas with k alternating quantifier blocks: the prefix starts with an existential block when start is true, and the matrix is conjunctive when cnf is true.

Equations

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

def DescriptiveComplexity.QBF (k : ℕ) : DecisionProblem (FirstOrder.Language.qbf k)

QBF with k alternating blocks, the canonical Σₖᵖ-complete problem: an existential outermost block, and a matrix whose shape follows the parity of k – conjunctive when the innermost quantifier is existential (k odd), disjunctive when it is universal (k even). See DescriptiveComplexity.Problems.Qbf for the completeness theorem.

Equations

• DescriptiveComplexity.QBF k = DescriptiveComplexity.QbfProblem k true (k % 2 == 1)

def DescriptiveComplexity.QBFPi (k : ℕ) : DecisionProblem (FirstOrder.Language.qbf k)

The dual family, with a universal outermost block: the canonical Πₖᵖ-complete problem.

Equations

• DescriptiveComplexity.QBFPi k = DescriptiveComplexity.QbfProblem k false (k % 2 == 0)