Code share: CLP(FD) to CLP(B) translator

General
1

@kuniaki.mukai wrote:

Here is a little program that translates CLP(FD) to CLP(B):

finsat.p.log (7,9 KB)

One can determine primes with it:

:- numlen(10). /* number of bits  */
   
primes(X) :-
   X #=< 31,
   #\ Y #^ Z #^ (Y #=< 31 #/\ Z #=< 31 #/\ X #= Y*Z #/\ Y #\= 1 #/\ Z #\= 1),
   term_variables(X, V),
   labeling(V).

Now running the primes example gives:

/* SWI-Prolog 9.1.21 */
?- primes(X), asnat(X,N), write(N), write(' '), fail; true.
1 2 3 5 7 11 13 17 19 23 29 31 
true.
2

Although still I am not familiar with relation between boolean constraint (clp(B)) and finite domain one (clp(FD)), I observed again a similarity of my sat based on DNF to FD as query below. I thinks similarity comes from that a truth-assignment could be viewed as a characteristic function on a subset of the given finite domain in an evident way.

Anyway I have nothing to add to what I understand in naive way about relation between clp(B) and clp(FD). I should delete the quoted comment.

% ?- sat(a+b), sat(b+c), psa.
%@  zid = 8
%@ 	[b]
%@ 	[a,c]
%@ 	[a,b]
%@ -------------------
%@ true.
% ?- sat(a+b), sat(b+c), sat(-(a=b)), psa.
%@  zid = 26
%@ 	[-a,b]
%@ 	[a,-b,c]
%@ -------------------
%@ true.
4

For curiosity by your comment, I ran the query below, which
seems to mean that the DNF as a BDD for a=b+c in a sense a boolean circuit for the formula, though it should be redundant one. It was interesting for me, but it should be too
elementary observation for BDD/ZDD.

% ?- sat(a=b+c), print_root.
%@ 16=t(a,7,11)
%@ 7=t(-a,0,5)
%@ 5=t(-b,0,4)
%@ 4=t(-c,0,1)
%@ 11=t(b,10,1)
%@ 10=t(c,0,1)
%@ true.