Crate pumpkin_solver

Source
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:

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 with domains within the range [0, 10]
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
solver
    .add_constraint(constraints::equals(vec![x, y, z], 17))
    .post();

For finding a solution, a TerminationCondition and a 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_over_all_propositional_variables();

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(solution) = result {
    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::maximise or Solver::minimise; 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
solver
    .add_constraint(constraints::maximum(vec![x, y, z], objective))
    .post();

Then we can find the optimal solution using Solver::minimise or Solver::maximise:

// Then we solve to optimality
let result = solver.minimise(&mut brancher, &mut termination, objective);

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, 10]
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
solver.add_constraint(constraints::all_different(vec![x, y, z])).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_over_all_propositional_variables();

// 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 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, 10]
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
solver.add_constraint(constraints::all_different(vec![x, y, z])).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_over_all_propositional_variables();

// Then we solve to satisfaction
let assumptions = vec![
    solver.get_literal(predicate!(x == 1)),
    solver.get_literal(predicate!(y <= 1)),
    solver.get_literal(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!(assumptions
            .into_iter()
            .all(|literal| core.contains(&literal)));
    }
}

Modules§

  • branching
    Contains structures and traits to define the decision making procedure of the Solver.
  • 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.
  • encodings
    Contains structures which encode pseudo-boolean constraints via the PseudoBooleanConstraintEncoder.
  • options
    Contains the options which can be passed to the Solver.
  • predicates
    Containts 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.
  • 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§

Structs§

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

Enums§

Traits§

  • Random
    A trait for generating random values; an example of where this is used is in the InDomainRandom value selector where it is used to determine which value in the domain to select.

Type Aliases§