unifier

Constraint satisfaction / optimization (CSP/COP) modeling and solver framework for Rust, integrating with pathwise's generic search and optimization traits (see "Solver stack" below for how far that integration currently goes).

Website and documentation: casoon.github.io/unifier

Status

Early (0.3.x), published to crates.io; see CHANGELOG.md. The core model, constraint propagation, global constraints, hard/soft scoring with weighted objectives, fallible model validation (ConstraintGraph::validate / ModelBuilder::build), and five solver strategies (Backtracking, Branch & Bound with optimistic-bound pruning, Local Search, LNS, Parallel Portfolio) are implemented and tested. SolveOutcome reports status (Optimal / Feasible / Infeasible / Aborted(reason)), the best solution found, search statistics, and — for Branch & Bound — a score bound.

ValidatedGraph::check_incremental additionally evaluates only the constraints adjacent to changed assignment variables, without starting a solver search. Violations carry structured explanations; specialized explanations are implemented for NoOverlap, Cumulative, and Precedence.

Not yet covered: general unsat cores, a serde-based model/solution serialization or CLI, and independent verification of production-scale scheduling scenarios — evaluate accordingly before relying on this for production planning.

Problem class

Constraint Satisfaction Problems (CSP) — and, once an objective is optimized rather than just satisfied, Constraint Optimization Problems (COP): variables, domains, constraints, and (for COP) an objective. Typical instances: scheduling, timetabling, resource allocation.

These problems are generally NP-hard — there is no single "best algorithm" the way there is for sorting. unifier's solver strategies are therefore interchangeable rather than fixed, and the design targets an anytime solver: a valid solution fast, then iterative improvement, cancellable at any point.

Core model

• Variable / Domain — Variable (integer-valued, identified by VariableId) with a Domain: Range { min, max } for contiguous bounds, or Explicit(BTreeSet<i64>) once a value is punched out of the middle of a range
• Constraint — Equal, NotEqual, LessThanOrEqual, AllDifferent, NoOverlap, Cumulative, Precedence, AllowedValues/ForbiddenValues, ExactlyOne/AtMost/AtLeast, PeriodicValues, MinimumDistance, MaximumBucketLoad, BucketBlockPattern
• Objective — WeightedSum soft-score terms (hard constraints are never violated in a feasible solution; soft terms are a weighted preference to maximize), aggregated into a HardSoftScore with lexicographic strong / medium / weak soft levels
• Interval / Resource / Activity / Group — scheduling-oriented data types (start/duration/end, capacity, resource demands, grouped activities sharing one interval). ModelBuilder::compile_scheduling_model compiles them into the constraint graph automatically (Cumulative for capacity > 1 resources, NoOverlap for unary ones, LessThanOrEqual pairs for group containment), plus calendar exclusions, optional (presence-gated) activities, resource alternatives, and a tardiness objective helper

The problem itself is modeled as a constraint graph (a hypergraph of variables, constraints, and objectives), not a tree — the tree only emerges as part of a solver's search process. ConstraintGraph::validate / ModelBuilder::build reject structurally invalid models (unknown variable references, empty domains, duplicate IDs, self-contradictory constraint parameters) before a solver ever sees them.

Solver stack

pathwise provides the generic Problem/OptimizationProblem traits and interchangeable search/optimization strategies (A*, branch and bound, local search, simulated annealing, ...). unifier does not implement those traits or route search through pathwise's generic algorithms. It ships its own CSP/COP-specialized solver stack: constraint propagation (full generalized arc consistency for AllDifferent via Régin's matching + SCC algorithm; bounds- /singleton-consistency plus energetic-reasoning overload detection and, for NoOverlap, edge-finding bound-tightening for the scheduling constraints; AC-3 otherwise), dom/wdeg and MRV/fail-first variable ordering, reversible (checkpoint/undo) domains instead of cloning per search node, and Branch & Bound with its own optimistic-bound pruning. What unifier does share with pathwise: two generic, CSP-independent portfolio-coordination primitives — a cancellation token and a shared incumbent for anytime/parallel search coordination (pathwise::core::cancellation, pathwise::core::incumbent) — used by unifier's solvers instead of duplicating that logic locally.

The overall architecture is four layers: DSL (problem-building surface API), constraint model (variable/domain/constraint graph), solver engine (propagation, backtracking, branch & bound, local search, LNS), and runtime (incremental scoring, cancellation).

Installation

[dependencies]
unifier = "0.3"

License

MIT — see LICENSE.