I posted on ZDD-based handling on DNF (disjunctive normal form ).

I added the following small module named `zsat`

to use attributed variables

as basic propositions. So far prolog variables X in sat input was numbervars-ed

to special ground term `'$VAR'(I)`

with some integer index I. The idea is to put this index I

as an attribute of variable X, where `zsat`

is the name of the attribute.

The meaning of `X = Y`

is, of course, taken as `(X -> Y) AND (Y -> X)`

.

This post is just from curiosity to treat prolog unification as logical equivalence.

I have no idea and plan to develop further on zdd-based sat.

```
:- module(zsat, []).
% ?- sat. % Setup for sat to work.
% ?- sat(a = b), sat(X = Y), sat_count(C).
%@ C = 4,
%@ put_attr(X, zsat, 0),
%@ put_attr(Y, zsat, 1).
% ?- sat(A + B), sat_count(C), A = B, sat_count(D).
%@ A = B,
%@ C = 3,
%@ D = 1,
%@ put_attr(B, zsat, 0).
% ?- sat(A + B + C + D), sat_count(Count0),
% A = B, B = C, C = D, sat_count(Count1).
%@ A = B, B = C, C = D,
%@ Count0 = 15,
%@ Count1 = 1,
%@ put_attr(D, zsat, 0).
attr_unify_hook(X, Y):- var(Y),
( get_attr(Y, zsat, U) ->
sat_index_equal(U, X)
; put_attr(Y, zsat, X)
).
%
sat_index_equal(X, X).
sat_index_equal(I, J):- sat(@('$VAR'(I))= @('$VAR'(J))).
```