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

Boolean Constraint Solver

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.

Solver Interface

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.

Examples

Example 1

| ?- 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.

Example 2

| ?- 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.

Example 3

| ?- [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.

Example 4

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.