problemreductions/models/formula/
qbf.rs

1//! Quantified Boolean Formulas (QBF) problem implementation.
2//!
3//! QBF is the problem of determining whether a fully quantified Boolean formula
4//! with alternating universal and existential quantifiers is true. It is the
5//! canonical PSPACE-complete problem (Stockmeyer & Meyer, 1973).
6//!
7//! Given F = (Q_1 u_1)(Q_2 u_2)...(Q_n u_n) E, where each Q_i is either
8//! ∀ (ForAll) or ∃ (Exists) and E is a Boolean expression in CNF,
9//! determine whether F is true.
10
11use crate::models::formula::{sat::validate_cnf_literals, CNFClause};
12use crate::registry::{FieldInfo, ProblemSchemaEntry};
13use crate::traits::Problem;
14use serde::{Deserialize, Serialize};
15
16inventory::submit! {
17    ProblemSchemaEntry {
18        name: "QuantifiedBooleanFormulas",
19        display_name: "Quantified Boolean Formulas",
20        aliases: &["QBF"],
21        dimensions: &[],
22        category: crate::registry::ProblemCategory::Formula,
23        module_path: module_path!(),
24        description: "Determine if a quantified Boolean formula is true",
25        fields: &[
26            FieldInfo { name: "num_vars", type_name: "usize", description: "Number of Boolean variables" },
27            FieldInfo { name: "quantifiers", type_name: "Vec<Quantifier>", description: "Quantifier for each variable (Exists or ForAll)" },
28            FieldInfo { name: "clauses", type_name: "Vec<CNFClause>", description: "CNF clauses of the Boolean expression E" },
29        ],
30    }
31}
32
33/// Quantifier type for QBF variables.
34#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
35pub enum Quantifier {
36    /// Existential quantifier (∃)
37    Exists,
38    /// Universal quantifier (∀)
39    ForAll,
40}
41
42/// Quantified Boolean Formulas (QBF) problem.
43///
44/// Given a fully quantified Boolean formula F = (Q_1 u_1)...(Q_n u_n) E,
45/// where each Q_i is ∀ or ∃ and E is in CNF, determine whether F is true.
46///
47/// # Example
48///
49/// ```
50/// use problemreductions::models::formula::{QuantifiedBooleanFormulas, Quantifier, CNFClause};
51/// use problemreductions::Problem;
52///
53/// // F = ∃u_1 ∀u_2 (u_1 ∨ u_2) ∧ (u_1 ∨ ¬u_2)
54/// let problem = QuantifiedBooleanFormulas::new(
55///     2,
56///     vec![Quantifier::Exists, Quantifier::ForAll],
57///     vec![
58///         CNFClause::new(vec![1, 2]),   // u_1 OR u_2
59///         CNFClause::new(vec![1, -2]),  // u_1 OR NOT u_2
60///     ],
61/// );
62///
63/// // With u_1=true, both clauses are satisfied regardless of u_2
64/// assert!(problem.is_true());
65/// ```
66#[derive(Debug, Clone, Serialize, Deserialize)]
67#[serde(try_from = "QuantifiedBooleanFormulasDef")]
68pub struct QuantifiedBooleanFormulas {
69    /// Number of variables.
70    num_vars: usize,
71    /// Quantifier for each variable (indexed 0..num_vars).
72    quantifiers: Vec<Quantifier>,
73    /// Clauses in CNF representing the Boolean expression E.
74    clauses: Vec<CNFClause>,
75}
76
77impl QuantifiedBooleanFormulas {
78    /// Create a new QBF problem.
79    ///
80    /// # Panics
81    ///
82    /// Panics if `quantifiers.len() != num_vars`.
83    pub fn new(num_vars: usize, quantifiers: Vec<Quantifier>, clauses: Vec<CNFClause>) -> Self {
84        Self::try_new(num_vars, quantifiers, clauses).unwrap_or_else(|message| panic!("{message}"))
85    }
86
87    /// Create a QBF problem after validating its quantifiers and CNF literals.
88    pub fn try_new(
89        num_vars: usize,
90        quantifiers: Vec<Quantifier>,
91        clauses: Vec<CNFClause>,
92    ) -> Result<Self, crate::registry::ConstructionError> {
93        if quantifiers.len() != num_vars {
94            return Err(format!(
95                "quantifiers length ({}) must equal num_vars ({num_vars})",
96                quantifiers.len()
97            )
98            .into());
99        }
100        validate_cnf_literals(num_vars, &clauses)?;
101        Ok(Self {
102            num_vars,
103            quantifiers,
104            clauses,
105        })
106    }
107
108    /// Get the number of variables.
109    pub fn num_vars(&self) -> usize {
110        self.num_vars
111    }
112
113    /// Get the number of clauses.
114    pub fn num_clauses(&self) -> usize {
115        self.clauses.len()
116    }
117
118    /// Get the quantifiers.
119    pub fn quantifiers(&self) -> &[Quantifier] {
120        &self.quantifiers
121    }
122
123    /// Get the clauses.
124    pub fn clauses(&self) -> &[CNFClause] {
125        &self.clauses
126    }
127
128    /// Evaluate whether the QBF formula is true using game-tree search.
129    ///
130    /// This implements a recursive minimax-style evaluation:
131    /// - For ∃ quantifiers: true if ANY assignment to the variable leads to true
132    /// - For ∀ quantifiers: true if ALL assignments to the variable lead to true
133    ///
134    /// Runtime is O(2^n) in the worst case.
135    pub fn is_true(&self) -> bool {
136        let mut assignment = vec![false; self.num_vars];
137        self.evaluate_recursive(&mut assignment, 0)
138    }
139
140    /// Recursive QBF evaluation.
141    fn evaluate_recursive(&self, assignment: &mut Vec<bool>, var_idx: usize) -> bool {
142        if var_idx == self.num_vars {
143            // All variables assigned — evaluate the CNF matrix
144            return self.clauses.iter().all(|c| c.is_satisfied(assignment));
145        }
146
147        match self.quantifiers[var_idx] {
148            Quantifier::Exists => {
149                // Try both values; true if either works
150                assignment[var_idx] = false;
151                if self.evaluate_recursive(assignment, var_idx + 1) {
152                    return true;
153                }
154                assignment[var_idx] = true;
155                self.evaluate_recursive(assignment, var_idx + 1)
156            }
157            Quantifier::ForAll => {
158                // Try both values; true only if both work
159                assignment[var_idx] = false;
160                if !self.evaluate_recursive(assignment, var_idx + 1) {
161                    return false;
162                }
163                assignment[var_idx] = true;
164                self.evaluate_recursive(assignment, var_idx + 1)
165            }
166        }
167    }
168}
169
170impl Problem for QuantifiedBooleanFormulas {
171    const NAME: &'static str = "QuantifiedBooleanFormulas";
172    type Solution = ();
173    type Value = crate::types::Or;
174
175    crate::problem_parameters![("num_vars", num_vars), ("num_clauses", num_clauses),];
176
177    fn evaluate(
178        &self,
179        _solution: &Self::Solution,
180    ) -> Result<crate::types::Or, crate::traits::EvaluationError> {
181        Ok(crate::types::Or(self.is_true()))
182    }
183
184    fn variant() -> Vec<(&'static str, &'static str)> {
185        crate::variant_params![]
186    }
187}
188
189impl crate::solvers::BruteForceProblem for QuantifiedBooleanFormulas {
190    fn dimensions(&self) -> Vec<usize> {
191        vec![]
192    }
193}
194
195crate::declare_variants! {
196    default QuantifiedBooleanFormulas => "2^num_vars",
197}
198
199crate::register_brute_force! {
200    QuantifiedBooleanFormulas decode |_, _| (),
201}
202
203#[derive(Deserialize)]
204struct QuantifiedBooleanFormulasDef {
205    num_vars: usize,
206    quantifiers: Vec<Quantifier>,
207    clauses: Vec<CNFClause>,
208}
209
210impl TryFrom<QuantifiedBooleanFormulasDef> for QuantifiedBooleanFormulas {
211    type Error = crate::registry::ConstructionError;
212
213    fn try_from(value: QuantifiedBooleanFormulasDef) -> Result<Self, Self::Error> {
214        Self::try_new(value.num_vars, value.quantifiers, value.clauses)
215    }
216}
217
218#[cfg(feature = "example-db")]
219pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
220    vec![crate::example_db::specs::ModelExampleSpec {
221        id: "quantified_boolean_formulas",
222        instance: Box::new(QuantifiedBooleanFormulas::new(
223            2,
224            vec![Quantifier::Exists, Quantifier::ForAll],
225            vec![
226                CNFClause::new(vec![1, 2]),  // u_1 OR u_2
227                CNFClause::new(vec![1, -2]), // u_1 OR NOT u_2
228            ],
229        )),
230        optimal_config: serde_json::json!(null),
231        optimal_value: serde_json::json!(true),
232    }]
233}
234
235#[cfg(test)]
236#[path = "../../unit_tests/models/formula/qbf.rs"]
237mod tests;
problemreductions/models/formula/qbf.rs

problemreductions/models/formula/
qbf.rs
