Zero-suppressed Binary Decision Diagrams (ZDDs) can save a lot of memory when most Boolean variables are equal to 0 in solutions. This is the case in many covering tasks.
clpb.pl is a ZDD-based variant of library(clpb). It
is mostly a drop-in-replacement for the library that ships with
Scryer Prolog, with the following important difference: Before using
sat/1, you must call zdd_set_vars/1 with a list of all Boolean
variables that occur in your model.
This variant of the library can be used to more space-efficiently compute that there are exactly 92,109,458,286,284,989,468,604 ways to cover an 8×8 chessboard with monominoes, dominoes and trominoes. See polyomino_tiling.pl for more information.
In addition, as with library(clpb), solutions can also be picked in
such a way that each solution is equally likely.
Sample solution:
Exercises:
-
A chessboard tiling is faultfree if every straight line that passes through the interior of the board also passes through the interior of some domino. Add suitable constraints to describe solutions that are faultfree.
-
How many of the above solutions satisfy the additional property that no two congruent pieces are adjacent?
-
And of those, how many are there where congruent pieces touch at their corners?
Project Euler Problem 161 asks for the number of Triomino tilings of a 9×12 grid.
euler_161.pl shows how this can be solved with the ZDD-based variant of CLP(B) constraints. Using an Intel Core i7 CPU (2.67 GHz), you know after a few days of computation time: There are exactly 20,574,308,184,277,971 ways to do it.
One of these solutions, picked at random:
There are currently some limitations:
- unification of CLP(B) variables is not yet implemented in this variant
labeling/1does not work yet.
In addition, card/2 does not yet support integer ranges.
Please see the source file for more information about these issues.