clarify comment
introduce and use low_high_hentry/3

Also, I have found a faster test case for BDD merging:

        :- use_module(clpb).

        sat(X, Y, X=:=Y).
        sat(X, Y, X#Y).
        sat(X, Y, X+Y).
        sat(X, Y, X*Y).

        vs_formula([V|Vs], F) :- vs_formula_(Vs, V, F).

        vs_formula_([], F, F).
        vs_formula_([V|Vs], F0, F) :-
                sat(V, F0, Sat),
                vs_formula_(Vs, Sat, F).

        run :-
                sat(A, B, Sat1),
                sat(C, D, Sat2),
                sat(E, F, Sat3),
                sat(Sat1),
                sat(Sat2),
                sat(Sat3),
                Vs0 = [A,B,C,D,E,F],
                permutation(Vs0, Vs),
                vs_formula(Vs, Formula),
                sat(Formula),
                false.

This finds the previous mistake in bdd_and/3 faster.
Updated ssl
better naming, update output
Updated pengines
Updated pengines
improve sat_count/2 when the second argument is instantiated

Example:

   ?- sat_count(X, 2).
   false.
Updated pengines
Declare format_calls/3 public
Updated pengines
SECURITY: sandbox handling of format/2.
apply existential quantification sooner when building counter networks
further simplification of counter_network/3 and related predicates

I am also considering the following patch (relative to the previous revision):

   diff --git a/library/clp/clpb.pl b/library/clp/clpb.pl
   index 79c2faf..2c20e91 100644
   --- a/library/clp/clpb.pl
   +++ b/library/clp/clpb.pl
   @@ -463,32 +463,29 @@ existential(V, BDD, Node) :-
    counter_network(Cs, Fs, Node) :-
            same_length([_|Fs], Indicators),
            fill_indicators(Indicators, 0, Cs),
   -        same_length(Fs, Vars0),
   -        % enumerate variables in reverse order so that they appear
   -        % in the correct order in the resulting BDD
   -        maplist(enumerate_variable, Vars0),
   -        reverse(Vars0, Vars),
   -        counter_network(Fs, Indicators, Vars, Node0),
   -        maplist(var_index_root, Vars, _, Roots),
   -        maplist(=(Root), Roots),
   -        root_put_formula_bdd(Root, card(Cs,Fs), Node),
   -        eq_and(Vars, Fs, Node0, Node),
   -        % remove attributes to avoid residual goals for these variables,
   -        % which are only used temporarily to build the counter network.
   -        maplist(del_attrs, Vars).
   -
   -eq_and([], [], Node, Node).
   -eq_and([X|Xs], [Y|Ys], Node0, Node) :-
   -        sat_rewrite(v(X) =:= Y, Sat),
   -        sat_bdd(Sat, B),
   -        apply(*, B, Node0, Node1),
   -        existential(X, Node1, Node2),
   -        eq_and(Xs, Ys, Node2, Node).
   -
   -counter_network([], [Node], [], Node).
   -counter_network([_|Fs], [I|Is0], [Var|Vars], Node) :-
   +        maplist(formula_var_bdd_existential, Fs, Vars0, BDDs, Exs),
   +        variables_in_index_order(Vars0, Vars1),
   +        % The counter network is built bottom-up, so variables with
   +        % highest index must be processed first.
   +        reverse(Vars1, Vars),
   +        counter_network_(Vars, Indicators, Node0),
   +        writeln(BDDs),
   +        foldl(bdd_and, BDDs, Node0, Node1),
   +        foldl(remove_existential, Exs, Node1, Node).
   +
   +% Introduce fresh variables for expressions that are not variables.
   +% These variables are later existentially quantified to remove them.
   +
   +formula_var_bdd_existential(v(Var), Var, 1, none) :- !.
   +formula_var_bdd_existential(F, Var, BDD, v(Var)) :-
   +        enumerate_variable(Var),
   +        sat_rewrite(v(Var) =:= F, Sat),
   +        sat_bdd(Sat, BDD).
   +
   +counter_network_([], [Node], Node).
   +counter_network_([Var|Vars], [I|Is0], Node) :-
            indicators_pairing(Is0, I, Var, Is),
   -        counter_network(Fs, Is, Vars, Node).
   +        counter_network_(Vars, Is, Node).

    indicators_pairing([], _, _, []).
    indicators_pairing([I|Is], Prev, Var, [Node|Nodes]) :-
   @@ -504,6 +501,13 @@ fill_indicators([I|Is], Index0, Cs) :-
            Index1 is Index0 + 1,
            fill_indicators(Is, Index1, Cs).

   +remove_existential(none, Node, Node).
   +remove_existential(v(Var), Node0, Node) :-
   +        existential(Var, Node0, Node),
   +        % remove attributes to avoid residual goals for these variables,
   +        % which are only used temporarily to build the counter network.
   +        del_attrs(Var).
   +
    /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
       Compute F(NA, NB).

   @@ -754,10 +758,13 @@ node_ite(Node, Node-ite(Var,High,Low)) :-

    labeling(Vs0) :-
            must_be(list, Vs0),
   +        variables_in_index_order(Vs0, Vs),
   +        maplist(indomain, Vs).
   +
   +variables_in_index_order(Vs0, Vs) :-
            maplist(var_with_index, Vs0, IVs0),
            keysort(IVs0, IVs),
   -        pairs_values(IVs, Vs),
   -        maplist(indomain, Vs).
   +        pairs_values(IVs, Vs).

    var_with_index(V, I-V) :-
            (   var_index_root(V, I, _) -> true

This prevents auxiliary variables when existing variables can be used.
It makes the whole predicate a bit harder to understand and has so far
shown only negligible benefits, even where card/2 constraints dominate,
such as Project Euler Problem 172.
ENHANCED: library(sandbox): do not examine pure Prolog facts.
FIXED: Crash on e.g. format('~*f',[-5, 100 rdiv 3]).  Mike Elston.
FIXED: expand_goal/7 position information in clause that process the module was incorrect
Updated odbc
introduce and use variables_in_index_order/2
use existing variables in card/2 constraint, if possible

Example, previously:

   %?- sat(card([2,3],[A,B,C,D,E])).
   %@ sat(A=:=A),
   %@ node(197)- (A->node(196);node(194)),
   %@ node(194)- (B->node(193);node(191)),
   %@ node(191)- (C->node(190);node(182)),
   %@ node(182)- (D->node(159);false),
   %@ node(159)- (E->true;false),
   %@ node(190)- (D->true;node(159)),
   %@ node(193)- (C->node(192);node(190)),
   %@ node(192)- (D->node(173);true),
   %@ node(173)- (E->false;true),
   %@ node(196)- (B->node(195);node(193)),
   %@ node(195)- (C->node(178);node(192)),
   %@ node(178)- (D->false;node(173)),
   %@ sat(B=:=B),
   %@ sat(C=:=C),
   %@ sat(D=:=D),
   %@ sat(E=:=E).

Now:

   %?- sat(card([2,3],[A,B,C,D,E])).
   %@ sat(A=:=A),
   %@ node(11)- (A->node(10);node(9)),
   %@ node(9)- (B->node(7);node(6)),
   %@ node(6)- (C->node(3);node(2)),
   %@ node(2)- (D->node(0);false),
   %@ node(0)- (E->true;false),
   %@ node(3)- (D->true;node(0)),
   %@ node(7)- (C->node(4);node(3)),
   %@ node(4)- (D->node(1);true),
   %@ node(1)- (E->false;true),
   %@ node(10)- (B->node(8);node(7)),
   %@ node(8)- (C->node(5);node(4)),
   %@ node(5)- (D->false;node(1)),
   %@ sat(B=:=B),
   %@ sat(C=:=C),
   %@ sat(D=:=D),
   %@ sat(E=:=E).
CLP(B): Add experimental support for +(List) and *(List) syntax,
        denoting multi-argument disjunctions and conjunctions.
        Please give feedback about this syntax.
        Suggested by Gernot Salzer.

    Example:

       ?- sat(*([A,B,C])).
       A = B, B = C, C = 1.