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).

Status

Early (0.1.x), published to crates.io. 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
• 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
• 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.1"

License

MIT — see LICENSE.