By default, CLP(B) residual goals appear in (approximately) algebraic
normal form (ANF). This projection is often computationally expensive.
We can set the Prolog flag clpb_residuals to the value 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:
?- set_prolog_flag(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, we
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).
