Hardness of QBF

The hardness half of the completeness of DescriptiveComplexity.QBF: every problem definable by a second-order sentence with k + 1 alternating blocks admits an ordered first-order reduction to DescriptiveComplexity.QBF (k + 1) (DescriptiveComplexity.qbf_hard_of_sigmaSODefinable). This is the Cook–Levin discharge of DescriptiveComplexity.Problems.Sat.Hardness with block marks added.

The quantifier prefix of a second-order definition is merged into a single block (DescriptiveComplexity.SecondOrderMerge), the Tseitin translation (Tseitin 1968) of the resulting first-order kernel is interpreted inside an ordered input structure exactly as for SAT (DescriptiveComplexity.qbfTseitinInterp), and each propositional variable is marked with the quantifier block it belongs to: an atom variable with the block its relation variable comes from, and every gate variable with the innermost block.

Gate variables can only be marked innermost, and only work out when the innermost quantifier is existential – they are functionally determined by the atoms, so ∃ gates, CNF ↔ φ, whereas a universal player could falsify a gate clause. With an existential outermost block the innermost quantifier is existential exactly when k is odd, which is why the literal signs of the interpretation are swapped (the parameter sw), and the kernel negated, when k is even: the disjunctive matrix of DescriptiveComplexity.QBF k at even k is, by DescriptiveComplexity.dnfSat_iff_not_cnfSatWith_true, the negation of a conjunctive matrix with all signs swapped, and that negation turns the innermost universal quantifier back into an existential one over the gates. The swap is arranged so that the parity disappears from the correctness proof: whichever of posIn/negIn a satisfied clause must make true always carries the positive Tseitin literals (DescriptiveComplexity.qbfT_lit_pos).

The key correctness statement is DescriptiveComplexity.qbfT_clauses_iff, the ∃-free form of DescriptiveComplexity.tseitin_satisfiable_iff: with the truth assignment given – as the quantifier prefix of a QBF supplies it, rather than existentially quantified as for SAT – the clauses of the encoding hold exactly when the induced valuation satisfies every Tseitin gate and makes the root variable true.

The discharge itself is DescriptiveComplexity.qbf_hard_of_sigmaSODefinable; together with the membership half of DescriptiveComplexity.Problems.Qbf.Membership it gives the completeness theorem DescriptiveComplexity.QBF_complete.

@[reducible]

noncomputable def DescriptiveComplexity.gateBlock {L : FirstOrder.Language} (M : SOBlock) (ψ : (L.sum M.lang).Sentence) : SOBlock

The block of Tseitin gate variables: one relation variable per subformula position of the kernel, of the interpretation's dimension. Reducible, so that (gateBlock M ψ).ι unfolds to the type of subformula positions.

Equations

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

noncomputable def DescriptiveComplexity.qbfTseitinInterp {L : FirstOrder.Language} (k : ℕ) (sw : Bool) (M : SOBlock) (ψ : (L.sum M.lang).Sentence) (mark : M.ι ⊕ (m : ℕ) × Tseitin.NodeAt ψ m → Fin k) : FOInterpretation (L.sum FirstOrder.Language.order) (FirstOrder.Language.qbf k) (TseitinTag M ψ) (tseitinDim M ψ)

The Tseitin interpretation with block marks: the CNF instance of the encoding of ψ, with each propositional variable marked by the quantifier block it belongs to. The signs of the literals are swapped when sw is true, i.e. when the innermost quantifier of the prefix is universal.

Equations

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

Characterization of the interpreted relations

theorem DescriptiveComplexity.qbfT_isClause_node {L : FirstOrder.Language} (k : ℕ) (sw : Bool) (M : SOBlock) (ψ : (L.sum M.lang).Sentence) (mark : M.ι ⊕ (m : ℕ) × Tseitin.NodeAt ψ m → Fin k) {A : Type} [L.Structure A] [LinearOrder A] (σp : (m : ℕ) × Tseitin.NodeAt ψ m) (c : Fin 3) (u : Fin (tseitinDim M ψ) → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.qbfIsClause ![(Sum.inl (Sum.inl (σp, c)), u)] ↔ Tseitin.IsClauseSem ψ ⋯ σp.snd c u

theorem DescriptiveComplexity.qbfT_isClause_top {L : FirstOrder.Language} (k : ℕ) (sw : Bool) (M : SOBlock) (ψ : (L.sum M.lang).Sentence) (mark : M.ι ⊕ (m : ℕ) × Tseitin.NodeAt ψ m → Fin k) {A : Type} [L.Structure A] [LinearOrder A] (u : Fin (tseitinDim M ψ) → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.qbfIsClause ![(Sum.inl (Sum.inr ()), u)] ↔ Canon 0 u

theorem DescriptiveComplexity.qbfT_isClause_var {L : FirstOrder.Language} (k : ℕ) (sw : Bool) (M : SOBlock) (ψ : (L.sum M.lang).Sentence) (mark : M.ι ⊕ (m : ℕ) × Tseitin.NodeAt ψ m → Fin k) {A : Type} [L.Structure A] [LinearOrder A] (vt : M.ι ⊕ (m : ℕ) × Tseitin.NodeAt ψ m) (u : Fin (tseitinDim M ψ) → A) : ¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.qbfIsClause ![(Sum.inr vt, u)]

theorem DescriptiveComplexity.qbfT_lit_iff {L : FirstOrder.Language} (k : ℕ) (sw : Bool) (M : SOBlock) (ψ : (L.sum M.lang).Sentence) (mark : M.ι ⊕ (m : ℕ) × Tseitin.NodeAt ψ m → Fin k) {A : Type} [L.Structure A] [LinearOrder A] (s : Bool) (tc tx : TseitinTag M ψ) (u x : Fin (tseitinDim M ψ) → A) : FirstOrder.Language.Structure.RelMap (if s = true then FirstOrder.Language.qbfPosIn else FirstOrder.Language.qbfNegIn) ![(tc, u), (tx, x)] ↔ TseitinLitSem M ψ (s ^^ sw) tc tx u x

The literals of the interpretation are those of the Tseitin encoding, with the signs swapped when sw is true.

theorem DescriptiveComplexity.qbfT_block_var {L : FirstOrder.Language} (k : ℕ) (sw : Bool) (M : SOBlock) (ψ : (L.sum M.lang).Sentence) (mark : M.ι ⊕ (m : ℕ) × Tseitin.NodeAt ψ m → Fin k) {A : Type} [L.Structure A] [LinearOrder A] (j : Fin k) (vt : M.ι ⊕ (m : ℕ) × Tseitin.NodeAt ψ m) (u : Fin (tseitinDim M ψ) → A) : FirstOrder.Language.Structure.RelMap (FirstOrder.Language.qbfBlock j) ![(Sum.inr vt, u)] ↔ mark vt = j

A variable is marked by exactly the block it belongs to; clause elements are marked by no block at all.

theorem DescriptiveComplexity.qbfT_lit_pos {L : FirstOrder.Language} (k : ℕ) (sw : Bool) (M : SOBlock) (ψ : (L.sum M.lang).Sentence) (mark : M.ι ⊕ (m : ℕ) × Tseitin.NodeAt ψ m → Fin k) {A : Type} [L.Structure A] [LinearOrder A] (tc tx : TseitinTag M ψ) (u x : Fin (tseitinDim M ψ) → A) : FirstOrder.Language.Structure.RelMap (if sw = true then FirstOrder.Language.qbfNegIn else FirstOrder.Language.qbfPosIn) ![(tc, u), (tx, x)] ↔ TseitinLitSem M ψ true tc tx u x

The literal that a satisfied clause needs to make true: whichever of posIn/negIn carries the positive Tseitin literals.

theorem DescriptiveComplexity.qbfT_lit_neg {L : FirstOrder.Language} (k : ℕ) (sw : Bool) (M : SOBlock) (ψ : (L.sum M.lang).Sentence) (mark : M.ι ⊕ (m : ℕ) × Tseitin.NodeAt ψ m → Fin k) {A : Type} [L.Structure A] [LinearOrder A] (tc tx : TseitinTag M ψ) (u x : Fin (tseitinDim M ψ) → A) : FirstOrder.Language.Structure.RelMap (if sw = true then FirstOrder.Language.qbfPosIn else FirstOrder.Language.qbfNegIn) ![(tc, u), (tx, x)] ↔ TseitinLitSem M ψ false tc tx u x

The literal that a satisfied clause needs to make false.

Correctness at a fixed valuation

The Tseitin correctness proof of DescriptiveComplexity.Problems.Sat.Hardness is stated with the truth assignment existentially quantified. Here the assignment is given, since the quantifier prefix of the QBF supplies it: the clauses of the encoding hold under val exactly when the induced valuation satisfies every gate and makes the root true.

theorem DescriptiveComplexity.qbfT_clauses_iff {L : FirstOrder.Language} (k : ℕ) (sw : Bool) (M : SOBlock) (ψ : (L.sum M.lang).Sentence) (mark : M.ι ⊕ (m : ℕ) × Tseitin.NodeAt ψ m → Fin k) {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (val : (qbfTseitinInterp k sw M ψ mark).Map A → Prop) : (∀ (c : (qbfTseitinInterp k sw M ψ mark).Map A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.qbfIsClause ![c] → ∃ (x : (qbfTseitinInterp k sw M ψ mark).Map A), FirstOrder.Language.Structure.RelMap (if sw = true then FirstOrder.Language.qbfNegIn else FirstOrder.Language.qbfPosIn) ![c, x] ∧ val x ∨ FirstOrder.Language.Structure.RelMap (if sw = true then FirstOrder.Language.qbfPosIn else FirstOrder.Language.qbfNegIn) ![c, x] ∧ ¬val x) ↔ (Tseitin.SatCond ψ ⋯ fun (vt : M.ι ⊕ (m : ℕ) × Tseitin.NodeAt ψ m) (x : Fin (tseitinDim M ψ) → A) => val (Sum.inr vt, x)) ∧ val (Sum.inr (Sum.inr ⟨0, Tseitin.rootAt ψ⟩), pad a₀ finZeroElim)

Correctness of the interpretation at a fixed valuation.

The reduction

theorem DescriptiveComplexity.pad_full {A : Type} {D : ℕ} (a₀ : A) (w : Fin D → A) : pad a₀ w = w

Padding a tuple that already has the interpretation's dimension does nothing.

theorem DescriptiveComplexity.altQuant_cast {A : Type} {m n : ℕ} (h : m = n) (P : (Fin n → A → Prop) → Prop) (pol : Bool) : altQuant A m (fun (νs : Fin m → A → Prop) => P fun (j : Fin n) => νs (Fin.cast ⋯ j)) pol ↔ altQuant A n P pol

Reindexing an alternating quantification along an equality of lengths.

def DescriptiveComplexity.qbfSwap (st : Bool) (Bs : List SOBlock) : Bool

Whether the innermost quantifier of an existentially-starting prefix with Bs.length + 1 blocks is universal – equivalently, whether Bs.length + 1 is even. The Tseitin gates can only be absorbed by an existential quantifier, so this is the flag that decides both the shape of the matrix and whether the kernel gets negated.

Equations

• DescriptiveComplexity.qbfSwap st Bs = !DescriptiveComplexity.innerPol Bs.length st

noncomputable def DescriptiveComplexity.qbfEnc {L : FirstOrder.Language} (st : Bool) (B : SOBlock) (Bs : List SOBlock) (φ : (soLang L (B :: Bs)).Sentence) : (L.sum (mergeBlocks (B :: Bs)).lang).Sentence

The sentence that is actually Tseitin-encoded: the merged kernel, negated when the innermost quantifier is universal.

Equations

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

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.qbfGt {L : FirstOrder.Language} (st : Bool) (B : SOBlock) (Bs : List SOBlock) (φ : (soLang L (B :: Bs)).Sentence) : SOBlock

The block of gate variables of the encoding.

Equations

• DescriptiveComplexity.qbfGt st B Bs φ = DescriptiveComplexity.gateBlock (DescriptiveComplexity.mergeBlocks (B :: Bs)) (DescriptiveComplexity.qbfEnc st B Bs φ)

noncomputable def DescriptiveComplexity.qbfMk {L : FirstOrder.Language} (st : Bool) (B : SOBlock) (Bs : List SOBlock) (φ : (soLang L (B :: Bs)).Sentence) : (mergeBlocks (B :: Bs)).ι ⊕ (m : ℕ) × Tseitin.NodeAt (qbfEnc st B Bs φ) m → Fin (Bs.length + 1)

The block marks of the interpreted instance: a relation variable is marked by the block it comes from, a gate variable by the innermost block.

Equations

• DescriptiveComplexity.qbfMk st B Bs φ vt = Fin.cast ⋯ (DescriptiveComplexity.markC (DescriptiveComplexity.qbfGt st B Bs φ) B Bs vt)

@[reducible]

noncomputable def DescriptiveComplexity.qbfRedInterp {L : FirstOrder.Language} (st : Bool) (B : SOBlock) (Bs : List SOBlock) (φ : (soLang L (B :: Bs)).Sentence) : FOInterpretation (L.sum FirstOrder.Language.order) (FirstOrder.Language.qbf (Bs.length + 1)) (TseitinTag (mergeBlocks (B :: Bs)) (qbfEnc st B Bs φ)) (tseitinDim (mergeBlocks (B :: Bs)) (qbfEnc st B Bs φ))

The interpretation of the reduction: the Tseitin encoding of the merged kernel, with block marks. Reducible, so that the characterizations of DescriptiveComplexity.qbfTseitinInterp apply to it directly.

Equations

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

theorem DescriptiveComplexity.qbfSwap_true_eq (Bs : List SOBlock) : qbfSwap true Bs = !(Bs.length + 1) % 2 == 1

The swap flag is the parity of the number of blocks: with an existential outermost block, the matrix of DescriptiveComplexity.QBF k is disjunctive exactly when a swap is needed.

theorem DescriptiveComplexity.qbfSwap_false_eq (Bs : List SOBlock) : qbfSwap false Bs = !(Bs.length + 1) % 2 == 0

Dually, with a universal outermost block.

theorem DescriptiveComplexity.realize_eq_realizeWith {L : FirstOrder.Language} {A : Type} [L.Structure A] {M : SOBlock} (μ : M.Assignment A) (χ : (L.sum M.lang).Sentence) : A ⊨ χ ↔ Tseitin.RealizeWith μ χ finZeroElim

Realization of a sentence in the expansion by an assignment is DescriptiveComplexity.Tseitin.RealizeWith.

theorem DescriptiveComplexity.exists_gates {L : FirstOrder.Language} {A : Type} [L.Structure A] {M : SOBlock} (a₀ : A) (μ : M.Assignment A) (χ : (L.sum M.lang).Sentence) : (∃ (g : (gateBlock M χ).Assignment A), (Tseitin.Gates μ χ fun (m : ℕ) (q : Tseitin.NodeAt χ m) (w : Fin m → A) => g ⟨m, q⟩ (pad a₀ w)) ∧ Tseitin.RealizeWith μ χ finZeroElim) ↔ Tseitin.RealizeWith μ χ finZeroElim

The gates are functionally determined: some gate valuation satisfies every gate, so quantifying them existentially adds nothing.

noncomputable def DescriptiveComplexity.qbfRd {L : FirstOrder.Language} (st : Bool) (B : SOBlock) (Bs : List SOBlock) (φ : (soLang L (B :: Bs)).Sentence) {A : Type} (a₀ : A) : BlockRead A ((qbfRedInterp st B Bs φ).Map A) (consLast (qbfGt st B Bs φ) B Bs)

The reading of the interpreted instance: each propositional variable is read at its canonically padded tuple.

Equations

• DescriptiveComplexity.qbfRd st B Bs φ a₀ i ν a = ν (Sum.inr (DescriptiveComplexity.splitIdx (DescriptiveComplexity.qbfGt st B Bs φ) B Bs i), DescriptiveComplexity.pad a₀ a)

theorem DescriptiveComplexity.qbf_inner {L : FirstOrder.Language} (st : Bool) (B : SOBlock) (Bs : List SOBlock) (φ : (soLang L (B :: Bs)).Sentence) {A : Type} [L.Structure A] (a₀ : A) (μ : (mergeBlocks (B :: Bs)).Assignment A) : (quantB (innerPol Bs.length st) fun (g : (qbfGt st B Bs φ).Assignment A) => xorP (qbfSwap st Bs) ((Tseitin.Gates μ (qbfEnc st B Bs φ) fun (m : ℕ) (q : Tseitin.NodeAt (qbfEnc st B Bs φ) m) (w : Fin m → A) => g ⟨m, q⟩ (pad a₀ w)) ∧ Tseitin.RealizeWith μ (qbfEnc st B Bs φ) finZeroElim)) ↔ Tseitin.RealizeWith μ ((mergeHom (B :: Bs) L).onSentence φ) finZeroElim

The innermost quantifier absorbs the gates: quantifying the gate block with the innermost polarity, over the Tseitin condition, is exactly the truth of the merged kernel. When the innermost quantifier is existential this is DescriptiveComplexity.exists_gates; when it is universal it is the same fact under the negation that the swapped encoding introduces.

theorem DescriptiveComplexity.qbfRed_correct {L : FirstOrder.Language} (st : Bool) (B : SOBlock) (Bs : List SOBlock) (φ : (soLang L (B :: Bs)).Sentence) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : (QbfProblem (Bs.length + 1) st !qbfSwap st Bs).Holds ((qbfRedInterp st B Bs φ).Map A) ↔ SORealize L A (B :: Bs) φ st

Correctness of the reduction: the interpreted quantified Boolean formula is true exactly when the second-order sentence holds.

noncomputable def DescriptiveComplexity.qbfReduction {L : FirstOrder.Language} (st : Bool) (B : SOBlock) (Bs : List SOBlock) (φ : (soLang L (B :: Bs)).Sentence) (Q : DecisionProblem L) (hφ : ∀ (A : Type) [inst : L.Structure A] [Finite A] [Nonempty A], Q.Holds A ↔ SORealize L A (B :: Bs) φ st) : OrderedFOReduction Q (QbfProblem (Bs.length + 1) st !qbfSwap st Bs)

The generic marked Tseitin reduction: an ordered first-order reduction to a quantified Boolean formula problem, from any problem defined on nonempty finite structures by a second-order sentence with a nonempty prefix.

Equations

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

Hardness

theorem DescriptiveComplexity.qbf_hard_of_sigmaSODefinable (k : ℕ) {L : FirstOrder.Language} (Q : DecisionProblem L) : SigmaSODefinable (k + 1) Q → Nonempty (OrderedFOReduction Q (QBF (k + 1)))

Hardness of QBF: every problem definable by a second-order sentence with k + 1 alternating blocks starting existentially admits an ordered first-order reduction to DescriptiveComplexity.QBF (k + 1).

This is the Cook–Levin discharge one level up: the quantifier prefix is merged into a single block, its first-order kernel is Tseitin-translated into a CNF instance inside an ordered input structure, and the propositional variables are marked with the block they belong to – the gate variables with the innermost one, which is why the matrix and the encoded sentence follow the parity of k + 1.

theorem DescriptiveComplexity.qbfPi_hard_of_piSODefinable (k : ℕ) {L : FirstOrder.Language} (Q : DecisionProblem L) : PiSODefinable (k + 1) Q → Nonempty (OrderedFOReduction Q (QBFPi (k + 1)))

Hardness of the dual: every problem definable by a second-order sentence with k + 1 alternating blocks starting universally admits an ordered first-order reduction to DescriptiveComplexity.QBFPi (k + 1).

This is the same construction at the other starting polarity. The parity of the matrix flips with it: the innermost quantifier of a universally-starting prefix of k + 1 blocks is existential exactly when k + 1 is even, so QBFPi k takes a conjunctive matrix for even k and a disjunctive one for odd k – the mirror image of DescriptiveComplexity.QBF.