unifierv0.6.0

CASOON Open Source

Model it in Rust. Solve it anytime.

unifier lets you state a problem as variables, domains, rules and goals, and finds the best answer it can: proven optimal when the search completes, the best so far when time runs out, and a clear Infeasible when no answer exists.

cargo add unifier
MITearlycrates.io 0.6.0Rust 1.87+
Terminal: cargo run -q --release --example job_shop prints Job shop: 3 jobs, 3 machines, horizon 21; Status: Optimal; Score: Feasible(strong=0, medium=0, weak=-11); Makespan: 11. Then one row per machine over the time steps 0 to 10, with digits for the job running: M0 00011......, M1 2222001111., M2 .....122200. Digits are job numbers; each row is one machine.

Who it is for

The job shop from the terminal, drawn

Three jobs, three machines, each job a fixed order of operations. unifier keeps every machine to one operation at a time, minimises the end of the last one and proves that 11 is the shortest possible. The chart is drawn from the output above.

The job shop, solved: makespan 11The optimal schedule that examples/job_shop.rs prints, one bar per operation, grouped by machine. Machine M0 runs job 0 from 0 to 3 and job 1 from 3 to 5. M1 runs job 2 from 0 to 4, job 0 from 4 to 6 and job 1 from 6 to 10. M2 runs job 1 from 5 to 6, job 2 from 6 to 9 and job 0 from 9 to 11. No machine runs two operations at once, every job keeps its order of operations, and the last operation ends at 11.The job shop, solved: makespan 1101234567891011Time unitsMakespan 11: 11M0 · job 0 (Job 0): 0 to 3M0 · job 0M0 · job 1 (Job 1): 3 to 5M0 · job 1M1 · job 2 (Job 2): 0 to 4M1 · job 2M1 · job 0 (Job 0): 4 to 6M1 · job 0M1 · job 1 (Job 1): 6 to 10M1 · job 1M2 · job 1 (Job 1): 5 to 6M2 · job 1M2 · job 2 (Job 2): 6 to 9M2 · job 2M2 · job 0 (Job 0): 9 to 11M2 · job 0Makespan 11Job 0Job 1Job 2
The job shop, solved: makespan 11The optimal schedule that examples/job_shop.rs prints, one bar per operation, grouped by machine. Machine M0 runs job 0 from 0 to 3 and job 1 from 3 to 5. M1 runs job 2 from 0 to 4, job 0 from 4 to 6 and job 1 from 6 to 10. M2 runs job 1 from 5 to 6, job 2 from 6 to 9 and job 0 from 9 to 11. No machine runs two operations at once, every job keeps its order of operations, and the last operation ends at 11.The job shop, solved: makespan 1101234567891011Time unitsMakespan 11: 11M0 · job 0 (Job 0): 0 to 3M0 · job 0M0 · job 1 (Job 1): 3 to 5M0 · job 1M1 · job 2 (Job 2): 0 to 4M1 · job 2M1 · job 0 (Job 0): 4 to 6M1 · job 0M1 · job 1 (Job 1): 6 to 10M1 · job 1M2 · job 1 (Job 1): 5 to 6M2 · job 1M2 · job 2 (Job 2): 6 to 9M2 · job 2M2 · job 0 (Job 0): 9 to 11M2 · job 0Makespan 11Job 0Job 1Job 2
The job shop, solved: makespan 11The optimal schedule that examples/job_shop.rs prints, one bar per operation, grouped by machine. Machine M0 runs job 0 from 0 to 3 and job 1 from 3 to 5. M1 runs job 2 from 0 to 4, job 0 from 4 to 6 and job 1 from 6 to 10. M2 runs job 1 from 5 to 6, job 2 from 6 to 9 and job 0 from 9 to 11. No machine runs two operations at once, every job keeps its order of operations, and the last operation ends at 11.The job shop, solved:makespan 1101234567891011Time unitsMakespan 11: 11M0 · job 0 (Job 0): 0 to 3M0 · job 0M0 · job 1 (Job 1): 3 to 5M0 · job 1M1 · job 2 (Job 2): 0 to 4M1 · job 2M1 · job 0 (Job 0): 4 to 6M1 · job 0M1 · job 1 (Job 1): 6 to 10M1 · job 1M2 · job 1 (Job 1): 5 to 6M2 · job 1M2 · job 2 (Job 2): 6 to 9M2 · job 2M2 · job 0 (Job 0): 9 to 11M2 · job 0Makespan 11Job 0Job 1Job 2
The job shop, solved: makespan 11The optimal schedule that examples/job_shop.rs prints, one bar per operation, grouped by machine. Machine M0 runs job 0 from 0 to 3 and job 1 from 3 to 5. M1 runs job 2 from 0 to 4, job 0 from 4 to 6 and job 1 from 6 to 10. M2 runs job 1 from 5 to 6, job 2 from 6 to 9 and job 0 from 9 to 11. No machine runs two operations at once, every job keeps its order of operations, and the last operation ends at 11.The job shop, solved:makespan 1101234567891011Time unitsMakespan 11: 11M0 · job 0 (Job 0): 0 to 3M0 · job 0M0 · job 1 (Job 1): 3 to 5M0 · job 1M1 · job 2 (Job 2): 0 to 4M1 · job 2M1 · job 0 (Job 0): 4 to 6M1 · job 0M1 · job 1 (Job 1): 6 to 10M1 · job 1M2 · job 1 (Job 1): 5 to 6M2 · job 1M2 · job 2 (Job 2): 6 to 9M2 · job 2M2 · job 0 (Job 0): 9 to 11M2 · job 0Makespan 11Job 0Job 1Job 2
All examples with their sourceModelling guide →
interchangeable solver strategies
5
built-in constraints, three of them global
17
outcome states: Optimal, Feasible, Infeasible, Aborted
4
runtime dependency (pathwise)
1

What you get

Quickstart

From a model to a proven optimum. The quickstart in the documentation walks through the full program and its output.

  1. Add the crate with cargo add unifier.
  2. Declare variables, constraints and objectives with ModelBuilder.
  3. Validate with build(), then pass the graph to a solver.
Read the documentation
main.rsRust
let mut model = ModelBuilder::new();
let a = model.new_var("a", 1..=4);
let b = model.new_var("b", 1..=4);
model.add_all_different([a, b]);
model.add_minimize([a, b], 1);

let graph = model.build().expect("valid model");
let outcome = BranchAndBoundSolver::new().solve(&graph, &SolverOptions::default());
Read the quickstart

New in v0.6.0

Changelog →

Frequently asked questions

What kind of problems is unifier for?

Constraint Satisfaction and Optimization Problems: variables, domains and rules, plus an objective once something should be optimized rather than just satisfied. Typical instances are scheduling, timetabling and resource allocation, but also puzzles and assignments such as map colouring or eight queens.

How does unifier relate to pathwise?

It does not implement pathwise's Problem or OptimizationProblem traits or route search through its generic algorithms. unifier ships its own CSP/COP-specialized solver stack, and shares only two generic, CSP-independent primitives with pathwise: a cancellation token and a shared incumbent for anytime and parallel search coordination.

What happens when a solver runs out of time?

A SolveOutcome reports Aborted(reason) together with the best solution found so far, not nothing. Branch & Bound additionally reports a score bound, so you can see how far the result is from a proven optimum.

Is unifier ready for production use?

It is early (0.x) but published to crates.io, with the core model, constraint propagation, global constraints, hard/soft scoring and all five solver strategies implemented and tested. General unsat cores, serde-based serialization or a CLI, and independent verification on production-scale scheduling scenarios are not yet covered — evaluate accordingly before relying on it for production planning.