QBF: quantified Boolean formulas with bounded alternation

Umbrella file for the problems DescriptiveComplexity.QBF k – quantified Boolean formulas with k alternating blocks of propositional quantifiers – the canonical complete problems for the levels of the polynomial hierarchy (Stockmeyer 1976; Wrathall 1976).

• DescriptiveComplexity.Problems.Qbf.Defs: the vocabulary FirstOrder.Language.qbf k (that of SAT, plus k unary block marks), the alternating semantics DescriptiveComplexity.altQuant, the two shapes of matrix (DescriptiveComplexity.CnfSat, DescriptiveComplexity.DnfSat) and their propositional duality, and the bundled problems DescriptiveComplexity.QBF / DescriptiveComplexity.QBFPi.
• DescriptiveComplexity.Problems.Qbf.Membership: the membership half, DescriptiveComplexity.qbfProblem_sigmaSODefinable and DescriptiveComplexity.qbfProblem_piSODefinable.
• DescriptiveComplexity.Problems.Qbf.Transfer: the block-by-block transfer between alternation over truth assignments and alternation over second-order block assignments.
• DescriptiveComplexity.Problems.Qbf.Hardness: the Tseitin interpretation with block marks, and its correctness at a fixed truth assignment.

The parity of k

The matrix of DescriptiveComplexity.QBF k is conjunctive for odd k and disjunctive for even k. This is forced, and is the standard form of the Σₖᵖ-complete quantified Boolean formula problems. The hardness proof encodes the first-order kernel of a second-order definition by the Tseitin translation (Tseitin 1968) of DescriptiveComplexity.Problems.Sat.Tseitin, which introduces auxiliary gate variables. Those are functionally determined by the block variables, so ∃ gates, CNF(atoms, gates) ↔ φ(atoms), and the gate quantifier can be absorbed into the innermost quantifier of the prefix only when that quantifier is existential – otherwise the universal player falsifies a gate clause and the instance collapses. For a prefix starting existentially the innermost quantifier is existential exactly when k is odd; at even k one uses the dual, disjunctive matrix, for which DescriptiveComplexity.dnfSat_iff_not_cnfSatWith_true turns the innermost universal quantifier back into an existential one over the gates.

Both halves are complete, for both families: DescriptiveComplexity.QBF_complete states that QBF (k + 1) is Σₖ₊₁ᵖ-complete and DescriptiveComplexity.QBFPi_complete that QBFPi (k + 1) is Πₖ₊₁ᵖ-complete, for every k. The two use the same reduction, DescriptiveComplexity.qbfReduction, which is parameterized by the starting polarity; only the parity of the matrix flips with it. At k = 0 they specialize to NP- and coNP-completeness (DescriptiveComplexity.QBF_one_NP_complete, DescriptiveComplexity.QBFPi_one_coNP_complete). Like the rest of the library the development is axiom-free: #print axioms reports only propext, Classical.choice and Quot.sound.

theorem DescriptiveComplexity.QBF_complete (k : ℕ) : (SigmaP (k + 1)).Complete (QBF (k + 1))

QBF with k + 1 alternating blocks is Σₖ₊₁ᵖ-complete. Membership is DescriptiveComplexity.qbf_mem_sigmaP – guess the k + 1 truth assignments as monadic second-order relations and evaluate the matrix first-order. Hardness is DescriptiveComplexity.qbf_hard_of_sigmaSODefinable, the marked Tseitin discharge. Registered in the Lax archive as Lax564036.QbfComplete.qbf_complete.

theorem DescriptiveComplexity.QBFPi_complete (k : ℕ) : (PiP (k + 1)).Complete (QBFPi (k + 1))

The dual family is Πₖ₊₁ᵖ-complete: QBFPi (k + 1), with a universal outermost block, is complete for Πₖ₊₁ᵖ. Membership is DescriptiveComplexity.qbfPi_mem_piP; hardness is DescriptiveComplexity.qbfPi_hard_of_piSODefinable, the same marked Tseitin discharge at the other starting polarity. Registered in the Lax archive as Lax564036.QbfComplete.qbfPi_complete.

theorem DescriptiveComplexity.QBFPi_one_coNP_complete : coNP.Complete (QBFPi 1)

QBF with one universal block is coNP-complete.

theorem DescriptiveComplexity.QBF_one_NP_complete : NP.Complete (QBF 1)

QBF with one block and a conjunctive matrix is NP-complete – it is essentially SAT with all variables marked.

theorem DescriptiveComplexity.qbf_one_mem_NP : NP.Mem (QBF 1)

QBF with one block is in NP.