ZDD-based SAT with attr_unfiy_hook/2

General
1

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

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.

3

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.

4

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 ?

5

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.

6

Thanks for great answer, which I never thought.