pumpkin_core/optimisation/
linear_unsat_sat.rs

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

pumpkin_core/optimisation/
linear_unsat_sat.rs
