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            if self
64                .solver
65                .add_clause(blocking_clause, constraint_tag)
66                .is_err()
67            {
68                return IteratedSolution::Finished;
69            }
70        }
71
72        let result = match self
73            .solver
74            .satisfy(self.brancher, self.termination, self.resolver)
75        {
76            Satisfiable(satisfiable) => {
77                let solution: Solution = satisfiable.solution().into();
78                self.has_solution = true;
79                self.next_blocking_clause = Some(get_blocking_clause(solution.as_reference()));
80                IterationResult::Solution(solution)
81            }
82            Unsatisfiable(_, _, _) => {
83                if self.has_solution {
84                    IterationResult::Finished
85                } else {
86                    IterationResult::Unsatisfiable
87                }
88            }
89            Unknown(_, _, _) => IterationResult::Unknown,
90        };
91
92        match result {
93            IterationResult::Solution(solution) => {
94                IteratedSolution::Solution(solution, self.solver, self.brancher, self.resolver)
95            }
96            IterationResult::Finished => IteratedSolution::Finished,
97            IterationResult::Unsatisfiable => IteratedSolution::Unsatisfiable,
98            IterationResult::Unknown => IteratedSolution::Unknown,
99        }
100    }
101}
102
103/// The different results we can get from the next solution call. We need this type because
104/// [`IteratedSolution`] takes a reference to [`Solver`], which, at the time where
105/// [`IterationResult::Solution`] is created, cannot be given as there is an exclusive borrow of the
106/// solver alive as well.
107enum IterationResult {
108    Solution(Solution),
109    Finished,
110    Unsatisfiable,
111    Unknown,
112}
113
114/// Creates a clause which prevents the current solution from occurring again by going over the
115/// defined output variables and creating a clause which prevents those values from
116/// being assigned.
117///
118/// This method is used when attempting to find multiple solutions.
119fn get_blocking_clause(solution: SolutionReference) -> Vec<Predicate> {
120    solution
121        .get_domains()
122        .map(|variable| predicate!(variable != solution.get_integer_value(variable)))
123        .collect::<Vec<_>>()
124}
125/// Enum which specifies the status of the call to [`SolutionIterator::next_solution`].
126#[allow(
127    clippy::large_enum_variant,
128    reason = "these will not be stored in bulk, so this is not an issue"
129)]
130#[derive(Debug)]
131pub enum IteratedSolution<'a, B, R> {
132    /// A new solution was identified.
133    Solution(Solution, &'a Solver, &'a B, &'a R),
134
135    /// No more solutions exist.
136    Finished,
137
138    /// The solver was terminated during search.
139    Unknown,
140
141    /// There exists no solution
142    Unsatisfiable,
143}
pumpkin_core/api/outputs/solution_iterator.rs

pumpkin_core/api/outputs/
solution_iterator.rs
