From a81c79f2a12cc4baa190aa898af221b9745fee3a Mon Sep 17 00:00:00 2001 From: zazabap Date: Fri, 13 Mar 2026 07:40:31 +0000 Subject: [PATCH 1/2] Add plan for #571: QuantifiedBooleanFormulas model Co-Authored-By: Claude Opus 4.6 --- ...03-13-quantified-boolean-formulas-model.md | 99 +++++++++++++++++++ 1 file changed, 99 insertions(+) create mode 100644 docs/plans/2026-03-13-quantified-boolean-formulas-model.md diff --git a/docs/plans/2026-03-13-quantified-boolean-formulas-model.md b/docs/plans/2026-03-13-quantified-boolean-formulas-model.md new file mode 100644 index 00000000..767650d0 --- /dev/null +++ b/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`, `clauses: Vec` | +| 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::(data)` in `load_problem()` + - Add `"QuantifiedBooleanFormulas" => try_ser::(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` + - 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 +``` From 6782dddae350b5ae35697c510924e4e885ed06a7 Mon Sep 17 00:00:00 2001 From: zazabap Date: Fri, 13 Mar 2026 07:53:00 +0000 Subject: [PATCH 2/2] Add QuantifiedBooleanFormulas (QBF) model Implement the canonical PSPACE-complete problem: given a fully quantified Boolean formula with alternating universal/existential quantifiers, determine whether it is true. Includes model, CLI support, paper entry, and comprehensive tests. Closes #571 Co-Authored-By: Claude Opus 4.6 --- ...aximumindependentset_to_maximumclique.json | 4 +- docs/paper/reductions.typ | 9 + docs/paper/references.bib | 26 ++ problemreductions-cli/src/cli.rs | 4 + problemreductions-cli/src/commands/create.rs | 55 ++++ problemreductions-cli/src/dispatch.rs | 2 + problemreductions-cli/src/problem_name.rs | 2 + src/lib.rs | 4 +- src/models/formula/mod.rs | 3 + src/models/formula/qbf.rs | 186 ++++++++++++++ src/models/mod.rs | 4 +- src/unit_tests/models/formula/qbf.rs | 241 ++++++++++++++++++ 12 files changed, 536 insertions(+), 4 deletions(-) create mode 100644 src/models/formula/qbf.rs create mode 100644 src/unit_tests/models/formula/qbf.rs diff --git a/docs/paper/examples/maximumindependentset_to_maximumclique.json b/docs/paper/examples/maximumindependentset_to_maximumclique.json index 21a8853e..352ddeb6 100644 --- a/docs/paper/examples/maximumindependentset_to_maximumclique.json +++ b/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": [ diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 565abdb1..98b0db5b 100644 --- a/docs/paper/reductions.typ +++ b/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:" — 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 ) ] +#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(, 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(, 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. ][ diff --git a/docs/paper/references.bib b/docs/paper/references.bib index 0ec874f6..6b1b2e5d 100644 --- a/docs/paper/references.bib +++ b/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} +} diff --git a/problemreductions-cli/src/cli.rs b/problemreductions-cli/src/cli.rs index 91792e20..39b4daf7 100644 --- a/problemreductions-cli/src/cli.rs +++ b/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, + /// Quantifiers for QBF (comma-separated, E=Exists, A=ForAll, e.g., "E,A,E") + #[arg(long)] + pub quantifiers: Option, } #[derive(clap::Args)] diff --git a/problemreductions-cli/src/commands/create.rs b/problemreductions-cli/src/commands/create.rs index 2df4f099..13af384e 100644 --- a/problemreductions-cli/src/commands/create.rs +++ b/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>> { .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> { + let q_str = args + .quantifiers + .as_deref() + .ok_or_else(|| anyhow::anyhow!("QBF requires --quantifiers (e.g., \"E,A,E\")"))?; + + let quantifiers: Vec = 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::>>()?; + + if quantifiers.len() != num_vars { + bail!( + "Expected {} quantifiers but got {}", + num_vars, + quantifiers.len() + ); + } + Ok(quantifiers) +} + /// Handle `pred create --random ...` fn create_random( args: &CreateArgs, diff --git a/problemreductions-cli/src/dispatch.rs b/problemreductions-cli/src/dispatch.rs index 49dd523c..b9bc96bc 100644 --- a/problemreductions-cli/src/dispatch.rs +++ b/problemreductions-cli/src/dispatch.rs @@ -226,6 +226,7 @@ pub fn load_problem( _ => deser_opt::>(data), }, "Satisfiability" => deser_sat::(data), + "QuantifiedBooleanFormulas" => deser_sat::(data), "KSatisfiability" => match variant.get("k").map(|s| s.as_str()) { Some("K2") => deser_sat::>(data), Some("K3") => deser_sat::>(data), @@ -289,6 +290,7 @@ pub fn serialize_any_problem( _ => try_ser::>(any), }, "Satisfiability" => try_ser::(any), + "QuantifiedBooleanFormulas" => try_ser::(any), "KSatisfiability" => match variant.get("k").map(|s| s.as_str()) { Some("K2") => try_ser::>(any), Some("K3") => try_ser::>(any), diff --git a/problemreductions-cli/src/problem_name.rs b/problemreductions-cli/src/problem_name.rs index 2b6c8c73..7cce811e 100644 --- a/problemreductions-cli/src/problem_name.rs +++ b/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 } } diff --git a/src/lib.rs b/src/lib.rs index a74c906f..29bb9029 100644 --- a/src/lib.rs +++ b/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, diff --git a/src/models/formula/mod.rs b/src/models/formula/mod.rs index f2a33cce..a4076193 100644 --- a/src/models/formula/mod.rs +++ b/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}; diff --git a/src/models/formula/qbf.rs b/src/models/formula/qbf.rs new file mode 100644 index 00000000..3970c7be --- /dev/null +++ b/src/models/formula/qbf.rs @@ -0,0 +1,186 @@ +//! Quantified Boolean Formulas (QBF) problem implementation. +//! +//! QBF is the problem of determining whether a fully quantified Boolean formula +//! with alternating universal and existential quantifiers is true. It is the +//! canonical PSPACE-complete problem (Stockmeyer & Meyer, 1973). +//! +//! Given F = (Q_1 u_1)(Q_2 u_2)...(Q_n u_n) E, where each Q_i is either +//! ∀ (ForAll) or ∃ (Exists) and E is a Boolean expression in CNF, +//! determine whether F is true. + +use crate::models::formula::CNFClause; +use crate::registry::{FieldInfo, ProblemSchemaEntry}; +use crate::traits::{Problem, SatisfactionProblem}; +use serde::{Deserialize, Serialize}; + +inventory::submit! { + ProblemSchemaEntry { + name: "QuantifiedBooleanFormulas", + module_path: module_path!(), + description: "Determine if a quantified Boolean formula is true", + fields: &[ + FieldInfo { name: "num_vars", type_name: "usize", description: "Number of Boolean variables" }, + FieldInfo { name: "quantifiers", type_name: "Vec", description: "Quantifier for each variable (Exists or ForAll)" }, + FieldInfo { name: "clauses", type_name: "Vec", description: "CNF clauses of the Boolean expression E" }, + ], + } +} + +/// Quantifier type for QBF variables. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)] +pub enum Quantifier { + /// Existential quantifier (∃) + Exists, + /// Universal quantifier (∀) + ForAll, +} + +/// Quantified Boolean Formulas (QBF) problem. +/// +/// 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 in CNF, determine whether F is true. +/// +/// # Example +/// +/// ``` +/// use problemreductions::models::formula::{QuantifiedBooleanFormulas, Quantifier, CNFClause}; +/// use problemreductions::Problem; +/// +/// // F = ∃u_1 ∀u_2 (u_1 ∨ u_2) ∧ (u_1 ∨ ¬u_2) +/// let problem = QuantifiedBooleanFormulas::new( +/// 2, +/// vec![Quantifier::Exists, Quantifier::ForAll], +/// vec![ +/// CNFClause::new(vec![1, 2]), // u_1 OR u_2 +/// CNFClause::new(vec![1, -2]), // u_1 OR NOT u_2 +/// ], +/// ); +/// +/// // With u_1=true, both clauses are satisfied regardless of u_2 +/// assert!(problem.is_true()); +/// ``` +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct QuantifiedBooleanFormulas { + /// Number of variables. + num_vars: usize, + /// Quantifier for each variable (indexed 0..num_vars). + quantifiers: Vec, + /// Clauses in CNF representing the Boolean expression E. + clauses: Vec, +} + +impl QuantifiedBooleanFormulas { + /// Create a new QBF problem. + /// + /// # Panics + /// + /// Panics if `quantifiers.len() != num_vars`. + pub fn new(num_vars: usize, quantifiers: Vec, clauses: Vec) -> Self { + assert_eq!( + quantifiers.len(), + num_vars, + "quantifiers length ({}) must equal num_vars ({})", + quantifiers.len(), + num_vars + ); + Self { + num_vars, + quantifiers, + clauses, + } + } + + /// Get the number of variables. + pub fn num_vars(&self) -> usize { + self.num_vars + } + + /// Get the number of clauses. + pub fn num_clauses(&self) -> usize { + self.clauses.len() + } + + /// Get the quantifiers. + pub fn quantifiers(&self) -> &[Quantifier] { + &self.quantifiers + } + + /// Get the clauses. + pub fn clauses(&self) -> &[CNFClause] { + &self.clauses + } + + /// Evaluate whether the QBF formula is true using game-tree search. + /// + /// This implements a recursive minimax-style evaluation: + /// - For ∃ quantifiers: true if ANY assignment to the variable leads to true + /// - For ∀ quantifiers: true if ALL assignments to the variable lead to true + /// + /// Runtime is O(2^n) in the worst case. + pub fn is_true(&self) -> bool { + let mut assignment = vec![false; self.num_vars]; + self.evaluate_recursive(&mut assignment, 0) + } + + /// Recursive QBF evaluation. + fn evaluate_recursive(&self, assignment: &mut Vec, var_idx: usize) -> bool { + if var_idx == self.num_vars { + // All variables assigned — evaluate the CNF matrix + return self.clauses.iter().all(|c| c.is_satisfied(assignment)); + } + + match self.quantifiers[var_idx] { + Quantifier::Exists => { + // Try both values; true if either works + assignment[var_idx] = false; + if self.evaluate_recursive(assignment, var_idx + 1) { + return true; + } + assignment[var_idx] = true; + self.evaluate_recursive(assignment, var_idx + 1) + } + Quantifier::ForAll => { + // Try both values; true only if both work + assignment[var_idx] = false; + if !self.evaluate_recursive(assignment, var_idx + 1) { + return false; + } + assignment[var_idx] = true; + self.evaluate_recursive(assignment, var_idx + 1) + } + } + } + + /// Convert a usize config to boolean assignment. + fn config_to_assignment(config: &[usize]) -> Vec { + config.iter().map(|&v| v == 1).collect() + } +} + +impl Problem for QuantifiedBooleanFormulas { + const NAME: &'static str = "QuantifiedBooleanFormulas"; + type Metric = bool; + + fn dims(&self) -> Vec { + vec![2; self.num_vars] + } + + fn evaluate(&self, config: &[usize]) -> bool { + let assignment = Self::config_to_assignment(config); + self.clauses.iter().all(|c| c.is_satisfied(&assignment)) + } + + fn variant() -> Vec<(&'static str, &'static str)> { + crate::variant_params![] + } +} + +impl SatisfactionProblem for QuantifiedBooleanFormulas {} + +crate::declare_variants! { + QuantifiedBooleanFormulas => "2^num_vars", +} + +#[cfg(test)] +#[path = "../../unit_tests/models/formula/qbf.rs"] +mod tests; diff --git a/src/models/mod.rs b/src/models/mod.rs index ceb584ce..f8fd7efb 100644 --- a/src/models/mod.rs +++ b/src/models/mod.rs @@ -10,7 +10,9 @@ pub mod set; // Re-export commonly used types pub use algebraic::{ClosestVectorProblem, BMF, ILP, QUBO}; -pub use formula::{CNFClause, CircuitSAT, KSatisfiability, Satisfiability}; +pub use formula::{ + CNFClause, CircuitSAT, KSatisfiability, QuantifiedBooleanFormulas, Quantifier, Satisfiability, +}; pub use graph::{ BicliqueCover, GraphPartitioning, KColoring, MaxCut, MaximalIS, MaximumClique, MaximumIndependentSet, MaximumMatching, MinimumDominatingSet, MinimumFeedbackVertexSet, diff --git a/src/unit_tests/models/formula/qbf.rs b/src/unit_tests/models/formula/qbf.rs new file mode 100644 index 00000000..4e433841 --- /dev/null +++ b/src/unit_tests/models/formula/qbf.rs @@ -0,0 +1,241 @@ +use super::*; +use crate::solvers::{BruteForce, Solver}; +use crate::traits::Problem; + +#[test] +fn test_quantifier_creation() { + let q1 = Quantifier::Exists; + let q2 = Quantifier::ForAll; + assert_eq!(q1, Quantifier::Exists); + assert_eq!(q2, Quantifier::ForAll); + assert_ne!(q1, q2); +} + +#[test] +fn test_qbf_creation() { + let problem = QuantifiedBooleanFormulas::new( + 3, + vec![Quantifier::Exists, Quantifier::ForAll, Quantifier::Exists], + vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![-1, 3])], + ); + assert_eq!(problem.num_vars(), 3); + assert_eq!(problem.num_clauses(), 2); + assert_eq!(problem.num_variables(), 3); + assert_eq!(problem.quantifiers().len(), 3); + assert_eq!(problem.clauses().len(), 2); +} + +#[test] +#[should_panic(expected = "quantifiers length")] +fn test_qbf_creation_mismatch() { + QuantifiedBooleanFormulas::new( + 3, + vec![Quantifier::Exists, Quantifier::ForAll], // Only 2, need 3 + vec![], + ); +} + +#[test] +fn test_qbf_evaluate() { + // F = ∃u_1 ∀u_2 (u_1 ∨ u_2) ∧ (u_1 ∨ ¬u_2) + let problem = QuantifiedBooleanFormulas::new( + 2, + vec![Quantifier::Exists, Quantifier::ForAll], + vec![ + CNFClause::new(vec![1, 2]), // u_1 OR u_2 + CNFClause::new(vec![1, -2]), // u_1 OR NOT u_2 + ], + ); + + // evaluate() just checks if the CNF is satisfied under the given assignment + assert!(problem.evaluate(&[1, 0])); // u_1=T, u_2=F: (T∨F)∧(T∨T) = T + assert!(problem.evaluate(&[1, 1])); // u_1=T, u_2=T: (T∨T)∧(T∨F) = T + assert!(!problem.evaluate(&[0, 0])); // u_1=F, u_2=F: (F∨F)∧(F∨T) = F + // u_1=F, u_2=T: clause1=(F∨T)=T, clause2=(F∨F)=F → false + assert!(!problem.evaluate(&[0, 1])); +} + +#[test] +fn test_qbf_is_true_simple_true() { + // F = ∃u_1 ∀u_2 (u_1 ∨ u_2) ∧ (u_1 ∨ ¬u_2) + // Setting u_1=T satisfies both clauses regardless of u_2 + let problem = QuantifiedBooleanFormulas::new( + 2, + vec![Quantifier::Exists, Quantifier::ForAll], + vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![1, -2])], + ); + assert!(problem.is_true()); +} + +#[test] +fn test_qbf_is_true_simple_false() { + // F = ∀u_1 ∃u_2 (u_1) ∧ (¬u_1) + // This is always false: no assignment can satisfy both u_1 and NOT u_1 + let problem = QuantifiedBooleanFormulas::new( + 2, + vec![Quantifier::ForAll, Quantifier::Exists], + vec![CNFClause::new(vec![1]), CNFClause::new(vec![-1])], + ); + assert!(!problem.is_true()); +} + +#[test] +fn test_qbf_is_true_all_exists() { + // When all quantifiers are Exists, QBF reduces to SAT + // F = ∃u_1 ∃u_2 (u_1 ∨ u_2) ∧ (¬u_1 ∨ ¬u_2) + let problem = QuantifiedBooleanFormulas::new( + 2, + vec![Quantifier::Exists, Quantifier::Exists], + vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![-1, -2])], + ); + // Satisfiable: u_1=T,u_2=F or u_1=F,u_2=T + assert!(problem.is_true()); +} + +#[test] +fn test_qbf_is_true_all_forall() { + // F = ∀u_1 ∀u_2 (u_1 ∨ u_2) + // False: u_1=F, u_2=F fails the clause + let problem = QuantifiedBooleanFormulas::new( + 2, + vec![Quantifier::ForAll, Quantifier::ForAll], + vec![CNFClause::new(vec![1, 2])], + ); + assert!(!problem.is_true()); +} + +#[test] +fn test_qbf_is_true_all_forall_tautology() { + // F = ∀u_1 (u_1 ∨ ¬u_1) + // Always true (tautology) + let problem = QuantifiedBooleanFormulas::new( + 1, + vec![Quantifier::ForAll], + vec![CNFClause::new(vec![1, -1])], + ); + assert!(problem.is_true()); +} + +#[test] +fn test_qbf_empty_formula() { + // Empty CNF is trivially true + let problem = + QuantifiedBooleanFormulas::new(2, vec![Quantifier::Exists, Quantifier::ForAll], vec![]); + assert!(problem.evaluate(&[0, 0])); + assert!(problem.is_true()); +} + +#[test] +fn test_qbf_zero_vars() { + // Zero variables, empty clauses + let problem = QuantifiedBooleanFormulas::new(0, vec![], vec![]); + assert!(problem.evaluate(&[])); + assert!(problem.is_true()); + assert_eq!(problem.dims(), Vec::::new()); +} + +#[test] +fn test_qbf_zero_vars_unsat() { + // Zero variables, but a clause that refers to var 1 (unsatisfiable) + let problem = QuantifiedBooleanFormulas::new(0, vec![], vec![CNFClause::new(vec![1])]); + assert!(!problem.evaluate(&[])); + assert!(!problem.is_true()); +} + +#[test] +fn test_qbf_solver() { + // F = ∃u_1 ∀u_2 (u_1 ∨ u_2) ∧ (u_1 ∨ ¬u_2) + let problem = QuantifiedBooleanFormulas::new( + 2, + vec![Quantifier::Exists, Quantifier::ForAll], + vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![1, -2])], + ); + + let solver = BruteForce::new(); + // find_satisfying finds any config where evaluate() returns true + let solution = solver.find_satisfying(&problem); + assert!(solution.is_some()); + let sol = solution.unwrap(); + assert!(problem.evaluate(&sol)); +} + +#[test] +fn test_qbf_solver_all_satisfying() { + // F = ∃u_1 ∀u_2 (u_1 ∨ u_2) ∧ (u_1 ∨ ¬u_2) + let problem = QuantifiedBooleanFormulas::new( + 2, + vec![Quantifier::Exists, Quantifier::ForAll], + vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![1, -2])], + ); + + let solver = BruteForce::new(); + let solutions = solver.find_all_satisfying(&problem); + // u_1=T makes both clauses satisfied regardless of u_2 + // So configs [1,0] and [1,1] should satisfy + assert_eq!(solutions.len(), 2); + for sol in &solutions { + assert!(problem.evaluate(sol)); + } +} + +#[test] +fn test_qbf_serialization() { + let problem = QuantifiedBooleanFormulas::new( + 2, + vec![Quantifier::Exists, Quantifier::ForAll], + vec![CNFClause::new(vec![1, -2])], + ); + + let json = serde_json::to_string(&problem).unwrap(); + let deserialized: QuantifiedBooleanFormulas = serde_json::from_str(&json).unwrap(); + + assert_eq!(deserialized.num_vars(), problem.num_vars()); + assert_eq!(deserialized.num_clauses(), problem.num_clauses()); + assert_eq!(deserialized.quantifiers(), problem.quantifiers()); + assert_eq!(deserialized.dims(), problem.dims()); +} + +#[test] +fn test_qbf_three_vars() { + // F = ∃u_1 ∀u_2 ∃u_3 (u_1 ∨ u_2 ∨ u_3) ∧ (¬u_1 ∨ ¬u_2 ∨ u_3) + // Strategy: set u_1=T. Then for any u_2: + // Clause 1 is satisfied (u_1=T). + // Set u_3=T: Clause 2 = (F ∨ ¬u_2 ∨ T) = T. + // So this is true. + let problem = QuantifiedBooleanFormulas::new( + 3, + vec![Quantifier::Exists, Quantifier::ForAll, Quantifier::Exists], + vec![ + CNFClause::new(vec![1, 2, 3]), + CNFClause::new(vec![-1, -2, 3]), + ], + ); + assert!(problem.is_true()); +} + +#[test] +fn test_qbf_dims() { + let problem = QuantifiedBooleanFormulas::new( + 4, + vec![ + Quantifier::Exists, + Quantifier::ForAll, + Quantifier::Exists, + Quantifier::ForAll, + ], + vec![CNFClause::new(vec![1, 2, 3, 4])], + ); + assert_eq!(problem.dims(), vec![2, 2, 2, 2]); +} + +#[test] +fn test_qbf_variant() { + assert_eq!(QuantifiedBooleanFormulas::variant(), vec![]); +} + +#[test] +fn test_qbf_quantifier_debug() { + let q = Quantifier::Exists; + let debug = format!("{:?}", q); + assert!(debug.contains("Exists")); +}