We develop
LazyCP, a lazy finite-domain constraint solver:
- supports many global constraints
- all-different,
- element, count,
- cardinality, bin_packing
- disjunctive, cumulative,
- circuit, path
- lazy PB explanations for propagations and conflicts
- user callbacks
- automated PB encodings
- encoding optimization
LazyCP is based on more general cutting planes reasoning which generally makes it exponentially faster than resolution-based solvers.
LazyPB is a fast lazy pseudo-Boolean (PB) solver that is the core solving engine of LazyCP:
- implements conflict-driven constraint learning (CDCL)
- fast data structures
- efficient backtracking
- cutting-plane-based conflict analysis
- variable selection heuristics
- presolving
- restart strategies
- constraint deletion strategies
- lazy constraint callbacks
