Dear Constraints community,
I am excited to announce the first public release of Huub, an extensible Lazy Clause Generation solver written in Rust.
Huub is both a MiniZinc solver and a Rust framework for building customized CP+SAT solving workflows. While it can be used directly through MiniZinc, the main motivation behind Huub is to provide a performant, modular, and extensible platform for experimenting with CP+SAT solving.
In particular, Huub is built around an IPASIR-UP based architecture. Rather than treating the SAT component as a fixed part of the solver implementation, it makes it possible to swap between different underlying SAT solvers. Currently, Huub uses CaDiCaL to provide access to modern SAT features.
As a framework, Huub is intended to make solver-level experimentation more accessible. Users can add their own propagators and branchers, and implement custom (meta-)search algorithms via Huub’s incremental interface. This makes it possible to move beyond a purely modelling-level interaction and incorporate problem-specific solving behaviour directly into the solving process.
Huub achieved 3rd place in the 2025 MiniZinc Challenge, and the solver is now available for others to try.
The version number 100.0.0 is a one-off milestone: Huub is named after my grandfather, who would have turned 100 this year. From here on, Huub will follow semantic versioning.
More information:
Website: https://huub.solutions
API documentation: https://docs.rs/huub
MiniZinc solver package: https://github.com/huub-solver/huub/releases/
Feedback from the community would be very welcome. Please don't hesitate to reach out digitally or in person at CP 2026.
Many thanks to the other project members, Allen Z. Zhong and Peter J. Stuckey, and to everyone who contributed along the way.
Cheers,