pumpkin_core/optimisation/
linear_sat_unsat.rs

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

pumpkin_core/optimisation/
linear_sat_unsat.rs
