pumpkin_core/optimisation/
linear_unsat_sat.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 UNSAT-SAT (LUS) optimisation procedure.
16#[derive(Debug, Clone, Copy)]
17pub struct LinearUnsatSat<Var, Callback> {
18    direction: OptimisationDirection,
19    objective: Var,
20    solution_callback: Callback,
21}
22
23impl<Var, Callback> LinearUnsatSat<Var, Callback> {
24    /// Create a new instance of [`LinearUnsatSat`].
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, B, Callback> OptimisationProcedure<B, Callback> for LinearUnsatSat<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        let initial_objective_lower_bound = solver.lower_bound(&objective);
56
57        // First we will solve the satisfaction problem without constraining the objective.
58        let primal_solution: Solution = match solver.satisfy(brancher, termination) {
59            SatisfactionResult::Satisfiable(satisfiable) => satisfiable.solution().into(),
60            SatisfactionResult::Unsatisfiable(_) => return OptimisationResult::Unsatisfiable,
61            SatisfactionResult::Unknown(_) => return OptimisationResult::Unknown,
62        };
63
64        let primal_objective = primal_solution.get_integer_value(objective.clone());
65
66        // Then, we iterate from the lower bound of the objective until (excluding) the primal
67        // objective, to find a better solution. The first solution we encounter must be the
68        // optimal solution.
69        //
70        // We purposefully start at one less than the initial lower bound of the objective. Even
71        // though this is a trivial case, this first iteration will output the correct steps to the
72        // proof that allow us to conclude a lower bound even if we are never able to conclude
73        // unsat for `objective <= initial_objective_lower_bound`. If we did not have this, then
74        // the proof would not contain the initial lower bound as an inference, and the dual bound
75        // claim can therefore not be checked.
76        for objective_lower_bound in (initial_objective_lower_bound - 1)..primal_objective {
77            let conclusion = {
78                let solve_result = solver.satisfy_under_assumptions(
79                    brancher,
80                    termination,
81                    &[predicate![objective <= objective_lower_bound]],
82                );
83
84                match solve_result {
85                    SatisfactionResultUnderAssumptions::Satisfiable(satisfiable) => {
86                        Some(OptimisationResult::Optimal(satisfiable.solution().into()))
87                    }
88                    SatisfactionResultUnderAssumptions::UnsatisfiableUnderAssumptions(
89                        _,
90                    ) => {
91                        None
92                    }
93                    SatisfactionResultUnderAssumptions::Unsatisfiable(_) =>
94                        unreachable!("If the problem is unsatisfiable here, it would have been unsatisifable in the initial solve."),
95                    SatisfactionResultUnderAssumptions::Unknown(_) => Some(OptimisationResult::Unknown),
96                }
97            };
98
99            match conclusion {
100                Some(OptimisationResult::Optimal(solution)) => {
101                    self.solution_callback.on_solution_callback(
102                        solver,
103                        primal_solution.as_reference(),
104                        brancher,
105                    );
106
107                    solver
108                        .conclude_proof_dual_bound(predicate![objective >= objective_lower_bound]);
109                    return OptimisationResult::Optimal(solution);
110                }
111                Some(OptimisationResult::Unknown) => {
112                    solver.conclude_proof_dual_bound(predicate![
113                        objective >= objective_lower_bound - 1
114                    ]);
115                }
116                Some(result) => return result,
117                None => {}
118            }
119        }
120
121        solver.conclude_proof_dual_bound(predicate![objective >= primal_objective]);
122        OptimisationResult::Optimal(primal_solution)
123    }
124}
pumpkin_core/optimisation/linear_unsat_sat.rs

pumpkin_core/optimisation/
linear_unsat_sat.rs
