# ZDD-based SAT with attr_unfiy_hook/2

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

I like the idea that Prolog variable is used in ZDD by `attr_unfify_hook/2`. But
I am wondering why the module prefix seems not necessary before `=`.

In fact, at first I wrote `zsat:(A=B)` for `A=B` thinking the prefix is necessary
to make clear which `attr_unify_hook` definition is referred. But as such style looked not so elegant, I dropped it and have found it is OK. I tried a complex explanation in mind, which I am not sure, and I may be missing something.

The module for the hook is determined by the attribute name. So, using

``````put_attr(Var, mymodule, Data),
``````

it calls attr_unify_hook/2 in `mymodule`.

Does `put_attr/3` check if the variable has another attribute of module name ? I thought otherwise ambiguity might occur on which definition of hooks to be selected. Am I missing some basics, as usual ?

put_attr/3 checks nothing (well, that the first argument is a variable and the second an atom). If there are multiple attributes, each hook is called. If there is no matching module you simply get an undefined predicate exception.

Thanks for great answer, which I never thought.