Pumpkin

ASCII art pumpkin logo

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. As a result, downloading and compiling Pumpkin is straight-forward!

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!

:3rd_place_medal: Pumpkin won the bronze medal in the fixed search track of the 2025 MiniZinc Challenge!

Citing

Please cite Pumpkin using the following citation:

@InProceedings{flippo_et_al:LIPIcs.CP.2024.11,
  author =	{Flippo, Maarten and Sidorov, Konstantin and Marijnissen, Imko and Smits, Jeff and Demirovi\'{c}, Emir},
  title =	{{A Multi-Stage Proof Logging Framework to Certify the Correctness of CP Solvers}},
  booktitle =	{30th International Conference on Principles and Practice of Constraint Programming (CP 2024)},
  pages =	{11:1--11:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-336-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{307},
  editor =	{Shaw, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.11},
  URN =		{urn:nbn:de:0030-drops-206969},
  doi =		{10.4230/LIPIcs.CP.2024.11},
  annote =	{Keywords: proof logging, formal verification, constraint programming}
}

Usage

To use Pumpkin as a library, use cargo to install it with:

cargo add pumpkin-solver

Pumpkin is also the command-line interface to the library. It provides support for (W)CNF and FlatZinc files. Obtaining the solver binary can also be done with cargo:

cargo install pumpkin-solver

Building from Source

To clone the project, run:

git clone https://github.com/ConSol-Lab/pumpkin

Since Pumpkin is written in pure Rust, it is easy to install! After cloning, you can build the project using a version of Rust (1.72.1+) using the following commands:

cargo build           # Creates a non-optimized build with debug info
cargo build --release # Creates an optimized build

MiniZinc

Pumpkin serves as a backend solver for the MiniZinc modelling language.

To use it as such a backend, follow the following steps:

Step 1: Clone the repository and build it using cargo build --release.
Step 2: Install MiniZinc using the appropriate executable or binary archive.
Step 3: Add the following to the MZN_SOLVER_PATH environment variable: <path_to_pumpkin>/minizinc (see this thread on how to do this using a shell).
Step 4: Check whether the installation worked using the command minizinc --help pumpkin.

Components

Pumpkin consists of 3 different crates:

The library contained in pumpkin-solver; defines the API through which the solver can be used via Rust.
The CLI contained in here; defines the usage of Pumpkin through a command line.
The proof logging contained in drcp-format; defines proof logging which can be used in combination with Pumpkin.
The python bindings contained in pumpkin-solver-py; defines the python interface for Pumpkin

The easiest way to get to know the different modules is through the documentation. This documentation can be created automatically using the command:

cargo doc --no-deps

Examples

There are several examples of how to use the solver specified in the documentation of the different components. For more concrete examples of how to use Pumpkin to solve a set of example problems, we refer to the examples folder which contains examples such as bibd, nqueens, and disjunctive scheduling.

Publications Using Pumpkin

M. Flippo, K. Sidorov, I. Marijnissen, J. Smits, and E. Demirović, ‘A Multi-Stage Proof Logging Framework to Certify the Correctness of CP Solvers’, in 30th International Conference on Principles and Practice of Constraint Programming (CP 2024), 2024, vol. 307, p. 11:1-11:20.
R. Baauw, M. Flippo, and E. Demirović, ‘Conflict Analysis Based on Cutting-Planes for Constraint Programming’, in 31st International Conference on Principles and Practice of Constraint Programming (CP 2025), 2025, vol. 340, p. 4:1-4:19.
K. Sidorov, I. Marijnissen, and E. Demirović, ‘Unite and Lead: Finding Disjunctive Cliques for Scheduling Problems’, in 31st International Conference on Principles and Practice of Constraint Programming (CP 2025), 2025, vol. 340, p. 35:1-35:24.

Contributing

We encourage contributions to Pumpkin by merge requests and issues. When contributing please ensure that you adhere to the following guidelines.

Documentation

One of the development goals of Pumpkin is to ensure that the solver is easy-to-use and well-documented. To this end, it is required that any external contribution is well-documented (both the structs/enums/methods and the implementation itself)!

Pre-commit Hooks

To ensure certain standards, we make use of pre-commit hooks. The hooks that we use can be registered using the following command:

cp .githooks/pre-commit .git/hooks

Formatting

To make use of these formatting rules, we require the nightly toolchain. Note that we only use the nightly toolchain for formatting. The nightly version which can be installed using the following command:

rustup toolchain install --component rustfmt -- nightly

The formatting can then be run using:

cargo +nightly fmt