ENHANCED: CLP(B): Stronger propagation, reducing choice points in labeling/1.
ENHANCED: CLP(B): Stronger propagation, reducing choice points in labeling/1.

We now apply the previous reasoning to *all* variables in the BDD.
This currently slows down labeling significantly when collecting all
solutions (there may be a way to improve this). However, it has the
significant advantage that it propagates more strongly in many
situations and leaves no redundant choice points after labeling/1.

Example:

   %?- sat(~X1+ (X2+X3)* ~X4), labeling([X1,X4]).
   %@ X1 = X4, X4 = 0,
   %@ sat(X2=:=X2),
   %@ sat(X3=:=X3) ;
   %@ X1 = 0,
   %@ X4 = 1,
   %@ sat(X2=:=X2),
   %@ sat(X3=:=X3) ;
   %@ X1 = 1,
   %@ X4 = 0,
   %@ sat(X2=:=X2),
   %@ sat(X2#X2*X3#X3),
   %@ sat(X3=:=X3).

Found with:

   :- use_module(library(clpb)).

   sat(_) --> [].
   sat(~_) --> [].
   sat(X*Y) --> [_], sat(X), sat(Y).
   sat(X+Y) --> [_], sat(X), sat(Y).
   sat(X#Y) --> [_], sat(X), sat(Y).

   vs_eqs(Vs, Eqs) :- phrase(vs_eqs(Vs), Eqs).

   vs_eqs([]) --> [].
   vs_eqs([V|Vs]) --> vs_eqs_(Vs, V), vs_eqs(Vs).

   vs_eqs_([], _) --> [].
   vs_eqs_([V|Vs], X) --> vs_eqs_(Vs, X), ( [(X=V)] ; [] ).

   list_sublist([]) --> [].
   list_sublist([L|Ls]) --> ([] | [L]), list_sublist(Ls).

   list_sublist(Ls0, Ls) :- phrase(list_sublist(Ls0), Ls).

   labeling_nondet(Vs) :-
           call_cleanup(labeling(Vs), Det = true),
           Det \== true.

   run(N) :-
           length(Ls, N),
           portray_clause(N),
           phrase(sat(Sat1), Ls),
           term_variables(Sat1, Vs),
           vs_eqs(Vs, Eqs),
           maplist(call, Eqs),
           sat(Sat1),
           term_variables(Sat1, Vs1),
           list_sublist(Vs1, Vs2),
           findall(Vs2, labeling_nondet(Vs2), Sols1),
           findall(Vs2, labeling(Vs2), Sols2),
           length(Sols1, L1),
           length(Sols2, L2),
           (   L1 =:= L2 -> throw(Sat1-Vs2)
           ;   true
           ),
           false.

   run :- run(_).

Notice the use of call_cleanup/2 to collect all solutions where a
choice point is still left. The cases we want to avoid with stronger
propagation are when the number of solutions where a choice point is
left is the *same* as the total number of solutions, because this
means that the choice point is unnecessary.

The stronger propagation also helps when no labeling at all is involved.

Example:

   %?- sat((X1*X2+ ~X3)* (~X2+ ~X1)).
   %@ X3 = 0,
   %@ sat(X1=:=X1),
   %@ sat(1#X1*X2),
   %@ sat(X2=:=X2).

koryonik/swipl-devel,mndrix/swipl-devel,mndrix/swipl-devel,edechter/swipl-devel,edechter/swipl-devel,mndrix/swipl-devel,jn7163/swipl-devel,koryonik/swipl-devel,koryonik/swipl-devel,mndrix/swipl-devel,mndrix/swipl-devel,koryonik/swipl-devel,edechter/swipl-devel,jn7163/swipl-devel,edechter/swipl-devel,jn7163/swipl-devel,edechter/swipl-devel,jn7163/swipl-devel,koryonik/swipl-devel,jn7163/swipl-devel