pumpkin_core/api/outputs/
solution_iterator.rs

1//! Contains the structures corresponding to solution iterations.
2
3use std::fmt::Debug;
4
5use super::SatisfactionResult::Satisfiable;
6use super::SatisfactionResult::Unknown;
7use super::SatisfactionResult::Unsatisfiable;
8use super::SolutionReference;
9use crate::branching::Brancher;
10use crate::predicate;
11use crate::predicates::Predicate;
12use crate::results::ProblemSolution;
13use crate::results::Solution;
14use crate::termination::TerminationCondition;
15use crate::Solver;
16
17/// A struct which allows the retrieval of multiple solutions to a satisfaction problem.
18#[derive(Debug)]
19pub struct SolutionIterator<'solver, 'brancher, 'termination, B, T> {
20    solver: &'solver mut Solver,
21    brancher: &'brancher mut B,
22    termination: &'termination mut T,
23    next_blocking_clause: Option<Vec<Predicate>>,
24    has_solution: bool,
25}
26
27impl<'solver, 'brancher, 'termination, B: Brancher, T: TerminationCondition>
28    SolutionIterator<'solver, 'brancher, 'termination, B, T>
29{
30    pub(crate) fn new(
31        solver: &'solver mut Solver,
32        brancher: &'brancher mut B,
33        termination: &'termination mut T,
34    ) -> Self {
35        SolutionIterator {
36            solver,
37            brancher,
38            termination,
39            next_blocking_clause: None,
40            has_solution: false,
41        }
42    }
43
44    /// Find a new solution by blocking the previous solution from being found. Also calls the
45    /// [`Brancher::on_solution`] method from the [`Brancher`] used to run the initial solve.
46    pub fn next_solution(&mut self) -> IteratedSolution<'_, B> {
47        if let Some(blocking_clause) = self.next_blocking_clause.take() {
48            // We do not care much about this tag, as the proof is nonsensical for
49            // solution enumeration anyways.
50            let constraint_tag = self.solver.new_constraint_tag();
51            if self
52                .solver
53                .add_clause(blocking_clause, constraint_tag)
54                .is_err()
55            {
56                return IteratedSolution::Finished;
57            }
58        }
59
60        let result = match self.solver.satisfy(self.brancher, self.termination) {
61            Satisfiable(satisfiable) => {
62                let solution: Solution = satisfiable.solution().into();
63                self.has_solution = true;
64                self.next_blocking_clause = Some(get_blocking_clause(solution.as_reference()));
65                IterationResult::Solution(solution)
66            }
67            Unsatisfiable(_, _) => {
68                if self.has_solution {
69                    IterationResult::Finished
70                } else {
71                    IterationResult::Unsatisfiable
72                }
73            }
74            Unknown(_, _) => IterationResult::Unknown,
75        };
76
77        match result {
78            IterationResult::Solution(solution) => {
79                IteratedSolution::Solution(solution, self.solver, self.brancher)
80            }
81            IterationResult::Finished => IteratedSolution::Finished,
82            IterationResult::Unsatisfiable => IteratedSolution::Unsatisfiable,
83            IterationResult::Unknown => IteratedSolution::Unknown,
84        }
85    }
86}
87
88/// The different results we can get from the next solution call. We need this type because
89/// [`IteratedSolution`] takes a reference to [`Solver`], which, at the time where
90/// [`IterationResult::Solution`] is created, cannot be given as there is an exclusive borrow of the
91/// solver alive as well.
92enum IterationResult {
93    Solution(Solution),
94    Finished,
95    Unsatisfiable,
96    Unknown,
97}
98
99/// Creates a clause which prevents the current solution from occurring again by going over the
100/// defined output variables and creating a clause which prevents those values from
101/// being assigned.
102///
103/// This method is used when attempting to find multiple solutions.
104fn get_blocking_clause(solution: SolutionReference) -> Vec<Predicate> {
105    solution
106        .get_domains()
107        .map(|variable| predicate!(variable != solution.get_integer_value(variable)))
108        .collect::<Vec<_>>()
109}
110/// Enum which specifies the status of the call to [`SolutionIterator::next_solution`].
111#[allow(
112    clippy::large_enum_variant,
113    reason = "these will not be stored in bulk, so this is not an issue"
114)]
115#[derive(Debug)]
116pub enum IteratedSolution<'a, B> {
117    /// A new solution was identified.
118    Solution(Solution, &'a Solver, &'a B),
119
120    /// No more solutions exist.
121    Finished,
122
123    /// The solver was terminated during search.
124    Unknown,
125
126    /// There exists no solution
127    Unsatisfiable,
128}
pumpkin_core/api/outputs/solution_iterator.rs

pumpkin_core/api/outputs/
solution_iterator.rs
