Introduction
Dogelog Player is a Prolog system 100% written in Prolog itself. To enable SAT solvers we gave it a generational garbage collector and saw performance gain Java 42%, JavaScript 51% and Python 61%. We compare here with a few other Prolog systems.
OR Representation
A SAT solver is a computer program which aims to solve the Boolean satisfiability problem. We follow an approach where the given formula is first transformed into a normal form. If this normal form differs from zero 0, we know that the formula was satisfiable.
Normal forms such as conjunctive normal form or disjunctive normal form are part of mainstream consciousness. On the other hand a popular normal form for circuit design is BDD. Lets write A[X/V] for substituting the variable X by the value V. It has this co-factor representation:
A = X * A[X/1] + (-X) * A[X/0]
In the above (*)/2 denotes conjunction, (+)/2 denotes disjunction and (-)/2 denotes negation. In practice one might find reduce ordered BDDs, i.e. ROBDDs. They are ordered because variables X1,..,Xn are chosen in a fixed order in the co-factor representation.
% tree_make(+Atom, +Tree, +Tree, -Tree)
tree_make(_, A, A, A) :- !.
tree_make(X, A, B, (X->A;B)).
Further ROBDDs are reduced, a variable is only used in a subtree if necessary. The above Prolog code shows how such a reduction can be done on the fly. If A and B are the cofactors, we write a BDD node as (X->A;B), and the intention is that a node (X->A;A) can be reduced to A.
XOR Representation
While BDDs are essentially Boolean expansions, we find also FBDDs, functional BDDs, which are based on Read-Muller expansions. This expansion represents a formula A with the help of the exclusive-or operator from its co-factors. The expansion with a positive variable X reads as follows:
A = A[X/0] # X * A[X/1]
In the above (#)/2 denotes exclusive-or. Whereas BDDs pay tribute to Boolean lattices, FBDDs can be seen as founded on Boolean rings. Analguously to ROBDDs, there are ROFBDDs adding reduction and ordering to FBDDs. The reduction rule for FBDDs reads as follows:
% tree2_make(+Atom, +Tree, +Tree, -Tree)
tree2_make(_, A, 0, A) :- !.
tree2_make(X, A, B, (X*->A;B)).
To highlight the similar tree structure of BDDs and FBDDs we used the soft-cut syntax (X*->A;B) to represent Read-Muller expansion nodes. But tree structures have also true 1 and false 0 as their leaves. The reduction for FBDDs has the intention that (X*->A;0) can be replaced by A.
Perpetual Processes
In the average Read-Muller expansion takes a more space than Boolean expansion. But there are some pratical examples, such as a half-adder, that take less space in Read-Muller expansion than in Boolean expansion. Adding two values A and B, gives sum S = A#B and carry C = A*B:
0 0 1 1
0 1 0 1
+ --- + --- + --- + ---
0 0 0 1 0 1 1 0
We wrote OR representation library tree.p and XOR representation library tree2.p in ca. 4000 bytes each. These librariers understand the boolean formula syntax from the SWI-Prolog CLP(B) library. The results for the half adder problem are these trees:
?- tree_eval(a=\=b, S), tree_eval(a*b, C).
S = (a->(b->0;1);b->1;0),
C = (a->(b->1;0);0).
?- tree2_eval(a=\=b, S), tree2_eval(a*b, C).
S = (a*->(b*->0;1);1),
C = (a*->0;b*->0;1).
There are more drastic examples where OR and XOR representation differ. But there is no winner, sometimes the OR representation explodes and the XOR representation doesn't and vice versa. We put according test cases into an according test suite.
?- between(1,100,_), suite_quiet, fail; true.
We were then interested whether Prolog systems can stand the formula explosion running the above query. A Prolog system might produce a right result but not correctly reclaim its memory. We used ulimit -m | -v to see whether the Prolog system creates a segmentation fault:
This test was passed by our Dogelog Player 1.1.4 for Java, using our generational GC. The test was passed by Ciao Prolog 1.22.0, SWI-Prolog 9.1.8 and Trealla Prolog 2.30.50. It wasn't passed by Scryer Prolog 0.9.3 which was gradually eating more and more memory.
Solver Performance
The test suite contains SAT and #SAT test cases. The later is the problem of counting the number of interpretations that satisfy a given Boolean formula. Unlike OR representation, XOR representation dimishes its benefit, since we didn't find a simple #SAT approach.
|(X -> A; B)| = |A| + |B|
|(X *-> A; B)| = |A| + |A#B|
The above shows the counting formulas we used. To count a Read-Muller expansion we needed to compute an exclusive-or during the counting. So performance gains during normalization are often ruined during counting. The test suite contains 4 satisfiablity and 4 counting test cases:
We included Scryer Prolog in our testing, although memory leaking could be a form of cheating, since it could indicate that the Prolog system doesn't make some effort to reclaim memory. Ciao Prolog is the front runner and performs almost 10-times faster than Trealla Prolog.
SWI-Prolog could recently improve its speed, and it only takes the double of time as of Ciao Prolog. Interestingly Dogelog Player for Java is not last, it can for example beat Trealla Prolog. This archivement wouldn't be possible without our new generative GC and its performance gain.
Conclusions
There are some pratical examples, such as a half-adder, that take less space in Read-Muller expansion than in Boolean expansion. The test suite contains 4 satisfiablity and 4 counting test cases. Interestingly Dogelog Player for Java is not last thanks to the performance gain.