Fix #571: Add QuantifiedBooleanFormulas model

docs/paper/examples/maximumindependentset_to_maximumclique.json

@@ -31,8 +31,8 @@
   "target": {
     "problem": "MaximumClique",
     "variant": {
-      "weight": "i32",
-      "graph": "SimpleGraph"
+      "graph": "SimpleGraph",
+      "weight": "i32"
     },
     "instance": {
       "edges": [

docs/paper/reductions.typ

@@ -55,6 +55,7 @@
   "ClosestVectorProblem": [Closest Vector Problem],
   "SubsetSum": [Subset Sum],
   "MinimumFeedbackVertexSet": [Minimum Feedback Vertex Set],
+  "QuantifiedBooleanFormulas": [Quantified Boolean Formulas (QBF)],
 )
 
 // Definition label: "def:<ProblemName>" — each definition block must have a matching label
@@ -821,6 +822,14 @@ Circuit Satisfiability is the most natural NP-complete problem: the Cook-Levin t
 ) <fig:circuit-sat>
 ]
 
+#problem-def("QuantifiedBooleanFormulas")[
+  Given a set $U = {u_1, dots, u_n}$ of Boolean variables and a fully quantified Boolean formula $F = (Q_1 u_1)(Q_2 u_2) dots.c (Q_n u_n) E$, where each $Q_i in {exists, forall}$ is a quantifier and $E$ is a Boolean expression in CNF with $m$ clauses, determine whether $F$ is true.
+][
+Quantified Boolean Formulas (QBF) is the canonical PSPACE-complete problem, established by #cite(<stockmeyer1973>, form: "prose"). QBF generalizes SAT by adding universal quantifiers ($forall$) alongside existential ones ($exists$), creating a two-player game semantics: the existential player chooses values for $exists$-variables, the universal player for $forall$-variables, and the formula is true iff the existential player has a winning strategy ensuring all clauses are satisfied. This quantifier alternation is the source of PSPACE-hardness and makes QBF the primary source of PSPACE-completeness reductions for combinatorial game problems. The problem remains PSPACE-complete even when $E$ is restricted to 3-CNF (Quantified 3-SAT), but is polynomial-time solvable when each clause has at most 2 literals @schaefer1978. The best known exact algorithm is brute-force game-tree evaluation in $O^*(2^n)$ time. For QBF with $m$ CNF clauses, #cite(<williams2002>, form: "prose") achieves $O^*(1.709^m)$ time.
+
+*Example.* Consider $F = exists u_1 space forall u_2 space [(u_1 or u_2) and (u_1 or not u_2)]$ with $n = 2$ variables and $m = 2$ clauses. Setting $u_1 = 1$: clause $C_1 = (1 or u_2) = 1$ and $C_2 = (1 or not u_2) = 1$ for any $u_2$. Hence $F$ is true -- the existential player wins by choosing $u_1 = 1$. In contrast, $F' = forall u_1 space exists u_2 space [(u_1) and (not u_1)]$ is false: when $u_1 = 0$, clause $(u_1)$ fails regardless of $u_2$.
+]
+
 #problem-def("Factoring")[
   Given a composite integer $N$ and bit sizes $m, n$, find integers $p in [2, 2^m - 1]$ and $q in [2, 2^n - 1]$ such that $p times q = N$. Here $p$ has $m$ bits and $q$ has $n$ bits.
 ][

docs/paper/references.bib

@@ -456,3 +456,29 @@ @article{cygan2014
   note    = {Conference version: STOC 2014},
   doi     = {10.1137/140990255}
 }
+
+@inproceedings{stockmeyer1973,
+  author    = {Larry J. Stockmeyer and Albert R. Meyer},
+  title     = {Word Problems Requiring Exponential Time: Preliminary Report},
+  booktitle = {Proceedings of the 5th Annual ACM Symposium on Theory of Computing (STOC)},
+  pages     = {1--9},
+  year      = {1973},
+  doi       = {10.1145/800125.804029}
+}
+
+@inproceedings{williams2002,
+  author    = {Ryan Williams},
+  title     = {Algorithms for Quantified Boolean Formulas},
+  booktitle = {Proceedings of the 13th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA)},
+  pages     = {299--307},
+  year      = {2002}
+}
+
+@article{schaefer1978,
+  author  = {Thomas J. Schaefer},
+  title   = {The Complexity of Satisfiability Problems},
+  journal = {Conference Record of the 10th Annual ACM Symposium on Theory of Computing (STOC)},
+  pages   = {216--226},
+  year    = {1978},
+  doi     = {10.1145/800133.804350}
+}

docs/plans/2026-03-13-quantified-boolean-formulas-model.md

@@ -0,0 +1,99 @@
+# Plan: Add QuantifiedBooleanFormulas Model
+
+**Issue:** #571 — [Model] QuantifiedBooleanFormulas(qbf)(*)
+**Skill:** add-model
+
+## Information Checklist
+
+| # | Item | Value |
+|---|------|-------|
+| 1 | Problem name | `QuantifiedBooleanFormulas` |
+| 2 | Mathematical definition | Given a fully quantified Boolean formula F=(Q_1 u_1)...(Q_n u_n)E where each Q_i is ∀ or ∃ and E is a CNF formula, determine whether F is true |
+| 3 | Problem type | Satisfaction (Metric = bool) |
+| 4 | Type parameters | None |
+| 5 | Struct fields | `num_vars: usize`, `quantifiers: Vec<Quantifier>`, `clauses: Vec<CNFClause>` |
+| 6 | Configuration space | `vec![2; num_vars]` — each variable is 0 or 1 |
+| 7 | Feasibility check | A config represents a full assignment; evaluate returns true iff the formula is true under that assignment (ignoring quantifier semantics in evaluate — quantifier semantics are captured by the brute-force solver's game-tree search) |
+| 8 | Objective function | `bool` — satisfied or not under the given assignment |
+| 9 | Best known exact algorithm | O(2^n) brute-force game-tree evaluation (Stockmeyer & Meyer, 1973); complexity string: `"2^num_vars"` |
+| 10 | Solving strategy | BruteForce works — but needs special handling: `find_satisfying` must find a *witnessing assignment* for the existential variables such that for all universal variable assignments, E is satisfied. The `evaluate()` method just checks if a single full assignment satisfies the CNF matrix E (standard SAT-like evaluation). |
+| 11 | Category | `formula` |
+
+## Design Decisions
+
+### evaluate() Semantics
+Following the check-issue comment's analysis, `evaluate()` will treat the config as a full assignment and check whether the CNF matrix E is satisfied. This is consistent with how the `Problem` trait works (a single config → metric). The quantifier semantics are implicit: a QBF is TRUE iff there exists an assignment to existential variables such that for ALL universal variable assignments, E evaluates to true. The brute-force solver enumerates all 2^n assignments and returns any satisfying one.
+
+### Quantifier Enum
+Define a `Quantifier` enum with `Exists` and `ForAll` variants, serializable with serde.
+
+### Reusing CNFClause
+Reuse the existing `CNFClause` type from `sat.rs` (1-indexed signed integers).
+
+## Steps
+
+### Step 1: Implement the model (`src/models/formula/qbf.rs`)
+
+1. Define `Quantifier` enum: `{ Exists, ForAll }` with `Debug, Clone, PartialEq, Eq, Serialize, Deserialize`
+2. Define `QuantifiedBooleanFormulas` struct with fields: `num_vars`, `quantifiers`, `clauses`
+3. Add `inventory::submit!` for `ProblemSchemaEntry`
+4. Constructor: `new(num_vars, quantifiers, clauses)` with assertion that `quantifiers.len() == num_vars`
+5. Getter methods: `num_vars()`, `num_clauses()`, `quantifiers()`, `clauses()`
+6. Implement `Problem` trait:
+   - `NAME = "QuantifiedBooleanFormulas"`
+   - `Metric = bool`
+   - `dims() = vec![2; num_vars]`
+   - `evaluate(config)` — convert to bool assignment, check if all clauses are satisfied (same as SAT)
+   - `variant() = variant_params![]`
+7. Implement `SatisfactionProblem` (marker trait)
+8. Add `declare_variants!` with complexity `"2^num_vars"`
+9. Add `is_true(&self) -> bool` method that implements proper QBF game-tree evaluation (recursive minimax)
+10. Link test file: `#[cfg(test)] #[path = "../../unit_tests/models/formula/qbf.rs"] mod tests;`
+
+### Step 2: Register the model
+
+1. `src/models/formula/mod.rs` — add `pub(crate) mod qbf;` and `pub use qbf::{QuantifiedBooleanFormulas, Quantifier};`
+2. `src/models/mod.rs` — add `QuantifiedBooleanFormulas, Quantifier` to the formula re-export line
+3. `src/lib.rs` prelude — add `QuantifiedBooleanFormulas` to the formula prelude exports
+
+### Step 3: Register in CLI
+
+1. `problemreductions-cli/src/dispatch.rs`:
+   - Add import for `QuantifiedBooleanFormulas`
+   - Add `"QuantifiedBooleanFormulas" => deser_sat::<QuantifiedBooleanFormulas>(data)` in `load_problem()`
+   - Add `"QuantifiedBooleanFormulas" => try_ser::<QuantifiedBooleanFormulas>(any)` in `serialize_any_problem()`
+2. `problemreductions-cli/src/problem_name.rs`:
+   - Add `"qbf" | "quantifiedbooleanformulas" => "QuantifiedBooleanFormulas".to_string()` in `resolve_alias()`
+   - Add `("QBF", "QuantifiedBooleanFormulas")` to `ALIASES` array
+
+### Step 4: Add CLI creation support
+
+1. `problemreductions-cli/src/commands/create.rs`:
+   - Add `"QuantifiedBooleanFormulas"` match arm: parse `--num-vars`, `--clauses`, and a new `--quantifiers` flag
+   - Add to `example_for()`: `"QuantifiedBooleanFormulas" => "--num-vars 3 --clauses \"1,2;-1,3\" --quantifiers \"E,A,E\""`
+2. `problemreductions-cli/src/cli.rs`:
+   - Add `--quantifiers` flag to `CreateArgs`: `pub quantifiers: Option<String>`
+   - Update `all_data_flags_empty()` to include `args.quantifiers.is_none()`
+   - Add QBF to "Flags by problem type" table
+
+### Step 5: Write unit tests (`src/unit_tests/models/formula/qbf.rs`)
+
+1. `test_quantifier_creation` — verify Quantifier enum
+2. `test_qbf_creation` — construct instance, verify dimensions
+3. `test_qbf_evaluate` — verify evaluate() on valid/invalid assignments
+4. `test_qbf_is_true` — verify game-tree evaluation for known true/false instances
+5. `test_qbf_solver` — verify brute-force solver finds satisfying assignments
+6. `test_qbf_serialization` — round-trip serde test
+7. `test_qbf_trivial` — empty formula, all-exists (reduces to SAT)
+
+### Step 6: Document in paper
+
+Add problem-def entry in `docs/paper/reductions.typ`:
+- Add display name: `"QuantifiedBooleanFormulas": [Quantified Boolean Formulas (QBF)]`
+- Add `#problem-def("QuantifiedBooleanFormulas")[...]` with formal definition and background
+
+### Step 7: Verify
+
+```bash
+make test clippy fmt-check
+```

problemreductions-cli/src/cli.rs

@@ -218,6 +218,7 @@ Flags by problem type:
   BMF                             --matrix (0/1), --rank
   CVP                             --basis, --target-vec [--bounds]
   FVS                             --arcs [--weights] [--num-vertices]
+  QBF                             --num-vars, --clauses, --quantifiers
   ILP, CircuitSAT                 (via reduction only)
 
 Geometry graph variants (use slash notation, e.g., MIS/KingsSubgraph):
@@ -332,6 +333,9 @@ pub struct CreateArgs {
     /// Directed arcs for directed graph problems (e.g., 0>1,1>2,2>0)
     #[arg(long)]
     pub arcs: Option<String>,
+    /// Quantifiers for QBF (comma-separated, E=Exists, A=ForAll, e.g., "E,A,E")
+    #[arg(long)]
+    pub quantifiers: Option<String>,
 }
 
 #[derive(clap::Args)]

problemreductions-cli/src/commands/create.rs

@@ -5,6 +5,7 @@ use crate::problem_name::{parse_problem_spec, resolve_variant};
 use crate::util;
 use anyhow::{bail, Context, Result};
 use problemreductions::models::algebraic::{ClosestVectorProblem, BMF};
+use problemreductions::models::formula::Quantifier;
 use problemreductions::models::graph::GraphPartitioning;
 use problemreductions::models::misc::{BinPacking, PaintShop};
 use problemreductions::prelude::*;
@@ -48,6 +49,7 @@ fn all_data_flags_empty(args: &CreateArgs) -> bool {
         && args.target_vec.is_none()
         && args.bounds.is_none()
         && args.arcs.is_none()
+        && args.quantifiers.is_none()
 }
 
 fn type_format_hint(type_name: &str, graph_type: Option<&str>) -> &'static str {
@@ -82,6 +84,9 @@ fn example_for(canonical: &str, graph_type: Option<&str>) -> &'static str {
             "--graph 0-1,1-2,2-3 --edge-weights 1,1,1"
         }
         "Satisfiability" => "--num-vars 3 --clauses \"1,2;-1,3\"",
+        "QuantifiedBooleanFormulas" => {
+            "--num-vars 3 --clauses \"1,2;-1,3\" --quantifiers \"E,A,E\""
+        }
         "KSatisfiability" => "--num-vars 3 --clauses \"1,2,3;-1,2,-3\" --k 3",
         "QUBO" => "--matrix \"1,0.5;0.5,2\"",
         "SpinGlass" => "--graph 0-1,1-2 --couplings 1,1",
@@ -264,6 +269,26 @@ pub fn create(args: &CreateArgs, out: &OutputConfig) -> Result<()> {
             util::ser_ksat(num_vars, clauses, k)?
         }
 
+        // QBF
+        "QuantifiedBooleanFormulas" => {
+            let num_vars = args.num_vars.ok_or_else(|| {
+                anyhow::anyhow!(
+                    "QuantifiedBooleanFormulas requires --num-vars, --clauses, and --quantifiers\n\n\
+                     Usage: pred create QBF --num-vars 3 --clauses \"1,2;-1,3\" --quantifiers \"E,A,E\""
+                )
+            })?;
+            let clauses = parse_clauses(args)?;
+            let quantifiers = parse_quantifiers(args, num_vars)?;
+            (
+                ser(QuantifiedBooleanFormulas::new(
+                    num_vars,
+                    quantifiers,
+                    clauses,
+                ))?,
+                resolved_variant.clone(),
+            )
+        }
+
         // QUBO
         "QUBO" => {
             let matrix = parse_matrix(args)?;
@@ -890,6 +915,36 @@ fn parse_matrix(args: &CreateArgs) -> Result<Vec<Vec<f64>>> {
         .collect()
 }
 
+/// Parse `--quantifiers` as comma-separated quantifier labels (E/A or Exists/ForAll).
+/// E.g., "E,A,E" or "Exists,ForAll,Exists"
+fn parse_quantifiers(args: &CreateArgs, num_vars: usize) -> Result<Vec<Quantifier>> {
+    let q_str = args
+        .quantifiers
+        .as_deref()
+        .ok_or_else(|| anyhow::anyhow!("QBF requires --quantifiers (e.g., \"E,A,E\")"))?;
+
+    let quantifiers: Vec<Quantifier> = q_str
+        .split(',')
+        .map(|s| match s.trim().to_lowercase().as_str() {
+            "e" | "exists" => Ok(Quantifier::Exists),
+            "a" | "forall" => Ok(Quantifier::ForAll),
+            other => Err(anyhow::anyhow!(
+                "Invalid quantifier '{}': expected E/Exists or A/ForAll",
+                other
+            )),
+        })
+        .collect::<Result<Vec<_>>>()?;
+
+    if quantifiers.len() != num_vars {
+        bail!(
+            "Expected {} quantifiers but got {}",
+            num_vars,
+            quantifiers.len()
+        );
+    }
+    Ok(quantifiers)
+}
+
 /// Handle `pred create <PROBLEM> --random ...`
 fn create_random(
     args: &CreateArgs,

problemreductions-cli/src/dispatch.rs

@@ -226,6 +226,7 @@ pub fn load_problem(
             _ => deser_opt::<SpinGlass<SimpleGraph, i32>>(data),
         },
         "Satisfiability" => deser_sat::<Satisfiability>(data),
+        "QuantifiedBooleanFormulas" => deser_sat::<QuantifiedBooleanFormulas>(data),
         "KSatisfiability" => match variant.get("k").map(|s| s.as_str()) {
             Some("K2") => deser_sat::<KSatisfiability<K2>>(data),
             Some("K3") => deser_sat::<KSatisfiability<K3>>(data),
@@ -289,6 +290,7 @@ pub fn serialize_any_problem(
             _ => try_ser::<SpinGlass<SimpleGraph, i32>>(any),
         },
         "Satisfiability" => try_ser::<Satisfiability>(any),
+        "QuantifiedBooleanFormulas" => try_ser::<QuantifiedBooleanFormulas>(any),
         "KSatisfiability" => match variant.get("k").map(|s| s.as_str()) {
             Some("K2") => try_ser::<KSatisfiability<K2>>(any),
             Some("K3") => try_ser::<KSatisfiability<K3>>(any),

problemreductions-cli/src/problem_name.rs

@@ -22,6 +22,7 @@ pub const ALIASES: &[(&str, &str)] = &[
     ("CVP", "ClosestVectorProblem"),
     ("MaxMatching", "MaximumMatching"),
     ("FVS", "MinimumFeedbackVertexSet"),
+    ("QBF", "QuantifiedBooleanFormulas"),
 ];
 
 /// Resolve a short alias to the canonical problem name.
@@ -56,6 +57,7 @@ pub fn resolve_alias(input: &str) -> String {
         "knapsack" => "Knapsack".to_string(),
         "fvs" | "minimumfeedbackvertexset" => "MinimumFeedbackVertexSet".to_string(),
         "subsetsum" => "SubsetSum".to_string(),
+        "qbf" | "quantifiedbooleanformulas" => "QuantifiedBooleanFormulas".to_string(),
         _ => input.to_string(), // pass-through for exact names
     }
 }

src/lib.rs

@@ -39,7 +39,9 @@ pub mod variant;
 pub mod prelude {
     // Problem types
     pub use crate::models::algebraic::{BMF, QUBO};
-    pub use crate::models::formula::{CNFClause, CircuitSAT, KSatisfiability, Satisfiability};
+    pub use crate::models::formula::{
+        CNFClause, CircuitSAT, KSatisfiability, QuantifiedBooleanFormulas, Satisfiability,
+    };
     pub use crate::models::graph::{BicliqueCover, GraphPartitioning, SpinGlass};
     pub use crate::models::graph::{
         KColoring, MaxCut, MaximalIS, MaximumClique, MaximumIndependentSet, MaximumMatching,

src/models/formula/mod.rs

@@ -4,11 +4,14 @@
 //! - [`Satisfiability`]: Boolean satisfiability (SAT) with CNF clauses
 //! - [`KSatisfiability`]: K-SAT where each clause has exactly K literals
 //! - [`CircuitSAT`]: Boolean circuit satisfiability
+//! - [`QuantifiedBooleanFormulas`]: Quantified Boolean Formulas (QBF) — PSPACE-complete
 
 pub(crate) mod circuit;
 mod ksat;
+pub(crate) mod qbf;
 mod sat;
 
 pub use circuit::{Assignment, BooleanExpr, BooleanOp, Circuit, CircuitSAT};
 pub use ksat::KSatisfiability;
+pub use qbf::{QuantifiedBooleanFormulas, Quantifier};
 pub use sat::{CNFClause, Satisfiability};