Finite Domain Package

This theory groups the predicates of the finite domain constraint solver and the SAT solver. The finite domain constraint solver is available as a module library(finite/clpfd). The SAT solver is available as a module library(finite/clpb). The modules implement instances of the CLP(X) scheme, where X is a domain [7].

For the finite domain solver the domain is the negative and positive integers, for the SAT solver the domain are the Boolean values {0,1}. For the finite domain solver there is also reification of constraints, which isn’t necessary for the SAT solver. Our algorithms are deterministic, for theoretical underpinnings and current trends see [8].

Kommentare