Crate huub 

Huub - a CP+SAT solver library for better decisions.

Huub is an efficient Rust library for developing constraint-based decision and optimization systems with learning capabilities. It combines the modelling strengths of constraint programming (CP) with the learning, conflict analysis, and proof machinery of Boolean satisfiability (SAT) solving.

Huub is built for combinatorial problems such as scheduling, rostering, packing, planning, configuration, and MiniZinc workflows. It lets models use high-level decision variables and constraints while still allowing the SAT engine to learn from deductions and failures during search.

The solver is designed to be reliable, performant, and extensible. It is well-tested, performs state-of-the-art preprocessing before search begins, combines strong propagation with modern SAT solving techniques, and exposes extension points for custom propagators, branchers, decision variable views, and SAT backends.

Quick start

A typical Huub workflow starts by building a model::Model, converting it to a solver::Solver, and querying solution values through the lowered solver views.

let mut model = Model::default();
let x = model.new_int_decision(0..=5);
let y = model.new_int_decision(0..=5);

model.linear(x + y).eq(5).post();
model.unique(vec![x, y]).post();

let (mut solver, map): (Solver, _) = model.lower().to_solver()?;
let x = map.get(&mut solver, x);
let y = map.get(&mut solver, y);

let mut solution = None;
let status = solver
	.solve()
	.on_solution(|sol| {
		solution = Some((x.val(sol), y.val(sol)));
	})
	.satisfy();

assert_eq!(status, Status::Satisfied);
let (x, y) = solution.unwrap();
assert_eq!(x + y, 5);
assert_ne!(x, y);

Modules

actions

Traits that encapsulate different sets of actions that can be performed at different phases and by different objects in the solving process.

constraints

Module containing the definitions for propagators and their implementations.

helpers

Module containing general, e.g. purely numeric, structures or used in multiple places in the library and are not exposed to the user.

lower

Data structures to store Model parts for analyses and for the reformulation process of creating a Solver object from a Model.

model

The modelling layer for constructing, simplifying, and lowering problem instances.

solver

Module containing the central solving infrastructure.

views

Module containing generic views for decision variables.

Type Aliases

Set

Type alias for an efficient set of values, that is suitable to track decision variable domains.