# 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].

- Integer Values: The
finite domain solver allows denoting integer value expressions.
These expressions can contain variables. More...

- Integer Sets: The
finite domain solver allows denoting integer set expressions.
These expressions cannot contain variables. More...

- Integer Comparison: As
a convenience the finite domain solver provides a couple of
comparisons between integers. More...

**Constraint Reification: **As a further convenience we
also provide reification of finite domain constraints. More...

**Domain Search: **Finally we provide a couple of solving
techniques for finite domain constraints and their reification.
More...

**Boolean Values: **The SAT solver allows denoting Boolean
value expressions. These expressions can contain variables. More...

**Boolean Satisfaction: **Finally we provide a couple of
solving techniques for SAT solver constraints. More...

## Kommentare