Struct QuantifiedBooleanFormulas 

pub struct QuantifiedBooleanFormulas { /* private fields */ }

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());

Implementations

impl QuantifiedBooleanFormulas

pub fn new( num_vars: usize, quantifiers: Vec<Quantifier>, clauses: Vec<CNFClause>, ) -> Self

Create a new QBF problem.

Panics

Panics if quantifiers.len() != num_vars.

pub fn num_vars(&self) -> usize

Get the number of variables.

pub fn num_clauses(&self) -> usize

Get the number of clauses.

pub fn quantifiers(&self) -> &[Quantifier]

Get the quantifiers.

pub fn clauses(&self) -> &[CNFClause]

Get the clauses.

pub fn is_true(&self) -> bool

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.

Trait Implementations

impl Clone for QuantifiedBooleanFormulas

fn clone(&self) -> QuantifiedBooleanFormulas

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for QuantifiedBooleanFormulas

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for QuantifiedBooleanFormulas

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Problem for QuantifiedBooleanFormulas

const NAME: &'static str = "QuantifiedBooleanFormulas"

Base name of this problem type (e.g., “MaximumIndependentSet”).

type Value = Or

The evaluation value type.

fn dims(&self) -> Vec<usize>

Configuration space dimensions. Each entry is the cardinality of that variable.

fn evaluate(&self, config: &[usize]) -> Or

Evaluate the problem on a configuration.

fn variant() -> Vec<(&'static str, &'static str)>

Returns variant attributes derived from type parameters.

fn num_variables(&self) -> usize

Number of variables (derived from dims).

fn problem_type() -> ProblemType

Look up this problem’s catalog entry.

impl Serialize for QuantifiedBooleanFormulas

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl DeclaredVariant for QuantifiedBooleanFormulas