Skip to main content

pumpkin_core/optimisation/
mod.rs

1//! Contains structures related to optimissation.
2
3use solution_callback::SolutionCallback;
4
5use crate::Solver;
6use crate::branching::Brancher;
7use crate::conflict_resolving::ConflictResolver;
8use crate::results::OptimisationResult;
9use crate::termination::TerminationCondition;
10
11pub mod linear_sat_unsat;
12pub mod linear_unsat_sat;
13pub mod solution_callback;
14
15pub trait OptimisationProcedure<B: Brancher, R: ConflictResolver, Callback: SolutionCallback<B, R>>
16{
17    fn optimise(
18        &mut self,
19        brancher: &mut B,
20        termination: &mut impl TerminationCondition,
21        resolver: &mut R,
22        solver: &mut Solver,
23    ) -> OptimisationResult<Callback::Stop>;
24}
25
26/// The type of search which is performed by the solver.
27#[derive(Debug, Clone, Copy, Default)]
28#[cfg_attr(feature = "clap", derive(clap::ValueEnum))]
29pub enum OptimisationStrategy {
30    /// Linear SAT-UNSAT - Starts with a satisfiable solution and tightens the bound on the
31    /// objective variable until an UNSAT result is reached. Can be seen as upper-bounding search.
32    #[default]
33    LinearSatUnsat,
34    /// Linear UNSAT-SAT - Starts with an unsatisfiable solution and tightens the bound on the
35    /// objective variable until a SAT result is reached. Can be seen as lower-bounding search.
36    LinearUnsatSat,
37}
38
39/// The direction of the optimisation, either maximising or minimising.
40#[derive(Debug, Clone, Copy, PartialEq)]
41pub enum OptimisationDirection {
42    Maximise,
43    Minimise,
44}