Repository files navigation

CLP(B), Constraint Logic Programming over Boolean variables, isavailable in Scryer Prolog and SWI-Prolog aslibrary(clpb).

This repository contains usage examples and tests of the library.

clpb.pdf is ashortened version of the librarydocumentation, intended as supplementary lecture material.

Project page:

https://www.metalevel.at/clpb/

Many of the examples useDCG notation todescribe lists of clauses. This lets you easily reason about theconstraints that are being posted, change the order in which they areposted, and in general more conveniently experiment with CLP(B).In some examples, it is faster to post a single big conjunctioninstead of several smaller ones.

I recommend you start with the following examples:

1. knights_and_knaves.pl: Solution ofseveral Boolean puzzles that appear in Raymond Smullyan'sWhat Isthe Name of this Book and Maurice Kraitchik'sMathematicalRecreations. These examples and otherlogic puzzlesare good starting points for learning more about CLP(B).

2. xor.pl: Verification of a digital circuit, expressingXOR with NAND gates:

   

   This example usesuniversally quantified variables to express theoutput as a function of the input variables in residual goals.

3. matchsticks.pl: A puzzle involvingmatchsticks. See below for more information.

4. cycle_n.pl: Uses Boolean constraints to expressindependent sets andmaximal independent sets (also calledkernels) of thecycle graph C_N.

   

   See below for more information about weighted solutions.

5. euler_172.pl: CLP(B) solution of Project EulerProblem 172: How many18-digit numbers n (without leading zeros) are theresuch that no digit occurs more than three times in n?

6. domino_tiling.pl: Domino tiling of anM×N chessboard. Using CLP(B), it is easy to seethat there are 12,988,816 ways to cover an8×8 chessboard with dominoes:

   

   Interestingly, theFibonacci numbersarise when we count the number of domino tilings of2×N chessboards. An example is shown in the rightfigure.

Other examples are useful as benchmarks:

• langford.pl: Count the number ofLangford pairings.
• n_queens.pl: CLP(B) formulation of theN-queens puzzle.
• pigeon.pl: A simple allocation task.
• schur.pl: A problem related toSchur's number asknown fromRamsey theory.

The directorybddcalc contains a very simple calculatorfor BDDs.

Inmatchsticks.pl, Boolean variables indicatewhether a matchstick is placed at a specific position. The task is toeliminate all subsquares from the initial configuration in such a waythat the maximum number of matchsticks is left in place:

We can use the CLP(B) predicateweighted_maximum/3 to show that weneed to remove at least 9 matchsticks to eliminate all subsquares.

The left figure shows a sample solution, leaving the maximum number ofmatchsticks (31) in place. If you keep more matchsticks in place,subsquares remain. For example, the right figure contains exactly7 subsquares, including the 4x4 outer square.

CLP(B) constraints can be used to quickly generate, test and countsolutions of such puzzles, among many other applications. For example,there are precisely 62,382,215,032 subsquare-free configurations thatuse exactly 18 matchsticks. This is the maximum number of suchconfigurations for any fixed number of matchsticks on this grid.

As another example, consider the following graph:

It is the so-calledcycle graph with100 nodes,C₁₀₀. Using CLP(B) constraints, itis easy to see that this graph has exactly 792,070,839,848,372,253,127independent sets, and exactly 1,630,580,875,002maximalindependent sets, which are also calledkernels. The gray nodes inthe next picture show one such kernel:

Suppose that we assign each noden_j the weightw_j =  (-1)^νj, whereνjdenotes the number of ones in the binary representationof j. In the above figure, nodes with negative weight aredrawn as squares, and nodes with positive weight are drawn as circles.

Only 5 nodes (1, 25, 41, 73 and 97) of this kernel with 38 nodes havenegative weight in this case, for a total weight of 28. In this case,the example shows a kernel withmaximum weight. It is easy tofind such kernels with the CLP(B) predicateweighted_maximum/3, andwe can also compute other interesting facts: For example, there areexactly 256 kernels of maximum weight in this case. There are exactly25,446,195,000 kernels with exactly 38 nodes. All kernels have between34 and 50 nodes. For any fixed number of nodes, the maximum number ofkernels (492,957,660,000) is attained with 41 nodes, and among thesekernels, the maximum total weight is 25.

By negating the coefficients ofweighted_maximum/3, we can also findkernels withminimum weight. For example:

The implementation oflibrary(clpb) is based on ordered and reducedBinary Decision Diagrams (BDDs). BDDs are an important datastructure for representing Boolean functions and have many virtuesthat often allow us to solve interesting tasks efficiently.

For example, the CLP(B) constraintsat(card([2],[X,Y,Z])) istranslated to the following BDD:

To inspect the BDD representation of Boolean constraints, set theProlog flagclpb_residuals to bdd. For example:

?- set_prolog_flag(clpb_residuals, bdd).true.?- sat(X+Y).node(2)- (v(X, 0)->true;node(1)),node(1)- (v(Y, 1)->true;false).

Usinglibrary(clpb) is a good way to learn more about BDDs. Thevariable order is determined by the order in which the variables arefirst encountered in constraints. You can enforce arbitrary variableorders by first posting a tautology such as+[1,V1,V2,...,Vn].

For example:

?-sat(+[1,Y,X]), sat(X+Y).node(2)- (v(Y, 0)->true;node(1)),node(1)- (v(X, 1)->true;false).

You can render CLP(B)'s residual goals as BDDs in SWISH using theBDD renderer.

There is a limited alternative version oflibrary(clpb), based onZero-suppressed Binary Decision Diagrams (ZDDs).

Please see thezdd directory for more information. Try theZDD-based version for tasks where the BDD-based version runs out ofmemory. You must usezdd_set_vars/1 before usingsat/1 though.

I am extremely grateful to:

Jan Wielemaker for providing theProlog system that made all this possible in the first place.

Ulrich Neumerkel, whointroduced me to constraint logic programming and CLP(B) inparticular. If you are teaching Prolog, I strongly recommend you checkout hisGUPU system.

Nysret Musliu, my thesisadvisor, whose interest in combinatorial tasks, constraintsatisfaction and SAT solving highly motivated me to work in thisarea.

Mats Carlsson, the designer andmain implementor of SICStus Prolog and its visionaryCLP(B) library.For any serious use of Prolog and constraints, make sure to check outhis elegant and fast system.

Donald Knuth for thesuperb treatment of BDDs and ZDDs in his books and programs.