Pumpkin is a combinatorial optimisation solver developed within 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, making it straightforward to download and compile. Beyond being a solver, Pumpkin also serves as a research vehicle for the lab — a platform for prototyping and studying new solving techniques, several of which are described in our publications.
A unique feature of Pumpkin is that it can produce certificates of infeasibility and optimality, which can be checked independently of the solver using our formally verified checker. See our CP'24 and CP'26 papers for details.
🥈🥉 Silver (fixed search) and bronze (free search) at the 2026 MiniZinc Challenge
🥉 Bronze (fixed search) at the 2025 MiniZinc Challenge
- Features
- Installation
- Examples
- MiniZinc
- Components
- Contributing
- Team
- Publications Involving Pumpkin
- Citing
- License
Pumpkin can produce certificates of infeasibility and optimality, checkable using our formally verified checker.
Pumpkin currently supports integer variables and the following (global) constraints:
- Cumulative global constraint
- Disjunctive 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 — feel free to open an issue or start a discussion with any questions or feature requests!
To use Pumpkin as a library, use cargo to install it with:
cargo add pumpkin-solverPumpkin 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-solverTo clone the project, run:
git clone https://github.com/ConSol-Lab/Pumpkin.gitSince Pumpkin is written in pure Rust, it is easy to install! After cloning, you can build the project using the most recent stable version of Rust using the following commands:
cargo build # Creates a non-optimized build with debug info
cargo build --release # Creates an optimized buildExamples of how to use the solver are included in the documentation of the different components. For more concrete, runnable examples of solving example problems with Pumpkin, see the examples folder, which includes bibd, nqueens, and disjunctive scheduling.
Pumpkin serves as a backend solver for the MiniZinc modelling language.
To use it as a backend, follow these 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_PATHenvironment 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.
This will add Pumpkin and PumpkinProof (which uses a flattening library specific for proof logging).
Pumpkin consists of several different components:
- The crates contained in pumpkin-crates:
- pumpkin-core; defines the API through which the solver can be used via Rust.
- pumpkin-propagators; contains (most of) the propagators used by Pumpkin.
- pumpkin-constraints; contains convenient ways to add one or more propagators modelling certain constraints to the solver.
- pumpkin-conflict-resolvers; contains the conflict resolvers (e.g., 1UIP or All-Decision conflict resolvers) used by Pumpkin.
- pumpkin-checking; contains the types used for checking the soundness of propagators in Pumpkin.
- The CLI contained in pumpkin-solver.
- The Python bindings contained in pumpkin-solver-py.
- The proof logging contained in drcp-format; a file reader and writer for the DRCP proof format (the proof format used by Pumpkin).
- The (unverified) proof processor contained in pumpkin-proof-processor.
- A debugger for DRCP proofs contained in drcp-debugger.
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-depsWe encourage contributions to Pumpkin via pull requests and issues. When contributing, please ensure that you adhere to the following guidelines.
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)!
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/hooksTo make use of these formatting rules, we require the nightly toolchain. Note that we only use the nightly toolchain for formatting. The nightly version can be installed using the following command:
rustup toolchain install --component rustfmt -- nightlyThe formatting can then be run using:
cargo +nightly fmtPumpkin is developed within the ConSol Lab at TU Delft.
- Emir Demirović: Principal Investigator.
- Maarten Flippo, Imko Marijnissen: Core developers, with contributions from others.
- Formally Verified Certification of Constraint Programming Proofs — Flippo, Sidorov, ten Brink, Pit-Claudel, Demirović; CP 2026
- From Literals to Atomic Constraints: Generalising Conflict-Driven Clause Learning for Constraint Programming — Marijnissen, Flippo, Demirović; CP 2026
- Domain-Independent Dynamic Programming with Constraint Propagation — Marijnissen, Beck, Demirović, Kuroiwa; ICAPS 2026
- Resolution Meets Cutting Planes: Introducing Hypercube Linear Resolution — Flippo, Stuckey, Demirović; CPAIOR 2026
- Conflict Analysis Based on Cutting-Planes for Constraint Programming — Baauw, Flippo, Demirović; CP 2025
- Unite and Lead: Finding Disjunctive Cliques for Scheduling Problems — Sidorov, Marijnissen, Demirović; CP 2025
- A Multi-Stage Proof Logging Framework to Certify the Correctness of CP Solvers — Flippo, Sidorov, Marijnissen, Smits, Demirović; CP 2024
- Towards Step-Wise Explanations of Large Search Trees — Bleukx, Stuckey, Guns; CP 2026
- On Inferring Cumulative Constraints — Sidorov; CP 2026
- Using Certifying Constraint Solvers for Generating Step-wise Explanations — Bleukx, Flippo, Bogaerts, Demirović, Guns; AAAI 2026
Please cite Pumpkin using the following citation:
@inproceedings{marijnissen_et_al:LIPIcs.CP.2026.42,
author = {Marijnissen, Imko and Flippo, Maarten and Demirovi\'{c}, Emir},
title = {{From Literals to Atomic Constraints: Generalising Conflict-Driven Clause Learning for Constraint Programming}},
booktitle = {32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)},
pages = {42:1--42:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
isbn = {978-3-95977-432-1},
issn = {1868-8969},
year = {2026},
volume = {379},
editor = {Beldiceanu, Nicolas},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2026.42},
urn = {urn:nbn:de:0030-drops-266744},
doi = {10.4230/LIPIcs.CP.2026.42},
annote = {Keywords: LCG, CP, CDCL, Lazy Literal, Conflict Analysis, Nogood Propagation},
}If you are using the proof-logging capabilities of Pumpkin, please additionally include 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}
}Pumpkin is dual-licensed under either of
at your option.