ADDED: CLP(B), Constraint Logic Programming over Boolean Variables

ADDED: CLP(B), Constraint Logic Programming over Boolean Variables

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!