pumpkin_core/optimisation/
linear_sat_unsat.rs

1use super::solution_callback::SolutionCallback;
2use super::OptimisationProcedure;
3use crate::branching::Brancher;
4use crate::optimisation::OptimisationDirection;
5use crate::predicate;
6use crate::results::OptimisationResult;
7use crate::results::ProblemSolution;
8use crate::results::SatisfactionResult;
9use crate::results::SatisfactionResultUnderAssumptions;
10use crate::results::Solution;
11use crate::termination::TerminationCondition;
12use crate::variables::IntegerVariable;
13use crate::Solver;
14
15/// Implements the linear SAT-UNSAT (LSU) optimisation procedure.
16#[derive(Debug, Clone, Copy)]
17pub struct LinearSatUnsat<Var, Callback> {
18    direction: OptimisationDirection,
19    objective: Var,
20    solution_callback: Callback,
21}
22
23impl<Var, Callback> LinearSatUnsat<Var, Callback> {
24    /// Create a new instance of [`LinearSatUnsat`].
25    pub fn new(
26        direction: OptimisationDirection,
27        objective: Var,
28        solution_callback: Callback,
29    ) -> Self {
30        Self {
31            direction,
32            objective,
33            solution_callback,
34        }
35    }
36}
37
38impl<Var, Callback, B> OptimisationProcedure<B, Callback> for LinearSatUnsat<Var, Callback>
39where
40    Var: IntegerVariable,
41    B: Brancher,
42    Callback: SolutionCallback<B>,
43{
44    fn optimise(
45        &mut self,
46        brancher: &mut B,
47        termination: &mut impl TerminationCondition,
48        solver: &mut Solver,
49    ) -> OptimisationResult {
50        let objective = match self.direction {
51            OptimisationDirection::Maximise => self.objective.scaled(-1),
52            OptimisationDirection::Minimise => self.objective.scaled(1),
53        };
54
55        // First we will solve the satisfaction problem without constraining the objective.
56        let mut best_solution: Solution = match solver.satisfy(brancher, termination) {
57            SatisfactionResult::Satisfiable(satisfiable) => satisfiable.solution().into(),
58            SatisfactionResult::Unsatisfiable(_, _) => return OptimisationResult::Unsatisfiable,
59            SatisfactionResult::Unknown(_, _) => return OptimisationResult::Unknown,
60        };
61
62        loop {
63            self.solution_callback.on_solution_callback(
64                solver,
65                best_solution.as_reference(),
66                brancher,
67            );
68
69            let best_objective_value = best_solution.get_integer_value(objective.clone());
70
71            let conclusion = {
72                let solve_result = solver.satisfy_under_assumptions(
73                    brancher,
74                    termination,
75                    &[predicate![objective <= best_objective_value - 1]],
76                );
77
78                match solve_result {
79                    SatisfactionResultUnderAssumptions::Satisfiable(satisfiable) => {
80                        best_solution = satisfiable.solution().into();
81                        None
82                    }
83                    SatisfactionResultUnderAssumptions::UnsatisfiableUnderAssumptions(
84                        _,
85                    ) => {
86                        Some(OptimisationResult::Optimal(best_solution.clone()))
87                    }
88                    SatisfactionResultUnderAssumptions::Unsatisfiable(_) => unreachable!("If the problem is unsatisfiable here, it would have been unsatisifable in the initial solve."),
89                    SatisfactionResultUnderAssumptions::Unknown(_) => Some(OptimisationResult::Satisfiable(best_solution.clone())),
90                }
91            };
92
93            match conclusion {
94                Some(OptimisationResult::Optimal(solution)) => {
95                    solver.conclude_proof_dual_bound(predicate![objective >= best_objective_value]);
96                    return OptimisationResult::Optimal(solution);
97                }
98                Some(result) => return result,
99                None => {}
100            }
101        }
102    }
103}
pumpkin_core/optimisation/linear_sat_unsat.rs

pumpkin_core/optimisation/
linear_sat_unsat.rs
