Go to the previous, next section.
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[X/0] + P[X/1].
~P # Q.
P # Q.
~P + Q.
P + ~Q.
~P * Q.
P * ~Q.
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:
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).
| ?- 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(V=:=Expr)
or sat(V=\=Expr) where 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 previous, next section.