elenchus_solver/sat/
models.rs

1//! Lazy, incremental model enumeration: each `next()` adds a blocking clause and
2//! continues from the existing solver state rather than re-solving from scratch.
3use alloc::vec::Vec;
4
5use super::solver::Solver;
6use super::{Cnf, Var};
7
8/// A lazy iterator over the models of a CNF, distinct on the `project` variables.
9/// Solving is **incremental**: each step adds a blocking clause and continues
10/// from the existing solver state instead of restarting from scratch.
11pub struct Models {
12    solver: Solver,
13    project: Vec<Var>,
14    done: bool,
15}
16
17impl Iterator for Models {
18    type Item = Vec<bool>;
19
20    fn next(&mut self) -> Option<Vec<bool>> {
21        if self.done {
22            return None;
23        }
24        if !self.solver.search() {
25            self.done = true;
26            return None;
27        }
28        let model = self.solver.model();
29        if !self.solver.block(&self.project, &model) {
30            self.done = true;
31        }
32        Some(model)
33    }
34}
35
36/// Lazily enumerate all models of `cnf`, distinct over `project`.
37pub fn all_models(cnf: &Cnf, project: Vec<Var>) -> Models {
38    Models {
39        solver: Solver::new(cnf),
40        project,
41        done: false,
42    }
43}
44
45/// Up to `limit` models, distinct over `project` (eagerly collected).
46pub fn models(cnf: &Cnf, project: &[Var], limit: usize) -> Vec<Vec<bool>> {
47    all_models(cnf, project.to_vec()).take(limit).collect()
48}
49
50/// Count distinct models projected onto `project`, up to `limit`.
51pub fn models_upto(cnf: &Cnf, project: &[Var], limit: usize) -> usize {
52    all_models(cnf, project.to_vec()).take(limit).count()
53}
elenchus_solver/sat/models.rs

elenchus_solver/sat/
models.rs
