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`-
True if
`P`is false. `P`*`Q`-
True if
`P`and`Q`are both true. `P`+`Q`-
True if at least one of
`P`and`Q`is true. `P`#`Q`-
True if exactly one of
`P`and`Q`is true. `X`^`P`-
True if there exists an
`X`such that`P`is true. Same as

.`P`[`X`/0] +`P`[`X`/1] `P`=:=`Q`-
Same as
`~`

.`P`#`Q` `P`=\=`Q`-
Same as

.`P`#`Q` `P`=<`Q`-
Same as
`~`

.`P`+`Q` `P`>=`Q`-
Same as

.`P`+ ~`Q` `P`<`Q`-
Same as
`~`

.`P`*`Q` `P`>`Q`-
Same as

.`P`* ~`Q` `card(`

`Is`,`Es`)-
True if the number of true expressions in
`Es`is a member of the set denoted by`Is`.

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.

The following predicates are defined:

`sat(`

`+Expression`)-
`Expression`is a Boolean expression. This checks the consistency of the expression wrt. the accumulated constraints, and, if the check succeeds,*tells*the constraint that the expression be true. If a variable`X`, occurring in the expression, is subsequently unified with some term`T`, this is treated as a shorthand for the constraint?- sat(X=:=T).

`taut(`

`+Expression`,`?Truth`)-
`Expression`is a Boolean expression. This*asks*whether the expression is now entailed by the accumulated constraints (`Truth`=1), or whether its negation is entailed by the accumulated constraints (`Truth`=0). Otherwise, it fails. `labeling(`

`+Variables`)-
`Variables`is a list of variables. The variables are instantiated to a list of 0s and 1s, in a way that satisfies any accumulated constraints. Enumerates all solutions by backtracking, but creates choicepoints only if necessary.

| ?- sat(X + Y). sat(X=\=_A*Y#Y) ?

illustrates three facts. First, any accumulated constraints affecting the
top-level variables are displayed as floundered goals, since the query
is not true for all `X`

and `Y`

. Secondly, accumulated
constraints are displayed as `sat(`

or `V`=:=`Expr`)`sat(`

where `V`=\=`Expr`)`V` is a variable and
`Expr` is a "polynomial", i.e. an exclusive or of conjunctions of
variables and constants. Thirdly, `_A`

had to be introduced as an
artificial variable, since `Y`

cannot be expressed as a function of
`X`

. That is, `X + Y`

is true iff there exists an `_A`

such that `X=\=_A*Y#Y`

. Let's check it!

| ?- taut(_A ^ (X=\=_A*Y#Y) =:= X + Y, T). T = 1 ?

verifies the above answer. Notice that the formula in this query is a tautology, and so it is entailed by an empty set of constraints.

| ?- taut(A =< C, T). no | ?- sat(A =< B), sat(B =< C), taut(A =< C, T). T = 1, sat(A=:=_A*_B*C), sat(B=:=_B*C) ? | ?- taut(a, T). T = 0 ? yes | ?- taut(~a, T). T = 0 ?

illustrates the entailment predicate. In the first query, the
expression "A implies C" is neither known to be true nor false, so the
query fails. In the second query, the system is told that "A implies
B" and "B implies C", so "A implies C" is entailed. The
expressions in the third and fourth queries are to be read "for each a,
a is true" and "for each a, a is false", respectively, and so ```
T
= 0
```

in both cases since both are unsatisfiable. This illustrates the
fact that the implicit universal quantifiers introduced by symbolic
constants are placed in front of the entire expression.

| ?- [user]. | adder(X, Y, Sum, Cin, Cout) :- sat(Sum =:= card([1,3],[X,Y,Cin])), sat(Cout =:= card([2-3],[X,Y,Cin])). | {user consulted, 40 msec 576 bytes} yes | ?- adder(x, y, Sum, cin, Cout). sat(Sum=:=cin#x#y), sat(Cout=:=x*cin#x*y#y*cin) ? yes | ?- adder(x, y, Sum, 0, Cout). sat(Sum=:=x#y), sat(Cout=:=x*y) ? yes | ?- adder(X, Y, 0, Cin, 1), labeling([X,Y,Cin]). Cin = 0, X = 1, Y = 1 ? ; Cin = 1, X = 0, Y = 1 ? ; Cin = 1, X = 1, Y = 0 ? ;

illustrates the use of cardinality constraints and models a one-bit adder circuit. The first query illustrates how representing the input signals by symbolic constants forces the output signals to be displayed as functions of the inputs and not vice versa. The second query computes the simplified functions obtained by setting carry-in to 0. The third query asks for particular input values satisfying sum and carry-out being 0 and 1, respectively.

The predicate `fault/3`

below describes a 1-bit adder consisting of
five gates, with at most one faulty gate. If one of the variables
`Fi`

is equal to 1, the corresponding gate is faulty, and its
output signal is undefined (i.e., the constraint representing the gate
is relaxed).

Assuming that we have found some incorrect output from a circuit, we
are interesting in finding the faulty gate. Two instances of incorrect
output are listed in `fault_ex/2`

:

fault([F1,F2,F3,F4,F5], [X,Y,Cin], [Sum,Cout]) :- sat( card([0-1],[F1,F2,F3,F4,F5]) * (F1 + (U1 =:= X * Cin)) * (F2 + (U2 =:= Y * U3)) * (F3 + (Cout =:= U1 + U2)) * (F4 + (U3 =:= X # Cin)) * (F5 + (Sum =:= Y # U3)) ). fault_ex(1, Faults) :- fault(Faults, [1,1,0], [1,0]). fault_ex(2, Faults) :- fault(Faults, [1,0,1], [0,0]).

To find the faulty gates, we run the query

| ?- fault_ex(I,L), labeling(L). I = 1, L = [0,0,0,1,0] ? ; I = 2, L = [1,0,0,0,0] ? ; I = 2, L = [0,0,1,0,0] ? ; no

Thus for input data `[1,1,0]`

, gate 4 must be faulty.
For input data `[1,0,1]`

, either gate 1 or gate 3 must be faulty.

To get a symbolic representation of the outputs interms of the input, we run the query

| ?- fault([0,0,0,0,0], [x,y,cin], [Sum,Cout]). sat(Cout=:=x*cin#x*y#y*cin), sat(Sum=:=cin#x#y)

which shows that the sum and carry out signals indeed compute the intended functions if no gate is faulty.

Go to the first, previous, next, last section, table of contents.