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    fn run_optimisation<B, R>(
41        &mut self,
42        brancher: &mut B,
43        termination: &mut impl TerminationCondition,
44        resolver: &mut R,
45        solver: &mut Solver,
46        objective: impl IntegerVariable,
47        mut best_solution: Solution,
48    ) -> OptimisationResult<Callback::Stop>
49    where
50        Callback: SolutionCallback<B, R>,
51        B: Brancher,
52        R: ConflictResolver,
53    {
54        loop {
55            let callback_result = self.solution_callback.on_solution_callback(
56                solver,
57                best_solution.as_reference(),
58                brancher,
59                resolver,
60            );
61
62            if let ControlFlow::Break(stop) = callback_result {
63                return OptimisationResult::Stopped(best_solution, stop);
64            }
65
66            let best_objective_value = best_solution.get_integer_value(objective.clone());
67
68            let conclusion = {
69                let solve_result = solver.satisfy_under_assumptions(
70                    brancher,
71                    termination,
72                    resolver,
73                    &[predicate![objective <= best_objective_value - 1]],
74                );
75
76                match solve_result {
77                    SatisfactionResultUnderAssumptions::Satisfiable(satisfiable) => {
78                        best_solution = satisfiable.solution().into();
79                        None
80                    }
81                    SatisfactionResultUnderAssumptions::UnsatisfiableUnderAssumptions(_) => {
82                        Some(OptimisationResult::Optimal(best_solution.clone()))
83                    }
84                    SatisfactionResultUnderAssumptions::Unsatisfiable(_) => unreachable!(
85                        "If the problem is unsatisfiable here, it would have been unsatisifable in the initial solve."
86                    ),
87                    SatisfactionResultUnderAssumptions::Unknown(_) => {
88                        Some(OptimisationResult::Satisfiable(best_solution.clone()))
89                    }
90                }
91            };
92
93            match conclusion {
94                Some(OptimisationResult::Optimal(solution)) => {
95                    return OptimisationResult::Optimal(solution);
96                }
97                Some(result) => return result,
98                None => {}
99            }
100        }
101    }
102}
103
104impl<Var, Callback, B, R> OptimisationProcedure<B, R, Callback> for LinearSatUnsat<Var, Callback>
105where
106    Var: IntegerVariable,
107    B: Brancher,
108    R: ConflictResolver,
109    Callback: SolutionCallback<B, R>,
110    Callback::Stop: std::fmt::Debug,
111{
112    fn optimise(
113        &mut self,
114        brancher: &mut B,
115        termination: &mut impl TerminationCondition,
116        resolver: &mut R,
117        solver: &mut Solver,
118    ) -> OptimisationResult<Callback::Stop> {
119        let objective = match self.direction {
120            OptimisationDirection::Maximise => self.objective.scaled(-1),
121            OptimisationDirection::Minimise => self.objective.scaled(1),
122        };
123
124        // First we will solve the satisfaction problem without constraining the objective.
125        let initial_solution: Solution = match solver.satisfy(brancher, termination, resolver) {
126            SatisfactionResult::Satisfiable(satisfiable) => satisfiable.solution().into(),
127            SatisfactionResult::Unsatisfiable(_, _, _) => return OptimisationResult::Unsatisfiable,
128            SatisfactionResult::Unknown(_, _, _) => return OptimisationResult::Unknown,
129        };
130
131        let optimisation_result = self.run_optimisation(
132            brancher,
133            termination,
134            resolver,
135            solver,
136            objective.clone(),
137            initial_solution,
138        );
139
140        match optimisation_result {
141            OptimisationResult::Optimal(solution) => {
142                let objective_value = solution.get_integer_value(objective.clone());
143                solver.conclude_proof_dual_bound(predicate![objective >= objective_value]);
144
145                OptimisationResult::Optimal(solution)
146            }
147            OptimisationResult::Unsatisfiable => {
148                solver.conclude_proof_unsat();
149                OptimisationResult::Unsatisfiable
150            }
151
152            result @ (OptimisationResult::Satisfiable(_)
153            | OptimisationResult::Stopped(_, _)
154            | OptimisationResult::Unknown) => result,
155        }
156    }
157}
pumpkin_core/optimisation/linear_sat_unsat.rs

pumpkin_core/optimisation/
linear_sat_unsat.rs
