Skip to content
41 changes: 41 additions & 0 deletions pumpkin-solver-py/examples/optimisation.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
from argparse import ArgumentParser
from pathlib import Path

from pumpkin_solver import constraints, Model
from pumpkin_solver.optimisation import OptimisationResult


def main(proof: Path | None):
model = Model(proof=proof)

objective = model.new_integer_variable(10, 20, name="objective")

# .. build the model here

def on_solution(solution):
objective_value = solution.int_value(objective)
print(f"objective_value={objective_value}")

status = model.optimise(objective, on_solution=on_solution)
match status:
case OptimisationResult.Optimal(_solution):
print("OPTIMAL")

case OptimisationResult.Satisfiable(_solution):
print("SATISFIABLE")

case OptimisationResult.Unsatisfiable():
print("UNSATISFIABLE")

case OptimisationResult.Unknown():
print("UNKNOWN")


if __name__ == "__main__":
arg_parser = ArgumentParser()

arg_parser.add_argument("--proof", type=Path, help="The proof file.", default=None)

args = arg_parser.parse_args()

main(args.proof)
14 changes: 12 additions & 2 deletions pumpkin-solver-py/src/model.rs
Original file line number Diff line number Diff line change
Expand Up @@ -246,13 +246,15 @@ impl Model {
}
}

#[pyo3(signature = (objective, optimiser=Optimiser::LinearSatUnsat, direction=Direction::Minimise, timeout=None))]
#[pyo3(signature = (objective, optimiser=Optimiser::LinearSatUnsat, direction=Direction::Minimise, timeout=None, on_solution=None))]
fn optimise(
&mut self,
py: Python<'_>,
objective: IntExpression,
optimiser: Optimiser,
direction: Direction,
timeout: Option<f32>,
on_solution: Option<Py<PyAny>>,
) -> OptimisationResult {
let mut termination = get_termination(timeout);

Expand All @@ -263,7 +265,15 @@ impl Model {

let objective = objective.0;

let callback: fn(&Solver, SolutionReference, &DefaultBrancher) = |_, _, _| {};
let callback = move |_: &Solver, solution: SolutionReference<'_>, _: &DefaultBrancher| {
let python_solution = crate::result::Solution::from(solution);

if let Some(on_solution_callback) = on_solution.as_ref() {
let _ = on_solution_callback
.call(py, (python_solution,), None)
.expect("failed to call solution callback");
}
};

let result = match optimiser {
Optimiser::LinearSatUnsat => self.solver.optimise(
Expand Down