Autumn Challenge 2023: Lion and Unicorn

Example
87

Well if you would compute Minatos ZDD normal form.
Then this here, Example 2:

?- sat((-a)*b+a*b), psa.
 zid = 7
        [-a,b]
        [a,b]

And this here:

?- sat(b), psa.
 zid = 2
        [b]

Would have the same ZDD. But it shows me two different results.

Why? Same problem with Example 1. Possibly to do that you
use 3-valued logic and not 2-valued logic. Your sat/1 predicate
doesn’t do what for example Markus Triskas sat/1 does?

Edit 11.12.2023
One could use Markus Triskas ZDD implementation to verify my claims.
It usage is as follows, before using sat/1, you must call zdd_set_vars/1
with a list of all Boolean variables that occur in your model.

https://github.com/triska/clpb/tree/master/zdd

Markus Triskas ZDD is already 8 years old, not sure whether
it still works. But if I remember well, it can show the resulting
ZDD. So could check against Markus Triskas ZDD.

My library is much simpler, there is no zdd_set_vars/1, its
just a parameter to tree3_eval/3: