[Model] QuantifiedBooleanFormulas(qbf)(*)

[isPANN]

Motivation

QUANTIFIED BOOLEAN FORMULAS (QBF) (*) (P263) from Garey & Johnson, A9 LO11. The canonical PSPACE-complete problem: given a fully quantified Boolean formula with alternating universal and existential quantifiers, determine whether it is true. QBF serves as the primary source of PSPACE-completeness reductions for combinatorial game problems and is the analogue of SAT for PSPACE.

Associated rules:

• As source:
  • R182: QBF -> GENERALIZED HEX (PSPACE-completeness of the Shannon switching game on vertices)
  • R183: QBF -> GENERALIZED GEOGRAPHY (PSPACE-completeness of the move-based graph traversal game)
  • R184: QBF -> GENERALIZED KAYLES (PSPACE-completeness of the vertex-removal game)
  • R185: QBF -> SEQUENTIAL TRUTH ASSIGNMENT
  • R186: QBF -> VARIABLE PARTITION TRUTH ASSIGNMENT
  • R187: QBF -> SIFT
  • R188: QBF -> ALTERNATING HITTING SET
  • R189: QBF -> ALTERNATING MAXIMUM WEIGHTED MATCHING
  • R210: QBF -> MODAL LOGIC PROVABILITY
• As target:
  • R207: (generic transformation) -> QBF (Stockmeyer and Meyer, 1973)

Definition

Name: QuantifiedBooleanFormulas

Reference: Garey & Johnson, Computers and Intractability, A9 LO11

Mathematical definition:

INSTANCE: Set U={u_1,u_2,...,u_n} of variables, well-formed quantified Boolean formula F=(Q_1u_1)(Q_2u_2)···(Q_nu_n)E, where E is a Boolean expression and each Q_i is either ∀ or ∃.
QUESTION: Is F true?

Variables

• Count: n = |U| (one variable per Boolean variable in the quantifier prefix)
• Per-variable domain: {0, 1} — representing FALSE and TRUE respectively
• Meaning: x_i in {0, 1} is the truth assignment for variable u_i. A configuration is a full assignment to all n variables. evaluate() checks whether the CNF matrix E is satisfied under the given assignment (consistent with the SAT pattern). Quantifier semantics (∃/∀ branching) are handled by the solver, not by evaluate().

Schema (data type)

Type name: QuantifiedBooleanFormulas
Variants: none (operates on a general quantified Boolean formula)

Field	Type	Description
num_vars	usize	Number of variables n = |U| (stored field, consistent with Satisfiability)
quantifiers	Vec<Quantifier>	Quantifier for each variable: Exists or ForAll, length n
clauses	Vec<CNFClause>	CNF representation of the Boolean expression E; reuses CNFClause from Satisfiability

Where Quantifier is an enum { Exists, ForAll } and CNFClause is reused from the existing Satisfiability model.

Derived getters:

• num_clauses() → self.clauses.len() — number of clauses in the CNF matrix E

Complexity

• Best known exact algorithm: The naive recursive algorithm evaluates QBF in O(2^n) time and O(n) space by branching on each quantified variable. For QBF with CNF matrix having m clauses, Williams (2002) achieves O(1.709^m) time. For general quantified CNFs of size poly(n) on n variables with O(1) quantifier alternations, Santhanam and Williams (2013) achieve 2^(n - n^{Omega(1)}) randomized time, the first known improvement over brute force for bounded-alternation QBF. The problem is PSPACE-complete (Stockmeyer and Meyer, 1973), so no polynomial-time algorithm is expected.
• declare_variants! complexity string: "2^num_vars"

Extra Remark

Full book text:

INSTANCE: Set U={u_1,u_2,...,u_n} of variables, well-formed quantified Boolean formula F=(Q_1u_1)(Q_2u_2)···(Q_nu_n)E, where E is a Boolean expression and each Q_i is either ∀ or ∃.
QUESTION: Is F true?
Reference: [Stockmeyer and Meyer, 1973]. Generic transformation.
Comment: PSPACE-complete, even if E is in conjunctive normal form with three literals per clause (QUANTIFIED 3SAT), but solvable in polynomial time when there are at most two literals per clause [Schaefer, 1978b]. If F is restricted to at most k alternations of quantifiers (i.e., there are at most k indices i such that Q_i≠Q_{i+1}), then the restricted problem is complete for some class in the polynomial hierarchy, depending on k and the allowed values for Q_1 (see Section 7.2).

How to solve

• It can be solved by (existing) bruteforce. (BruteForce enumerates all 2^n truth assignments and evaluate() checks CNF matrix satisfaction without exploiting quantifier structure. This is correct for satisfaction checking but does not leverage the quantifier prefix for pruning.)
• It can be solved by reducing to integer programming.
• Other: A dedicated QBF solver (e.g., QDPLL with clause/cube learning, or CEGAR-based solvers) could be added to exploit quantifier structure for more efficient solving.

Example Instance

Input:
U = {u_1, u_2, u_3, u_4, u_5, u_6}
F = EXISTS u_1 FORALL u_2 EXISTS u_3 FORALL u_4 EXISTS u_5 FORALL u_6
[(u_1 OR u_2 OR u_3) AND (NOT u_1 OR NOT u_4 OR u_5) AND (u_2 OR NOT u_3 OR u_6) AND (NOT u_5 OR NOT u_6 OR u_4)]

Quantifiers: [EXISTS, FORALL, EXISTS, FORALL, EXISTS, FORALL]
Clauses (CNF):

• C_1 = (u_1, u_2, u_3)
• C_2 = (NOT u_1, NOT u_4, u_5)
• C_3 = (u_2, NOT u_3, u_6)
• C_4 = (NOT u_5, NOT u_6, u_4)

Evaluation:
Set u_1 = TRUE. Then:

• C_1 = TRUE (u_1 = T). C_2 = (F OR NOT u_4 OR u_5).
• For any u_2:
  • Set u_3 = TRUE. C_3 = (u_2 OR F OR u_6). If u_2 = FALSE, need u_6 to be TRUE for C_3, but u_6 is universally quantified.
  • Set u_3 = FALSE instead. C_3 = (u_2 OR T OR u_6) = TRUE.
  • For any u_4:
    • C_2 = (F OR NOT u_4 OR u_5). If u_4 = TRUE, need u_5 = TRUE. If u_4 = FALSE, C_2 = TRUE.
    • Set u_5 = TRUE when u_4 = TRUE (C_2 = T), set u_5 = FALSE when u_4 = FALSE (C_2 = T).
    • C_4 = (NOT u_5 OR NOT u_6 OR u_4).
      • u_4 = TRUE, u_5 = TRUE: C_4 = (F OR NOT u_6 OR T) = TRUE for any u_6.
      • u_4 = FALSE, u_5 = FALSE: C_4 = (T OR NOT u_6 OR F) = TRUE for any u_6.

Answer: TRUE -- the existential player has a winning strategy.

[zazabap]

Issue Quality Check — Model

Check	Result	Details
Usefulness	✅ Pass	Novel problem not yet in reduction graph; canonical PSPACE-complete problem with 9+ planned reductions
Non-trivial	✅ Pass	Genuinely distinct from SAT/kSAT — quantifier alternation creates fundamentally different evaluation semantics
Correctness	⚠️ Warn	References verified but complexity section has minor issues (see below)
Well-written	⚠️ Warn	Mostly complete but some gaps in schema and complexity specification

Overall: 2 passed, 0 failed, 2 warnings

---

Usefulness

QuantifiedBooleanFormulas does not exist in the codebase. The motivation is strong: QBF is the canonical PSPACE-complete problem and serves as the source for reductions to combinatorial game problems. The issue lists 9 outgoing and 1 incoming reduction rule, providing good graph connectivity. The problem fills a clear gap — the project currently has no PSPACE-complete problems.

Non-trivial

QBF is genuinely distinct from all existing problems. While it shares CNF structure with Satisfiability and KSatisfiability, the addition of universal quantifiers fundamentally changes the evaluation semantics from "exists a satisfying assignment" to "exists a winning strategy in a two-player game." This is not a variant or restriction of any existing problem.

Correctness

References verified:

• Stockmeyer & Meyer (1973): Confirmed. "Word Problems Requiring Exponential Time: Preliminary Report" — established PSPACE-completeness of QBF. Published at STOC 1973.
• Williams (2002): Confirmed. "Algorithms for Quantified Boolean Formulas" — achieves O(1.709^m) time for QBF with m clauses in CNF. Published at SODA 2002.
• Schaefer (1978b): The claim that QBF with at most 2 literals per clause is polynomial-time solvable is a well-known result consistent with Schaefer's dichotomy theorem.

Minor issues:

• The bounded-alternation result 2^(n - n^{Omega(1)}) is from Santhanam & Williams (2013), "New Algorithms for QBF Satisfiability and Implications for Circuit Complexity" (ECCC TR13-108). The issue attributes this only to "Williams" without co-author Santhanam and without a year. The Omega notation is inherent to the result statement, so it cannot be replaced with a concrete numeric value — this means it should not be used directly in a declare_variants! complexity string.
• The issue needs a concrete complexity string for declare_variants!. Since the best general exact algorithm is brute-force O(2^n), the complexity string would be "2^num_vars". The 1.709^m result is parameterized by clauses rather than variables, making it an alternative but not necessarily better bound.

Well-written

Strengths:

• Mathematical definition is clear and well-formed
• Example instance is non-trivial (6 variables, 4 clauses, alternating quantifiers) with a fully worked evaluation
• Symbol usage (U, F, Q_i, E) is consistent across sections
• Brute-force solver approach is correctly identified

Issues to address:

1. Schema field num_vars: This is redundant since it equals quantifiers.len(). Consider removing it or making it a derived getter rather than a stored field. Existing problems like Satisfiability store num_vars explicitly, so this may be acceptable for consistency — but it should be noted.

2. Missing num_clauses in schema fields: The overhead expressions for reductions will likely need num_clauses as a getter. The schema table should list the size fields that will be used in complexity/overhead expressions.

3. Complexity string ambiguity: The Complexity section mixes three different results without clearly stating which one will be used for declare_variants!. For implementation, a concrete string like "2^num_vars" is needed.

4. Brute-force description is slightly misleading: The issue says "Runtime O(2^n), space O(n)" but QBF brute force is actually game-tree search (minimax-style recursion), not exhaustive enumeration of all 2^n assignments. The runtime is still O(2^n) in the worst case, but the description should clarify this is recursive evaluation, not enumeration — since the SatisfactionProblem trait's dims() returns [2; n] which would enumerate all 2^n assignments, but most of them are meaningless for QBF (the universal quantifier semantics are lost).

5. Important design consideration: QBF evaluation via the Problem trait is non-trivial. The evaluate() method receives a single configuration Vec<usize> of length n. For satisfaction problems, it returns bool. But QBF truth depends on all possible assignments to universal variables for each existential strategy — a single assignment vector does not capture the game-tree semantics. The implementation will need to either: (a) treat each config as a full assignment and return whether the formula is satisfied under that assignment (losing the quantifier semantics to brute-force enumeration), or (b) adopt a different approach. This is a fundamental design question that should be addressed in the issue.

Recommendations

• Clarify how evaluate() will handle quantifier semantics — will it evaluate the formula under a fixed assignment (ignoring quantifiers), or implement game-tree evaluation?
• Add a concrete declare_variants! complexity string proposal (e.g., "2^num_vars")
• Credit Santhanam as co-author on the bounded-alternation result
• Consider whether Literal should reuse the existing CNFClause type from Satisfiability or define its own

[zazabap]

Changelog — Issue body updated

The following fixes were applied to the issue body:

Mechanical fixes

1. Bounded-alternation credit: Changed "Williams" to "Santhanam and Williams (2013)" for the bounded-alternation QBF result.
2. Derived getter: Added num_clauses() as a derived getter in the Schema section (self.clauses.len()).
3. Complexity string: Added explicit declare_variants! complexity string "2^num_vars".

Substantive changes

4. evaluate() semantics (Q1 → A): Updated Variables section to clarify that a configuration is a full assignment to all n variables, evaluate() checks CNF matrix satisfaction only, and quantifier semantics (∃/∀ branching) are handled by the solver, not evaluate(). This is consistent with the SAT pattern.
5. num_vars storage (Q2 → A): Kept num_vars as a stored field for consistency with Satisfiability. Added clarifying note in schema table.
6. Clause type (Q3 → A): Changed clauses field type from Vec<Vec<Literal>> to Vec<CNFClause>, reusing CNFClause from Satisfiability. Removed the standalone Literal struct description.
7. Brute-force description (Q4): Updated "How to solve" to note that BruteForce enumerates all 2^n assignments and evaluate() checks CNF matrix satisfaction without exploiting quantifier structure. Added note that a dedicated QBF solver could be added under "Other".