@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.
```

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.
```

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.
```