# ZDD-based SAT with attr\_unfiy\_hook/2

**URL:** <https://swi-prolog.discourse.group/t/zdd-based-sat-with-attr-unfiy-hook-2/7461>\
**Category:** General\
**Created:** [May 19, 2024, 7:40pm UTC](https://swi-prolog.discourse.group/t/zdd-based-sat-with-attr-unfiy-hook-2/7461 "2024-05-19T19:40:05Z")\
**Posts on this page:** 6\
**Page:** 1

<div class="post-metadata">

**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\
**Post date:** [May 19, 2024, 7:40pm UTC](https://swi-prolog.discourse.group/t/zdd-based-sat-with-attr-unfiy-hook-2/7461/1 "2024-05-19T19:40:05Z")

</div>

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.

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

```

---

<div class="post-metadata">

**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\
**Post date:** [May 22, 2024, 3:09am UTC](https://swi-prolog.discourse.group/t/zdd-based-sat-with-attr-unfiy-hook-2/7461/2 "2024-05-22T03:09:43Z")

</div>

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

> [@kuniaki.mukai](#):
>
> ```prolog
> % ?- sat(A + B), sat_count(C), A = B, sat_count(D).
> 
> ```

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.

---

<div class="post-metadata">

**Author:** ![jan](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/jan/32/4_2.png) [@jan](https://swi-prolog.discourse.group/u/jan)\
**Post date:** [May 22, 2024, 7:44am UTC](https://swi-prolog.discourse.group/t/zdd-based-sat-with-attr-unfiy-hook-2/7461/3 "2024-05-22T07:44:49Z")

</div>

> [@kuniaki.mukai](#):
>
> I am wondering why the module prefix seems not necessary before `=`.

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

---

<div class="post-metadata">

**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\
**Post date:** [May 22, 2024, 10:35am UTC](https://swi-prolog.discourse.group/t/zdd-based-sat-with-attr-unfiy-hook-2/7461/4 "2024-05-22T10:35:37Z")

</div>

> [@jan](#):
>
> The module for the hook is determined by the attribute name. So, using
> 
> ```prolog
> put_attr(Var, mymodule, Data),
> 
> ```
> 
> it calls [attr\_unify\_hook/2](https://www.swi-prolog.org/pldoc/doc_for?object=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 ?

---

<div class="post-metadata">

**Author:** ![jan](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/jan/32/4_2.png) [@jan](https://swi-prolog.discourse.group/u/jan)\
**Post date:** [May 22, 2024, 11:00am UTC](https://swi-prolog.discourse.group/t/zdd-based-sat-with-attr-unfiy-hook-2/7461/5 "2024-05-22T11:00:29Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\
**Post date:** [May 22, 2024, 11:04am UTC](https://swi-prolog.discourse.group/t/zdd-based-sat-with-attr-unfiy-hook-2/7461/6 "2024-05-22T11:04:39Z")

</div>

> [@jan](#):
>
> [put\_attr/3](https://www.swi-prolog.org/pldoc/doc_for?object=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.

Thanks for great answer, which I never thought.