pumpkin_core/optimisation/
linear_unsat_sat.rs

1use std::num::NonZero;
2
3use super::solution_callback::SolutionCallback;
4use super::OptimisationProcedure;
5use crate::branching::Brancher;
6use crate::optimisation::OptimisationDirection;
7use crate::predicate;
8use crate::proof::ConstraintTag;
9use crate::results::OptimisationResult;
10use crate::results::ProblemSolution;
11use crate::results::SatisfactionResult;
12use crate::results::SatisfactionResultUnderAssumptions;
13use crate::results::Solution;
14use crate::termination::TerminationCondition;
15use crate::variables::IntegerVariable;
16use crate::Solver;
17
18/// Implements the linear UNSAT-SAT (LUS) optimisation procedure.
19#[derive(Debug, Clone, Copy)]
20pub struct LinearUnsatSat<Var, Callback> {
21    direction: OptimisationDirection,
22    objective: Var,
23    solution_callback: Callback,
24}
25
26impl<Var, Callback> LinearUnsatSat<Var, Callback> {
27    /// Create a new instance of [`LinearUnsatSat`].
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, B, Callback> OptimisationProcedure<B, Callback> for LinearUnsatSat<Var, Callback>
42where
43    Var: IntegerVariable,
44    B: Brancher,
45    Callback: SolutionCallback<B>,
46{
47    fn optimise(
48        &mut self,
49        brancher: &mut B,
50        termination: &mut impl TerminationCondition,
51        solver: &mut Solver,
52    ) -> OptimisationResult {
53        let objective = match self.direction {
54            OptimisationDirection::Maximise => self.objective.scaled(-1),
55            OptimisationDirection::Minimise => self.objective.scaled(1),
56        };
57
58        // First we will solve the satisfaction problem without constraining the objective.
59        let primal_solution: Solution = match solver.satisfy(brancher, termination) {
60            SatisfactionResult::Satisfiable(satisfiable) => satisfiable.solution().into(),
61            SatisfactionResult::Unsatisfiable(_, _) => return OptimisationResult::Unsatisfiable,
62            SatisfactionResult::Unknown(_, _) => return OptimisationResult::Unknown,
63        };
64
65        self.solution_callback.on_solution_callback(
66            solver,
67            primal_solution.as_reference(),
68            brancher,
69        );
70
71        let primal_objective = primal_solution.get_integer_value(objective.clone());
72
73        // Then, we iterate from the lower bound of the objective until (excluding) the primal
74        // objective, to find a better solution. The first solution we encounter must be the
75        // optimal solution.
76        //
77        // We purposefully start at one less than the initial lower bound of the objective. Even
78        // though this is a trivial case, this first iteration will output the correct steps to the
79        // proof that allow us to conclude a lower bound even if we are never able to conclude
80        // unsat for `objective <= initial_objective_lower_bound`. If we did not have this, then
81        // the proof would not contain the initial lower bound as an inference, and the dual bound
82        // claim can therefore not be checked.
83
84        let mut objective_lower_bound = solver.lower_bound(&objective);
85        let mut proven_lower_bound = objective_lower_bound;
86
87        while objective_lower_bound < primal_objective {
88            let conclusion = {
89                let solve_result = solver.satisfy_under_assumptions(
90                    brancher,
91                    termination,
92                    &[predicate![objective <= objective_lower_bound]],
93                );
94
95                match solve_result {
96                    SatisfactionResultUnderAssumptions::Satisfiable(satisfiable) => {
97                        Some(OptimisationResult::Optimal(satisfiable.solution().into()))
98                    }
99                    SatisfactionResultUnderAssumptions::UnsatisfiableUnderAssumptions(
100                        _,
101                    ) => {
102                        None
103                    }
104                    SatisfactionResultUnderAssumptions::Unsatisfiable(_) =>
105                        unreachable!("If the problem is unsatisfiable here, it would have been unsatisifable in the initial solve."),
106                    SatisfactionResultUnderAssumptions::Unknown(_) => Some(OptimisationResult::Unknown),
107                }
108            };
109
110            match conclusion {
111                Some(OptimisationResult::Optimal(solution)) => {
112                    self.solution_callback.on_solution_callback(
113                        solver,
114                        primal_solution.as_reference(),
115                        brancher,
116                    );
117
118                    solver
119                        .conclude_proof_dual_bound(predicate![objective >= objective_lower_bound]);
120                    return OptimisationResult::Optimal(solution);
121                }
122                Some(OptimisationResult::Unknown) => {
123                    solver.conclude_proof_dual_bound(predicate![objective >= proven_lower_bound]);
124                    return OptimisationResult::Satisfiable(primal_solution);
125                }
126                Some(result) => return result,
127                None => {}
128            }
129
130            solver
131                .add_clause(
132                    [predicate![objective >= objective_lower_bound + 1]],
133                    ConstraintTag::from_non_zero(NonZero::<u32>::MAX),
134                )
135                .expect("this should always be valid given the previous solves");
136
137            proven_lower_bound = objective_lower_bound + 1;
138            objective_lower_bound = solver.lower_bound(&objective);
139        }
140
141        solver.conclude_proof_dual_bound(predicate![objective >= primal_objective]);
142        OptimisationResult::Optimal(primal_solution)
143    }
144}
pumpkin_core/optimisation/linear_unsat_sat.rs

pumpkin_core/optimisation/
linear_unsat_sat.rs
