Crate pumpkin_solver

Expand description

§Pumpkin

Pumpkin is a combinatorial optimisation solver developed by the ConSol Lab at TU Delft. It is based on the (lazy clause generation) constraint programming paradigm.

Our goal is to keep the solver efficient, easy to use, and well-documented. The solver is written in pure Rust and follows Rust best practices.

A unique feature of Pumpkin is that it can produce a certificate of unsatisfiability. See our CP’24 paper for more details.

The solver currently supports integer variables and a number of (global) constraints:

Cumulative global constraint.
Element global constraint.
Arithmetic constraints: linear integer (in)equalities, integer division, integer multiplication, maximum, absolute value.
Clausal constraints.

We are actively developing Pumpkin and would be happy to hear from you should you have any questions or feature requests!

§Using Pumpkin

Pumpkin can be used to solve a variety of problems. The first step to solving a problem is adding variables:

// We create the solver with default options
let mut solver = Solver::default();

// We create 3 variables
let x = solver.new_bounded_integer(5, 10);
let y = solver.new_bounded_integer(-3, 15);
let z = solver.new_bounded_integer(7, 25);

Then we can add constraints supported by the Solver:

// We create the constraint:
// x + y + z = 17
let c1 = solver.new_constraint_tag();
solver
    .add_constraint(constraints::equals(vec![x, y, z], 17, c1))
    .post();

For finding a solution, a termination::TerminationCondition and a branching::Brancher should be specified, which determine when the solver should stop searching and the variable/value selection strategy which should be used:

// We create a termination condition which allows the solver to run indefinitely
let mut termination = Indefinite;
// And we create a search strategy (in this case, simply the default)
let mut brancher = solver.default_brancher();

Finding a solution to this problem can be done by using Solver::satisfy:

// Then we find a solution to the problem
let result = solver.satisfy(&mut brancher, &mut termination);

if let SatisfactionResult::Satisfiable(satisfiable) = result {
    let solution = satisfiable.solution();

    let value_x = solution.get_integer_value(x);
    let value_y = solution.get_integer_value(y);
    let value_z = solution.get_integer_value(z);

    // The constraint should hold for this solution
    assert!(value_x + value_y + value_z == 17);
} else {
    panic!("This problem should have a solution")
}

Optimizing an objective can be done in a similar way using Solver::optimise; first the objective variable and a constraint over this value are added:

// We add another variable, the objective
let objective = solver.new_bounded_integer(-10, 30);

// We add a constraint which specifies the value of the objective
let c1 = solver.new_constraint_tag();
solver
    .add_constraint(constraints::maximum(vec![x, y, z], objective, c1))
    .post();

Then we can find the optimal solution using Solver::optimise:

// Then we solve to optimality
let callback: fn(&Solver, SolutionReference, &DefaultBrancher) = |_, _, _| {};
let result = solver.optimise(
    &mut brancher,
    &mut termination,
    LinearSatUnsat::new(OptimisationDirection::Minimise, objective, callback),
);

if let OptimisationResult::Optimal(optimal_solution) = result {
    let value_x = optimal_solution.get_integer_value(x);
    let value_y = optimal_solution.get_integer_value(y);
    let value_z = optimal_solution.get_integer_value(z);
    // The maximum objective values is 7;
    // with one possible solution being: {x = 5, y = 5, z = 7, objective = 7}.

    // We check whether the constraint holds again
    assert!(value_x + value_y + value_z == 17);
    // We check whether the newly added constraint for the objective value holds
    assert!(
        max(value_x, max(value_y, value_z)) == optimal_solution.get_integer_value(objective)
    );
    // We check whether this is actually an optimal solution
    assert_eq!(optimal_solution.get_integer_value(objective), 7);
} else {
    panic!("This problem should have an optimal solution")
}

§Obtaining multiple solutions

Pumpkin supports obtaining multiple solutions from the Solver when solving satisfaction problems. The same solution is prevented from occurring multiple times by adding blocking clauses to the solver which means that after iterating over solutions, these solutions will remain blocked if the solver is used again.

// We create the solver with default options
let mut solver = Solver::default();

// We create 3 variables with domains within the range [0, 2]
let x = solver.new_bounded_integer(0, 2);
let y = solver.new_bounded_integer(0, 2);
let z = solver.new_bounded_integer(0, 2);

// We create the all-different constraint
let c1 = solver.new_constraint_tag();
solver.add_constraint(constraints::all_different(vec![x, y, z], c1)).post();

// We create a termination condition which allows the solver to run indefinitely
let mut termination = Indefinite;
// And we create a search strategy (in this case, simply the default)
let mut brancher = solver.default_brancher();

// Then we solve to satisfaction
let mut solution_iterator = solver.get_solution_iterator(&mut brancher, &mut termination);

let mut number_of_solutions = 0;

// We keep track of a list of known solutions
let mut known_solutions = Vec::new();

loop {
    match solution_iterator.next_solution() {
        IteratedSolution::Solution(solution, _, _) => {
            number_of_solutions += 1;
            // We have found another solution, the same invariant should hold
            let value_x = solution.get_integer_value(x);
            let value_y = solution.get_integer_value(y);
            let value_z = solution.get_integer_value(z);
            assert!(x != y && x != z && y != z);

            // It should also be the case that we have not found this solution before
            assert!(!known_solutions.contains(&(value_x, value_y, value_z)));
            known_solutions.push((value_x, value_y, value_z));
        }
        IteratedSolution::Finished => {
            // No more solutions exist
            break;
        }
        IteratedSolution::Unknown => {
            // Our termination condition has caused the solver to terminate
            break;
        }
        IteratedSolution::Unsatisfiable => {
            panic!("Problem should be satisfiable")
        }
    }
}
// There are six possible solutions to this problem
assert_eq!(number_of_solutions, 6)

§Obtaining an unsatisfiable core

Pumpkin allows the user to specify assumptions which can then be used to extract an unsatisfiable core (see results::unsatisfiable::UnsatisfiableUnderAssumptions::extract_core).

// We create the solver with default options
let mut solver = Solver::default();

// We create 3 variables with domains within the range [0, 2]
let x = solver.new_bounded_integer(0, 2);
let y = solver.new_bounded_integer(0, 2);
let z = solver.new_bounded_integer(0, 2);

// We create the all-different constraint
let c1 = solver.new_constraint_tag();
solver.add_constraint(constraints::all_different(vec![x, y, z], c1)).post();

// We create a termination condition which allows the solver to run indefinitely
let mut termination = Indefinite;
// And we create a search strategy (in this case, simply the default)
let mut brancher = solver.default_brancher();

// Then we solve to satisfaction
let assumptions = vec![
    predicate!(x == 1),
    predicate!(y <= 1),
    predicate!(y != 0),
];
let result =
    solver.satisfy_under_assumptions(&mut brancher, &mut termination, &assumptions);

if let SatisfactionResultUnderAssumptions::UnsatisfiableUnderAssumptions(
    mut unsatisfiable,
) = result
{
    {
        let core = unsatisfiable.extract_core();

        // In this case, the core should be equal to all of the assumption literals
        assert_eq!(core, vec![predicate!(y == 1), predicate!(x == 1)].into());
    }
}

§Feature Flags

gzipped-proofs (default): Write proofs to a gzipped file.
debug-checks: Enable expensive assertions in the solver. Turning this on slows down the solver by several orders of magnitude, so it is turned off by default.

Modules§

branching: Contains structures and traits to define the decision making procedure of the [Solver].
constraint_arguments: Contains inputs to constraints.
constraints: Defines the constraints that Pumpkin provides out of the box which can be added to the Solver.
containers: Contains containers which are used by the solver.
convert_case: Converts to and from various cases.
optimisation: Contains structures related to optimissation.
options: Contains the options which can be passed to the [Solver].
predicates: Contains structures which represent certain predicates.
proof: Pumpkin supports proof logging for SAT and CP problems. During search, the solver produces a ProofLog, which is a list of deductions made by the solver.
rand: Utilities for random number generation
results: Contains the outputs of solving using the [Solver].
statistics: Contains structures related to the statistic logging of the [Solver]
termination: Contains the conditions which are used to determine when the [Solver] should terminate even when the state of the satisfaction/optimization problem is unknown.
variables: Contains the variables which are used by the [Solver].

Macros§

conjunction: A macro which allows for the creation of a PropositionalConjunction.
create_statistics_struct: A macro for generating a struct for storing statistics.
declare_inference_label: Conveniently creates InferenceLabel for use in a propagator.
predicate: A macro which allows for the creation of a Predicate.

Structs§

Function: A struct which represents a linear function over weighted Literals, and a constant term.
PropagatorHandle: A typed wrapper around a propagator id that allows retrieving concrete propagators instead of type-erased instances Box<dyn Propagator>.
Solver: The main interaction point which allows the creation of variables, the addition of constraints, and solving problems.

Enums§

ConstraintOperationError: Errors related to adding constraints to the [Solver].

Traits§

Random: Abstraction for randomness, in order to swap out different source of randomness.

Type Aliases§

DefaultBrancher: A brancher which makes use of VSIDS [1] and solution-based phase saving (both adapted for CP).