The clp(B) system provided by this library module is an instance of the general Constraint Logic Programming scheme introduced in [Jaffar & Michaylov 87]. It is a solver for constraints over the Boolean domain, i.e. the values 0 and 1. This domain is particularly useful for modeling digital circuits, and the constraint solver can be used for verification, design, optimization etc. of such circuits.
To load the solver, enter the query:
| ?- use_module(library(clpb)).
The solver contains predicates for checking the consistency and entailment of a constraint wrt. previous constraints, and for computing particular solutions to the set of previous constraints.
The underlying representation of Boolean functions is based on Boolean Decision Diagrams [Bryant 86]. This representation is very efficient, and allows many combinatorial problems to be solved with good performance.
Boolean expressions are composed from the following operands: the
constants 0 and 1 (FALSE
and TRUE
), logical
variables, and symbolic constants, and from the following
connectives. P and Q are Boolean expressions, X is a
logical variable, Is is a list of integers or integer
ranges, and Es is a list of Boolean expressions:
~
P
P *
Q
P +
Q
P #
Q
X ^
P
P[
X/0] +
P[
X/1]
.
P =:=
Q
~
P #
Q
.
P =\=
Q
P #
Q
.
P =<
Q
~
P +
Q
.
P >=
Q
P + ~
Q
.
P <
Q
~
P *
Q
.
P >
Q
P * ~
Q
.
card(
Is,
Es)
Symbolic constants (Prolog atoms) denote parametric values and can be viewed as all-quantified variables whose quantifiers are placed outside the entire expression. They are useful for forcing certain variables of an equation to be treated as input parameters.