feat: Adding lower-bounding search to the solver (#132)

Currently, we only support upper-bounding search (LSU) in the solver; however, it makes sense to also support lower-bounding search (LUS) in the solver. This PR aims to implement lower-bounding search using assumptions. --------- Co-authored-by: Maarten Flippo <[email protected]>
ConSol-Lab · Feb 10, 2025 · 947896d · 947896d
1 parent 07bc835
commit 947896d
Show file tree

Hide file tree

Showing 13 changed files with 596 additions and 379 deletions.
diff --git a/pumpkin-solver/src/api/mod.rs b/pumpkin-solver/src/api/mod.rs
@@ -1,4 +1,5 @@
 mod outputs;
+
 pub(crate) mod solver;
 
 pub mod results {
@@ -14,7 +15,6 @@ pub mod results {
     //! right state for these operations. For example,
     //! [`SatisfactionResultUnderAssumptions::UnsatisfiableUnderAssumptions`] allows you to extract
     //! a core consisting of the assumptions using [`UnsatisfiableUnderAssumptions::extract_core`].
-    pub use crate::api::outputs::solution_callback_arguments::SolutionCallbackArguments;
     pub use crate::api::outputs::solution_iterator;
     pub use crate::api::outputs::unsatisfiable;
     pub use crate::api::outputs::OptimisationResult;
@@ -94,7 +94,7 @@ pub mod termination {
 }
 
 pub mod predicates {
-    //! Containts structures which represent certain [predicates](https://en.wikipedia.org/wiki/Predicate_(mathematical_logic)).
+    //! Contains structures which represent certain [predicates](https://en.wikipedia.org/wiki/Predicate_(mathematical_logic)).
     //!
     //! The solver only utilizes the following types of predicates:
     //! - A [`Predicate::LowerBound`] of the form `[x >= v]`

diff --git a/pumpkin-solver/src/api/outputs/mod.rs b/pumpkin-solver/src/api/outputs/mod.rs
@@ -2,7 +2,6 @@ use self::unsatisfiable::UnsatisfiableUnderAssumptions;
 pub use crate::basic_types::ProblemSolution;
 use crate::basic_types::Solution;
 pub use crate::basic_types::SolutionReference;
-pub(crate) mod solution_callback_arguments;
 pub mod solution_iterator;
 pub mod unsatisfiable;
 use crate::branching::Brancher;
@@ -47,7 +46,7 @@ pub enum SatisfactionResultUnderAssumptions<'solver, 'brancher, B: Brancher> {
     Unknown,
 }
 
-/// The result of a call to [`Solver::maximise`] or [`Solver::minimise`].
+/// The result of a call to [`Solver::optimise`].
 #[derive(Debug)]
 pub enum OptimisationResult {
     /// Indicates that an optimal solution has been found and proven to be optimal. It provides an

diff --git a/pumpkin-solver/src/api/outputs/solution_callback_arguments.rs b/pumpkin-solver/src/api/outputs/solution_callback_arguments.rs
diff --git a/pumpkin-solver/src/api/outputs/solution_iterator.rs b/pumpkin-solver/src/api/outputs/solution_iterator.rs
@@ -53,7 +53,7 @@ impl<'solver, 'brancher, 'termination, B: Brancher, T: TerminationCondition>
             Satisfiable(solution) => {
                 self.has_solution = true;
                 self.next_blocking_clause = Some(get_blocking_clause(&solution));
-                IteratedSolution::Solution(solution)
+                IteratedSolution::Solution(solution, self.solver)
             }
             Unsatisfiable => {
                 if self.has_solution {
@@ -84,9 +84,9 @@ fn get_blocking_clause(solution: &Solution) -> Vec<Predicate> {
     reason = "these will not be stored in bulk, so this is not an issue"
 )]
 #[derive(Debug)]
-pub enum IteratedSolution {
+pub enum IteratedSolution<'a> {
     /// A new solution was identified.
-    Solution(Solution),
+    Solution(Solution, &'a Solver),
 
     /// No more solutions exist.
     Finished,