library(clpb) provides CLP(B), Constraint Logic Programming over
Boolean variables. It is a SAT solver that seamlessly integrates into
Prolog in the sense that logic variables are used to state constraints
and report solutions. This library can be used to model and solve many
combinatorial problems such as verification, allocation and covering
tasks.
CLP(B) is an instance of the general CLP(X) scheme, extending logic
programming with reasoning over specialised domains.
The implementation is based on reduced and ordered Binary Decision
Diagrams (BDDs).
Usage examples of this library are available in a public git
repository:
https://github.com/triska/clpb
For more information, benchmarks and publications visit:
https://www.metalevel.at/clpb/
The interface of this library is consciously kept compatible with the
CLP(B) solver of SICStus Prolog, which served as the main inspiration
of this library. Many thanks to Mats Carlsson for his elegant example!
It is my hope that library(clpb) will allow a port of cTI, and —
eventually — of Ulrich Neumerkel's GUPU to Scryer Prolog.
Boolean expressions
===================
A Boolean expression is one of:
0 false
1 true
variable unknown truth value
atom universally quantified variable
~ Expr logical NOT
Expr + Expr logical OR
Expr * Expr logical AND
Expr # Expr exclusive OR
Var ^ Expr existential quantification
Expr =:= Expr equality
Expr =\= Expr disequality (same as #)
Expr =< Expr less or equal (implication)
Expr >= Expr greater or equal
Expr < Expr less than
Expr > Expr greater than
card(Is,Exprs) see below
+(Exprs) see below
*(Exprs) see below
where Expr again denotes a Boolean expression.
The Boolean expression card(Is,Exprs) is true iff the number of true
expressions in the list Exprs is a member of the list Is of
integers and integer ranges of the form From-To.
+(Exprs) and *(Exprs) denote, respectively, the disjunction and
conjunction of all elements in the list Exprs of Boolean
expressions.
Atoms denote parametric values that are universally quantified. All
universal quantifiers appear implicitly in front of the entire
expression. In residual goals, universally quantified variables always
appear on the right-hand side of equations. Therefore, they can be
used to express functional dependencies on input variables.
Interface predicates
====================
The most frequently used CLP(B) predicates are:
* sat(+Expr)
True iff the Boolean expression Expr is satisfiable.
* taut(+Expr, -T)
If Expr is a tautology with respect to the posted constraints, succeeds
with T = 1. If Expr cannot be satisfied, succeeds with T = 0.
Otherwise, it fails.
* labeling(+Vs)
Assigns truth values to the variables Vs such that all constraints
are satisfied.
The unification of a CLP(B) variable X with a term T is equivalent
to posting the constraint sat(X=:=T).
Examples
========
Here is an example session with a few queries and their answers:
?- use_module(library(clpb)).
true.
?- sat(X*Y).
X = Y, Y = 1.
?- sat(X * ~X).
false.
?- taut(X * ~X, T).
T = 0,
sat(X=:=X).
?- sat(X^Y^(X+Y)).
sat(X=:=X),
sat(Y=:=Y).
?- sat(X*Y + X*Z), labeling([X,Y,Z]).
X = Z, Z = 1, Y = 0 ;
X = Y, Y = 1, Z = 0 ;
X = Y, Y = Z, Z = 1.
?- sat(X =< Y), sat(Y =< Z), taut(X =< Z, T).
T = 1,
sat(X=:=X*Y),
sat(Y=:=Y*Z).
?- sat(1#X#a#b).
sat(X=:=a#b).
The pending residual goals constrain remaining variables to Boolean
expressions and are declaratively equivalent to the original query.
The last example illustrates that when applicable, remaining variables
are expressed as functions of universally quantified variables.
Obtaining BDDs
==============
By default, CLP(B) residual goals appear in (approximately) algebraic
normal form (ANF). This projection is often computationally expensive.
Assert the fact clpb:clpb_residuals(bdd) to see the BDD representation
of all constraints. This results in faster projection to residual
goals, and is also useful for learning more about BDDs.
For example:
?- asserta(clpb:clpb_residuals(bdd)).
true.
?- sat(X#Y).
node(3)- (v(X, 0)->node(2);node(1)),
node(1)- (v(Y, 1)->true;false),
node(2)- (v(Y, 1)->false;true).
Note that this representation cannot be pasted back on the toplevel,
and its details are subject to change. Use copy_term/3 to obtain
such answers as Prolog terms.
The variable order of the BDD is determined by the order in which the
variables first appear in constraints. To obtain different orders,
you can for example use:
?- sat(+[1,Y,X]), sat(X#Y).
node(3)- (v(Y, 0)->node(2);node(1)),
node(1)- (v(X, 1)->true;false),
node(2)- (v(X, 1)->false;true).
Monotonic CLP(B)
================
In the default execution mode, CLP(B) constraints are not monotonic.
This means that adding constraints can yield new solutions. For
example:
?- sat(X=:=1), X = 1+0.
false.
?- X = 1+0, sat(X=:=1), X = 1+0.
X = 1+0.
This behaviour is highly problematic from a logical point of view, and
it may render declarative debugging techniques inapplicable (see
https://www.metalevel.at/prolog/debugging for more information).
Assert the fact clpb:monotonic to make CLP(B) monotonic. If this
mode is enabled, then you must wrap CLP(B) variables with the functor
v/1. For example:
?- asserta(clpb:monotonic).
true.
?- sat(v(X)=:=1#1).
X = 0.
Enjoy!
