<div class="notebook"> <div class="nb-cell markdown" name="md1"> # Minato task From [Markus Triska](https://www.metalevel.at/prolog/attributedvariables#minatotask) This notebook demonstrates implementing zero-suppressed decision diagram (ZSDD or ZDD) as a constraint using SWI-Polog's attributed variables. The implementation is closely modelled after Markus Triska's implementation for SICStus Prolog, available from https://www.metalevel.at/prolog/minatotask.pl and described in https://www.metalevel.at/prolog/attributedvariables Markus claims that this task requires a _pre-unification_ hook as provided by the SICStus verify_attributes/3 interface. The reason for this is that we must distinguish variables that have been bound explicitly while establishing our path to a `true` node from those that have not been bound along this road. The latter set must be bound to `0` after finding a path that ends in `true`. Using SICStus we can reason about the pre-unification and post-unification state, solving this problem. In the SWI-Prolog attributed variable interface this is not possible as the hooks are called _after_ the unification and thus we do not know whether a variable was bound to `1` that is not on the path to `true` is `1` because it is the same variable also encountered on the path to `true` (in which case the ZDD is satisfied) or it is another variable (in which case the constraint must fail). See also this [mailing list message](https://groups.google.com/d/msg/swi-prolog/PlHdBTX_I7I/lnoKJzdiCAAJ), providing access to the thread and history. </div> <div class="nb-cell markdown" name="md4"> ## Tests We use the ZDD below to verify that variables not on the `true` path must be `0`. This means that if `X` is `1`, `Y` must be unified with `0` and a value of `1` is not admissible (third test). </div> <div class="nb-cell program" name="p4"> zdd([X,Y], ( X -> true ; ( Y -> true ; false ) )). </div> <div class="nb-cell query" data-tabled="true" name="q1"> test([0,Y], ZDD) </div> <div class="nb-cell query" data-tabled="true" name="q2"> test([1,Y], ZDD). </div> <div class="nb-cell query" data-tabled="true" name="q3"> test([1,1], ZDD). </div> <div class="nb-cell markdown" name="md5"> ### Sharing test In the following test, `Y` appears twice. `Y` must be `1` for the ZDD to be safisfied, but as we find this path we must be careful not to force it to `0` in the other branch, so the second test must succeed and the third must fail. </div> <div class="nb-cell program" name="p5"> zdd([X,Y], ( X -> ( Y -> true ; false) ; ( Y -> true ; false ) )). </div> <div class="nb-cell query" data-tabled="true" name="q4"> test([1,Y], ZDD). </div> <div class="nb-cell query" data-tabled="true" name="q5"> test([1,1], ZDD). </div> <div class="nb-cell query" data-tabled="true" name="q6"> test([1,0], ZDD). </div> <div class="nb-cell markdown" name="md2"> ## The test code </div> <div class="nb-cell program" data-background="true" name="p3"> test(Vars0, ZDD) :- zdd(Vars, ZDD), zdd(ZDD), Vars0 = Vars. </div> <div class="nb-cell markdown" name="md3"> ## The solver We solve this as follows: we copy the ZDD, creating a copy with fresh variables. Now we combine the copied and the original variables in the same node, creating nodes of the form below, where `AV` is the variable of the original ZDD and `V` is its shadow copy. - z(AV, V, Then, Else) We also copy the list of variables, so this is not a plain list, but a list of `AV-V` pairs. Now, as we restrict the ZDD we assign each shadow variable the value of the principle variable if this is bound. If we now find a path to `true`, our variable list contains the values of the variables that established this path in `V` and we must unify all `AV` whose `V` is unbound with `0`. </div> <div class="nb-cell program" data-background="true" name="p1"> %! zdd(+ZDD) is det. % % Use ZDD as a constraint between the variables inside the ZDD. % ZDD is a term of the following shape % % - b(true) % - b(false) % - true % - false % Terminal nodes. The values `true` and `false` are shorthands. % - (Var -> Then ; Else) % A ZDD non-terminal node. zdd(ZDD) :- term_variables(ZDD, Vars), copy_term(Vars+ZDD, ShadowVars+Shadow), zdd_nodes(ZDD, Shadow, Nodes), maplist(var_pair, Vars, ShadowVars, VarPairs), maplist(put_zdd(zdd_vs(Nodes, VarPairs)), Vars). zdd_nodes(true, true, b(true)). zdd_nodes(false, false, b(false)). zdd_nodes(b(Val), b(Val), b(Val)). zdd_nodes((V1->If1;Then1), (V2->If2;Then2), z(V1,V2,If,Then)) :- zdd_nodes(If1, If2, If), zdd_nodes(Then1, Then2, Then). var_pair(V1, V2, V1-V2). put_zdd(ZDD, Var) :- put_attr(Var, ZDD). attr_unify_hook(zdd_vs(ZDD0, Vs), AV) :- ( integer(AV) -> zdd_restriction(ZDD0, ZDD) ; throw(aliasing_not_implemented) ), remaining_vars_0(ZDD, Vs). remaining_vars_0(b(true), Vs) :- all_others_0(Vs). remaining_vars_0(z(_,_,_,_), _). all_others_0([]). all_others_0([AV-V|Vs]) :- ( var(V) -> AV = 0 ; true ), all_others_0(Vs). %! zdd_restriction(+ZDDIn, -ZDDOut) % % Compute the restriction of ZDDIn by replacing all determined % branching points with their branch. In addition, the shadow % variables are instantiated to the choice made, so we can distinguish % variables in the path to `true` from other variables. zdd_restriction(b(T), b(T)). zdd_restriction(z(AV, V, Then0, Else0), ZDD) :- ( AV == 0 -> V = 0, zdd_restriction(Else0, ZDD) ; AV == 1 -> V = 1, zdd_restriction(Then0, ZDD) ; var(AV) -> zdd_restriction(Then0, Then), zdd_restriction(Else0, Else), ZDD = z(AV, V, Then, Else) ; type_error(boolean, AV) ). </div> </div>