A fast generic Constraint Solver.
Goals and technology:
- Has a modular structure, that facilitates seamless integration with other solvers.
The types of solvers that are compatible:
- A DPLL/CDCL SAT solver which has an interface to:
- A Multi-Valued SAT solver, with similar capabilities to the Boolean-SAT described above.
- A Constraint Solver based on AC-3
or Global AC-3 (GAC-3) which has an interface to:
- Run only the Constraint Propagation phase.
- Has an efficient query interface to find all literals that the last Constraint Propagation has inferred.
- Has an interface that allows the integration with external CDCL. This means either that the solver has CDCL by itself, like HaifaCSP, or has a way to trace-back the history of propagation.
- Maybe: a Local Search Solver - to be used for decision making.
- Employ CDCL over the whole problem, including generic constraint learning, similar to HaifaCSP](https://strichman.net.technion.ac.il/haifacsp/).
- Support a mix of different types of propagation and consistency, where Global AC-3 is the strongest and bounds-consistency is the weakest.
- Have an extendable variable-domain. Examples of domains:
- Boolean variables.
- Tiny integer-domains, sets of which will be implemented as bit-vectors.
- 32-bit integer-domains implemented as collections of intervals, such as interval_set.
- Bounds, either of integers (fixed or unlimited precision), or floating-point.
- Different solvers work with different types of domains. Some of the solvers will have a single domain type, such as SAT-solvers, which typically work only with Boolean domains. This use of single-domain types allows an efficient static-dispatch. This is more efficient than using virtual functions to get to the correct functions at run-time.
- Synching between different domain-types is performed by a special equality solver that can access all domain types.