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(pumpkin_constraints::equals(vec![x, y, z], 17, c1))
    .post();

For finding a solution, a core::termination::TerminationCondition, a core::branching::Brancher and a core::conflict_resolving::ConflictResolver 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();
// Finally, we create a default conflict resolver
let mut resolver = ResolutionResolver::default();

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, &mut resolver);

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(pumpkin_constraints::maximum(vec![x, y, z], objective, c1))
    .post();

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


let callback = |_: &Solver, _: SolutionReference, _: &DefaultBrancher, _: &ResolutionResolver| -> ControlFlow<()> {
    return ControlFlow::Continue(());
};

// Then we solve to optimality
let result = solver.optimise(
    &mut brancher,
    &mut termination,
    &mut resolver,
    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(pumpkin_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();
// Finally, we create a default conflict resolver
let mut resolver = ResolutionResolver::default();

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

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 core::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(pumpkin_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();
// Finally, we create a default conflict resolver
let mut resolver = ResolutionResolver::default();

// 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,
    &mut resolver,
    &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!(x == 1), predicate!(y <= 1), predicate!(y != 0)].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§

conflict_resolvers: Contains the implementations of ConflictResolvers, and NogoodMinimisers.
core: The core interfaces and structures used by the pumpkin solver.
propagators: Contains the implementations of Propagators.

Structs§

Solver: The main interaction point which allows the creation of variables, the addition of constraints, and solving problems.

Functions§

absolute: Creates the Constraint |signed| = absolute.
all_different: Creates the Constraint that enforces that all the given variables are distinct.
binary_equals: Creates the NegatableConstraint lhs = rhs.
binary_greater_than: Creates the NegatableConstraint lhs > rhs.
binary_greater_than_or_equals: Creates the NegatableConstraint lhs >= rhs.
binary_less_than: Creates the NegatableConstraint lhs < rhs.
binary_less_than_or_equals: Creates the NegatableConstraint lhs <= rhs.
binary_not_equals: Creates the NegatableConstraint lhs != rhs.
boolean_equals: Creates the Constraint ∑ weights_i * bools_i == rhs.
boolean_less_than_or_equals: Creates the Constraint ∑ weights_i * bools_i <= rhs.
clause: Creates the NegatableConstraint \/ literal
conjunction: Creates the NegatableConstraint /\ literal
cumulative: Creates the Cumulative Constraint.
cumulative_with_options: Creates the Cumulative Constraint with the provided CumulativeOptions.
disjunctive_strict: Creates the Disjunctive Constraint (also called the NoOverlap Constraint or the Unary Resource Constraint).
division: Creates the Constraint numerator / denominator = rhs.
element: Creates the element Constraint which states that array[index] = rhs.
equals: Creates the NegatableConstraint ∑ terms_i = rhs.
greater_than: Create the NegatableConstraint ∑ terms_i > rhs.
greater_than_or_equals: Create the NegatableConstraint ∑ terms_i >= rhs.
less_than: Create the NegatableConstraint ∑ terms_i < rhs.
less_than_or_equals: Create the NegatableConstraint ∑ terms_i <= rhs.
maximum: Creates the Constraint max(array) = m.
minimum: Creates the Constraint min(array) = m.
negative_table: Create the negative table NegatableConstraint.
not_equals: Create the NegatableConstraint ∑ terms_i != rhs.
plus: Creates the Constraint a + b = c.
table: Create the table NegatableConstraint.
times: Creates the Constraint a * b = c.