Developing Huub

This page contains information for developers working on Huub itself, including building, testing, debugging the solver, and understanding its dependencies and inspirations.

MiniZinc Integration

For local MiniZinc debugging, you can assemble a staging deployment tree under target/staging with the current debug and release binaries, the MiniZinc library, generated solver configurations (huub.msc and huub-dev.msc), and generated completions using the following commands:

cargo xtask stage

This creates symlinks target/staging/bin/huub and target/staging/bin/huub-dev, pointing at the current release and debug builds (don't forget to trigger cargo build or cargo build --release before running!), and the associated MiniZinc solver configurations in huub.msc and huub-dev.msc in target/staging/share/minizinc/solvers.

The huub-dev.msc solver entry uses the Huub (dev) name and the solutions.huub-dev identifier so it is easy to distinguish from a release build.

Adding target/staging/share/minizinc/solvers to the MZN_SOLVER_PATH environment variable will allow you to use the two solver configurations as follows:

minizinc --solver huub [ARGS...]
# or
minizinc --solver huub-dev [ARGS...]

Compiling and Running MiniZinc Models

Alternatively, you can compile a MiniZinc instance and run it using a current build of Huub.

This process can be split into two steps. First, produce the required .fzn.json and .ozn files using the following command:

minizinc --solver huub --compile [OTHER FLAGS AND INSTANCE FILES]

Then, run the current version of Huub using cargo and pipe the result back into MiniZinc to evaluate the output:

cargo run [BUILD FLAGS] -- [HUUB FLAGS AND FZNJSON FILE] | minizinc --ozn-file [OZN FILE]

Debugging with a Debugger

To attach a debugger directly, you can point it at the latest build in ./target/debug or ./target/release-with-debug (created using cargo build or cargo build --profile release-with-debug) in combination with the [HUUB FLAGS AND FZNJSON FILE].

For example, the following command can be used to run Huub with the lldb debugger:

lldb -- ./target/debug/huub [HUUB FLAGS AND FZNJSON FILE]

SAT Solver Integration

Huub is built using the IPASIR-UP interface for SAT solvers, proposed by Fazakas et al.. Huub is tested with the following solvers that implement this interface:

CaDiCaL

Encoding to SAT

Huub uses Pindakaas, a Rust crate for SAT solving and encoding to CNF, for its SAT solver integration and CNF encoding.

If you're exploring CP+SAT approaches, you might also be interested in:

Chuffed — A C++ CP+SAT solver with a focus on performance.
OR-Tools — Google's operations research library with multiple solving paradigms, based around CP+SAT.
Pumpkin — Another CP+SAT solver written in Rust.

Keyboard shortcuts