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

pumpkin_core/api/outputs/
solution_iterator.rs
