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.

• CLPB Interface:
• CLPB Examples: