Skip to content

feat: Add logging for branchers #135

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 9 commits into from
Apr 9, 2025
8 changes: 6 additions & 2 deletions pumpkin-py/src/model.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,10 +9,12 @@ use pumpkin_solver::options::SolverOptions;
use pumpkin_solver::predicate;
use pumpkin_solver::proof::Format;
use pumpkin_solver::proof::ProofLog;
use pumpkin_solver::results::SolutionReference;
use pumpkin_solver::termination::Indefinite;
use pumpkin_solver::variables::DomainId;
use pumpkin_solver::variables::Literal;
use pumpkin_solver::ConstraintOperationError;
use pumpkin_solver::DefaultBrancher;
use pumpkin_solver::Solver;
use pyo3::prelude::*;

Expand Down Expand Up @@ -261,16 +263,18 @@ impl Model {

let objective = objective.to_affine_view(&variable_map);

let callback: fn(&Solver, SolutionReference, &DefaultBrancher) = |_, _, _| {};

let result = match optimiser {
Optimiser::LinearSatUnsat => solver.optimise(
&mut brancher,
&mut Indefinite,
LinearSatUnsat::new(direction, objective, |_, _| {}),
LinearSatUnsat::new(direction, objective, callback),
),
Optimiser::LinearUnsatSat => solver.optimise(
&mut brancher,
&mut Indefinite,
LinearUnsatSat::new(direction, objective, |_, _| {}),
LinearUnsatSat::new(direction, objective, callback),
),
};

Expand Down
12 changes: 7 additions & 5 deletions pumpkin-solver/src/api/outputs/solution_iterator.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
//! Contains the structures corresponding to solution iterations.

use std::fmt::Debug;

use super::SatisfactionResult::Satisfiable;
use super::SatisfactionResult::Unknown;
use super::SatisfactionResult::Unsatisfiable;
Expand All @@ -13,7 +15,7 @@ use crate::Solver;

/// A struct which allows the retrieval of multiple solutions to a satisfaction problem.
#[derive(Debug)]
pub struct SolutionIterator<'solver, 'brancher, 'termination, B: Brancher, T> {
pub struct SolutionIterator<'solver, 'brancher, 'termination, B, T> {
solver: &'solver mut Solver,
brancher: &'brancher mut B,
termination: &'termination mut T,
Expand All @@ -40,7 +42,7 @@ impl<'solver, 'brancher, 'termination, B: Brancher, T: TerminationCondition>

/// Find a new solution by blocking the previous solution from being found. Also calls the
/// [`Brancher::on_solution`] method from the [`Brancher`] used to run the initial solve.
pub fn next_solution(&mut self) -> IteratedSolution {
pub fn next_solution(&mut self) -> IteratedSolution<B> {
if let Some(blocking_clause) = self.next_blocking_clause.take() {
if self.solver.add_clause(blocking_clause).is_err() {
return IteratedSolution::Finished;
Expand All @@ -51,7 +53,7 @@ impl<'solver, 'brancher, 'termination, B: Brancher, T: TerminationCondition>
Satisfiable(solution) => {
self.has_solution = true;
self.next_blocking_clause = Some(get_blocking_clause(&solution));
IteratedSolution::Solution(solution, self.solver)
IteratedSolution::Solution(solution, self.solver, self.brancher)
}
Unsatisfiable => {
if self.has_solution {
Expand Down Expand Up @@ -82,9 +84,9 @@ fn get_blocking_clause(solution: &Solution) -> Vec<Predicate> {
reason = "these will not be stored in bulk, so this is not an issue"
)]
#[derive(Debug)]
pub enum IteratedSolution<'a> {
pub enum IteratedSolution<'a, B> {
/// A new solution was identified.
Solution(Solution, &'a Solver),
Solution(Solution, &'a Solver, &'a B),

/// No more solutions exist.
Finished,
Expand Down
13 changes: 9 additions & 4 deletions pumpkin-solver/src/api/solver.rs
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,7 @@ use crate::engine::ConstraintSatisfactionSolver;
use crate::optimisation::linear_sat_unsat::LinearSatUnsat;
#[cfg(doc)]
use crate::optimisation::linear_unsat_sat::LinearUnsatSat;
use crate::optimisation::solution_callback::SolutionCallback;
use crate::optimisation::OptimisationProcedure;
use crate::options::SolverOptions;
#[cfg(doc)]
Expand Down Expand Up @@ -402,12 +403,16 @@ impl Solver {
///
/// It returns an [`OptimisationResult`] which can be used to retrieve the optimal solution if
/// it exists.
pub fn optimise<Var: IntegerVariable, Callback: Fn(&Solver, SolutionReference)>(
pub fn optimise<B, Callback>(
&mut self,
brancher: &mut impl Brancher,
brancher: &mut B,
termination: &mut impl TerminationCondition,
mut optimisation_procedure: impl OptimisationProcedure<Var, Callback>,
) -> OptimisationResult {
mut optimisation_procedure: impl OptimisationProcedure<B, Callback>,
) -> OptimisationResult
where
B: Brancher,
Callback: SolutionCallback<B>,
{
optimisation_procedure.optimise(brancher, termination, self)
}
}
Expand Down
10 changes: 10 additions & 0 deletions pumpkin-solver/src/bin/pumpkin-solver/flatzinc/instance.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ use std::fmt::Write;
use std::rc::Rc;

use pumpkin_solver::branching::branchers::dynamic_brancher::DynamicBrancher;
use pumpkin_solver::optimisation::OptimisationDirection;
use pumpkin_solver::variables::DomainId;
use pumpkin_solver::variables::Literal;

Expand All @@ -15,6 +16,15 @@ pub(crate) enum FlatzincObjective {
Minimize(DomainId),
}

impl From<FlatzincObjective> for (OptimisationDirection, DomainId) {
fn from(value: FlatzincObjective) -> Self {
match value {
FlatzincObjective::Maximize(domain_id) => (OptimisationDirection::Maximise, domain_id),
FlatzincObjective::Minimize(domain_id) => (OptimisationDirection::Minimise, domain_id),
}
}
}

#[derive(Default)]
pub(crate) struct FlatZincInstance {
pub(super) outputs: Vec<Output>,
Expand Down
50 changes: 27 additions & 23 deletions pumpkin-solver/src/bin/pumpkin-solver/flatzinc/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ use pumpkin_solver::results::OptimisationResult;
use pumpkin_solver::results::ProblemSolution;
use pumpkin_solver::results::SatisfactionResult;
use pumpkin_solver::results::SolutionReference;
use pumpkin_solver::statistics::StatisticLogger;
use pumpkin_solver::termination::Combinator;
use pumpkin_solver::termination::OsSignal;
use pumpkin_solver::termination::TerminationCondition;
Expand All @@ -33,7 +34,6 @@ use pumpkin_solver::variables::DomainId;
use pumpkin_solver::Solver;

use self::instance::FlatZincInstance;
use self::instance::FlatzincObjective;
use self::instance::Output;
use crate::flatzinc::error::FlatZincError;

Expand All @@ -57,13 +57,15 @@ pub(crate) struct FlatZincOptions {
}

fn solution_callback(
brancher: &impl Brancher,
instance_objective_function: Option<DomainId>,
options_all_solutions: bool,
outputs: &[Output],
solver: &Solver,
solution: SolutionReference,
) {
if options_all_solutions || instance_objective_function.is_none() {
brancher.log_statistics(StatisticLogger::default());
if let Some(objective) = instance_objective_function {
solver.log_statistics_with_objective(solution.get_integer_value(objective) as i64);
} else {
Expand Down Expand Up @@ -100,28 +102,26 @@ pub(crate) fn solve(
instance.search.expect("Expected a search to be defined")
};

let (direction, objective) = match instance.objective_function {
Some(FlatzincObjective::Maximize(domain_id)) => {
(OptimisationDirection::Maximise, domain_id)
}
Some(FlatzincObjective::Minimize(domain_id)) => {
(OptimisationDirection::Minimise, domain_id)
}
None => {
satisfy(options, &mut solver, brancher, termination, outputs);
return Ok(());
}
};
let (direction, objective): (OptimisationDirection, DomainId) =
match instance.objective_function {
Some(objective) => objective.into(),
None => {
satisfy(options, &mut solver, brancher, termination, outputs);
return Ok(());
}
};

let callback = |solver: &Solver, solution: SolutionReference<'_>| {
solution_callback(
Some(objective),
options.all_solutions,
&outputs,
solver,
solution,
);
};
let callback =
|solver: &Solver, solution: SolutionReference<'_>, brancher: &DynamicBrancher| {
solution_callback(
brancher,
Some(objective),
options.all_solutions,
&outputs,
solver,
solution,
);
};

let result = match options.optimisation_strategy {
OptimisationStrategy::LinearSatUnsat => solver.optimise(
Expand All @@ -139,6 +139,8 @@ pub(crate) fn solve(
match result {
OptimisationResult::Optimal(optimal_solution) => {
if !options.all_solutions {
brancher.log_statistics(StatisticLogger::default());
solver.log_statistics();
print_solution_from_solver(optimal_solution.as_reference(), &instance.outputs)
}
println!("==========");
Expand Down Expand Up @@ -172,8 +174,9 @@ fn satisfy(
let mut solution_iterator = solver.get_solution_iterator(&mut brancher, &mut termination);
loop {
match solution_iterator.next_solution() {
IteratedSolution::Solution(solution, solver) => {
IteratedSolution::Solution(solution, solver, brancher) => {
solution_callback(
brancher,
None,
options.all_solutions,
&outputs,
Expand All @@ -200,6 +203,7 @@ fn satisfy(
} else {
match solver.satisfy(&mut brancher, &mut termination) {
SatisfactionResult::Satisfiable(solution) => solution_callback(
&brancher,
None,
options.all_solutions,
&outputs,
Expand Down
8 changes: 8 additions & 0 deletions pumpkin-solver/src/branching/brancher.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,11 +12,14 @@ use crate::branching::value_selection::ValueSelector;
#[cfg(doc)]
use crate::branching::variable_selection::VariableSelector;
use crate::branching::SelectionContext;
#[cfg(doc)]
use crate::create_statistics_struct;
use crate::engine::predicates::predicate::Predicate;
use crate::engine::variables::DomainId;
use crate::engine::Assignments;
#[cfg(doc)]
use crate::results::solution_iterator::SolutionIterator;
use crate::statistics::StatisticLogger;
#[cfg(doc)]
use crate::Solver;

Expand All @@ -32,6 +35,11 @@ use crate::Solver;
/// If the [`Brancher`] (or any component thereof) is implemented incorrectly then the
/// behaviour of the solver is undefined.
pub trait Brancher {
/// Logs statistics of the brancher using the provided [`StatisticLogger`].
///
/// It is recommended to create a struct through the [`create_statistics_struct!`] macro!
fn log_statistics(&self, _statistic_logger: StatisticLogger) {}

/// Returns the next decision concerning a single variable and value; it returns the
/// [`Predicate`] corresponding to this decision (or [`None`] if all variables under
/// consideration are assigned).
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ use crate::branching::SelectionContext;
use crate::engine::predicates::predicate::Predicate;
use crate::engine::variables::DomainId;
use crate::engine::Assignments;
use crate::statistics::StatisticLogger;
use crate::DefaultBrancher;
use crate::Solver;

Expand Down Expand Up @@ -110,6 +111,12 @@ impl<OtherBrancher: Brancher> Brancher for AlternatingBrancher<OtherBrancher> {
}
}

fn log_statistics(&self, statistic_logger: StatisticLogger) {
self.default_brancher
.log_statistics(statistic_logger.clone());
self.other_brancher.log_statistics(statistic_logger);
}

fn on_appearance_in_conflict_predicate(&mut self, predicate: Predicate) {
self.default_brancher
.on_appearance_in_conflict_predicate(predicate);
Expand Down
32 changes: 31 additions & 1 deletion pumpkin-solver/src/branching/branchers/autonomous_search.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
use super::independent_variable_value_brancher::IndependentVariableValueBrancher;
use crate::basic_types::moving_averages::CumulativeMovingAverage;
use crate::basic_types::moving_averages::MovingAverage;
use crate::basic_types::PredicateId;
use crate::basic_types::PredicateIdGenerator;
use crate::basic_types::SolutionReference;
Expand All @@ -9,9 +11,12 @@ use crate::branching::BrancherEvent;
use crate::branching::SelectionContext;
use crate::containers::KeyValueHeap;
use crate::containers::StorageKey;
use crate::create_statistics_struct;
use crate::engine::predicates::predicate::Predicate;
use crate::engine::Assignments;
use crate::results::Solution;
use crate::statistics::Statistic;
use crate::statistics::StatisticLogger;
use crate::variables::DomainId;
use crate::DefaultBrancher;
/// A [`Brancher`] that combines [VSIDS \[1\]](https://dl.acm.org/doi/pdf/10.1145/378239.379017)
Expand Down Expand Up @@ -56,7 +61,6 @@ use crate::DefaultBrancher;
/// value-selection heuristic to simulate local search behavior in complete solvers’, in the
/// proceedings of the Principles and Practice of Constraint Programming (CP 2018).
#[derive(Debug)]

pub struct AutonomousSearch<BackupBrancher> {
/// Predicates are mapped to ids. This is used internally in the heap.
predicate_id_info: PredicateIdGenerator,
Expand All @@ -83,8 +87,19 @@ pub struct AutonomousSearch<BackupBrancher> {
/// If the heap does not contain any more unfixed predicates then this backup_brancher will be
/// used instead.
backup_brancher: BackupBrancher,

statistics: AutonomousSearchStatistics,
}

create_statistics_struct!(AutonomousSearchStatistics {
num_backup_called: usize,
num_predicates_removed: usize,
num_calls: usize,
num_predicates_added: usize,
average_size_of_heap: CumulativeMovingAverage<usize>,
num_assigned_predicates_encountered: usize,
});

const DEFAULT_VSIDS_INCREMENT: f64 = 1.0;
const DEFAULT_VSIDS_MAX_THRESHOLD: f64 = 1e100;
const DEFAULT_VSIDS_DECAY_FACTOR: f64 = 0.95;
Expand All @@ -110,6 +125,7 @@ impl DefaultBrancher {
RandomSelector::new(assignments.get_domains()),
RandomSplitter,
),
statistics: Default::default(),
}
}
}
Expand All @@ -130,6 +146,7 @@ impl<BackupSelector> AutonomousSearch<BackupSelector> {
decay_factor: DEFAULT_VSIDS_DECAY_FACTOR,
best_known_solution: None,
backup_brancher,
statistics: Default::default(),
}
}

Expand All @@ -144,6 +161,8 @@ impl<BackupSelector> AutonomousSearch<BackupSelector> {
/// Bumps the activity of a predicate by [`Vsids::increment`].
/// Used when a predicate is encountered during a conflict.
fn bump_activity(&mut self, predicate: Predicate) {
self.statistics.num_predicates_added +=
(!self.predicate_id_info.has_id_for_predicate(predicate)) as usize;
let id = self.predicate_id_info.get_id(predicate);
self.resize_heap(id);
self.heap.restore_key(id);
Expand Down Expand Up @@ -181,6 +200,7 @@ impl<BackupSelector> AutonomousSearch<BackupSelector> {
.get_predicate(*candidate)
.expect("We expected present predicates to be registered.");
if context.is_predicate_assigned(predicate) {
self.statistics.num_assigned_predicates_encountered += 1;
let _ = self.heap.pop_max();

// We know that this predicate is now dormant
Expand Down Expand Up @@ -226,17 +246,27 @@ impl<BackupSelector> AutonomousSearch<BackupSelector> {

impl<BackupBrancher: Brancher> Brancher for AutonomousSearch<BackupBrancher> {
fn next_decision(&mut self, context: &mut SelectionContext) -> Option<Predicate> {
self.statistics.num_calls += 1;
self.statistics
.average_size_of_heap
.add_term(self.heap.num_nonremoved_elements());
let result = self
.next_candidate_predicate(context)
.map(|predicate| self.determine_polarity(predicate));
if result.is_none() && !context.are_all_variables_assigned() {
// There are variables for which we do not have a predicate, rely on the backup
self.statistics.num_backup_called += 1;
self.backup_brancher.next_decision(context)
} else {
result
}
}

fn log_statistics(&self, statistic_logger: StatisticLogger) {
let statistic_logger = statistic_logger.attach_to_prefix("AutonomousSearch");
self.statistics.log(statistic_logger);
}

fn on_backtrack(&mut self) {
self.backup_brancher.on_backtrack()
}
Expand Down
Loading