I would appreciate if you add to your page on an explanation of
your requirement on pre unify_hook for those who have only
basics of Boolean constraints like me. So far I must be missing
your point between pre unify_hook and such basics.
( X -> ( Y -> true ; false) ; ( Y -> true ; false ) )
?- zdd_set_vars([X,Y]),sat((X*Y) + (~X* Y)).
node(4)-(X->node(3);node(3)),node(3)-(Y->true;false),
Is ZDD a just prolog term ? if so what is the semantics of the ZDD ?
For me, result of the query depends on meanings of
these symbols; ((true -> true) or ((true->true) or false)) = true
in Boolean, isn’t it ? Surely I must be missing something.
> To unsubscribe from this group and stop receiving emails from it, send an email to swi-prolog+unsubscribe@googlegroups.com.
> Visit this group at https://groups.google.com/group/swi-prolog.
> For more options, visit https://groups.google.com/d/optout.
--
You received this message because you are subscribed to the Google Groups "SWI-Prolog" group.
To unsubscribe from this group and stop receiving emails from it, send an email to swi-prolog+unsubscribe@googlegroups.com.
Module:verify_attributes(-Var, +Value, -Goals)
https://sicstus.sics.se/sicstus/docs/3.7.1/html/sicstus_17.html
The SICStus documentation also says so:
"
It may succeed non-deterministically, in which
case attr_unify_hook(_) :-
...
call(Fa)
...
But Markus Trisa writes:
"The way in which this hook currently works makes the implementation of important classes of constraint solvers impossible or at least extremely impractical. For increased generality and convenience, simultaneous unifications as in[X,Y]=[0,1]
should be processed sequentially by the Prolog engine, or a more general hook should be provided in the future."
I am not sure whether SICStus Prolog solves the problem.
SICStus Prolog writes:
"This predicate is called whenever a variable Var that might have attributes in Module is about to be bound to Value (it might have none). The unification resumes after the call toverify_attributes/3
."
So although the hook is synchronous to the unification,
i.e. step by step. I am not sure what happens to the
goals. The specification only says:
"It is expected to return, in Goals, a list of goals
to be called after Var has been bound to Value.What is the meaning of after here? How much after? Are
we really save for what Markus Triska thinks a problem.
A possible workaround for Markus Triskas problem would
be to store the ZDD with different variables, and have
a map that shows which variables correspond to the
variables in the ZDD.
The in the SWI-Prolog hook, he could work step-by-step
through this map, although the map would have received
a "simultaneous" or better "multiple variable" instantiation.
Just some guesses what could be done...
> <mailto:swi-prolog+unsub...@googlegroups.com>.
> > <mailto:swi-prolog+unsub...@googlegroups.com>.
; get_attr_local(X, Fb) ->
...
meta_conj(Fb, Goal, C), put_attr_local(X, C) % rescue conjunction
...
% A (meta) conjunction of two goals meta_conj('$:'(Fa), '$:'(Fb), '$:'('basiccontrol:,'(Fa, Fb))).
Welcome to SWI-Prolog (threaded, 64 bits, version 7.5.8)
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.
?- freeze(X, write(foo)), freeze(X, write(bar)), get_attrs(X, A).
A = att(freeze, '$and'(user:write(foo), user:write(bar)), []),
> > > <mailto:swi-prolog+unsub...@googlegroups.com>.
> > > > <mailto:swi-prolog+unsub...@googlegroups.com>.
; put_attr_local(X, Goal)https://ciao-lang.org/docs/ciao/attr_doc.html
> > > > > <mailto:swi-prolog+unsub...@googlegroups.com>.
> For more options, visit <a href="https://groups.google.com/d/optout" rel="nofollow" target="_blank" onmousedown="this.href='https://groups.
... for every unit clause l in Φ Φ ← unit-propagate(l, Φ);
...https://en.wikipedia.org/wiki/DPLL_algorithm
?- ZDD = ( X -> b(true) ; ( Y -> b(true) ; b(false) ) ), Vs = [X,Y], variables_set_zdd(Vs, ZDD), Vs = [1,1]. noIf a ZDD is zero suppressed then the above ZDD is equivalent
7.1 Pigeon Hole Problems
ZDD = ( X -> true ; ( Y -> true ; false ) )
solve_obdd(true). |
solve_obdd((X -> _;B)) :- X=0, solve_obdd(B). |
This kind of mistakes could be avoided with the SICStus interface.
SICStus is also widely known as one of the fastest Prolog systems
available. Take from this what you will.
It probably would be even faster when it adopted the SWI-Prolog attvar
interface as, however you look at it, post-unification hooks simply have
to do less work and have less impact on the rest of the system.
(_8118->(_8132->false;true);_8132->true;false))
Is not a ZDD.
You didn't compress according to this rule:
Jan Burse wrote:
> ZDD compression:
> (X -> false; A) == A
_8132->false
And it is constant 0 (same as false).
But you didn't supress it, so its not ZDD.
This predicate is called whenever an attributed variable Var (which has at least one attribute) is about to be bound to Value (a non-variable term or another attributed variable). When Var is to be bound to Value, a special interrupt called attributed variable interrupt is triggered, and then XSB's interrupt handler (written in Prolog) calls verify_attributes/2. If it fails, the unification is deemed to have failed. It may succeed non-deterministically, in which case the unification might backtrack to give another answer."
http://xsb.sourceforge.net/shadow_site/manual2/node4.htmlSince ZDD are little bit complex, why not discuss the API issue
on the basis of CNF. Here is a nice paper, with a SICStus
solution. Can this be done in SWI-Prolog. If yes, how? If no, why?
A Pearl on SAT Solving in Prolog
Jacob M. Howe and Andy King, 2010
http://www.staff.city.ac.uk/~jacob/solver/flops.pdf
2017-09-08 12:48 GMT+02:00 Jan Burse <burs...@gmail.com>:Since ZDD are little bit complex, why not discuss the API issue
on the basis of CNF. Here is a nice paper, with a SICStus
solution. Can this be done in SWI-Prolog. If yes, how? If no, why?
A Pearl on SAT Solving in Prolog
Jacob M. Howe and Andy King, 2010
http://www.staff.city.ac.uk/~jacob/solver/flops.pdfJan, thanks so much. It's really a pearl !
Welcome to SWI-Prolog (threaded, 64 bits, version 7.5.8)
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.
?- reduce([add(s(s(0)),s(s(0)),X)]).
X = s(s(s(s(0)))) .
System | Abs | Rel SWI |
our interpreter | 5.710 | 311% |
Lean Prolog | 3.991 | 217% |
Styla | 13.164 | 717% |
SWI-Prolog | 1.835 | 100% |
System | Abs | Rel SWI |
Jekejeke | 0.905 | 157% |
SWI-Prolog | 0.578 | 100% |
Hi Carlo,
There's an implementation of block in swi prolog's
library/dialect/sicstus directory. I'm always confused by the module
syntax, but it's possible to consult the file directly. Then the :-
block statement is accepted. If I understand the paper/code correctly,
without blocking, unit propagation is applied too eagerly (because the
watches are not sufficiently delayed).
cheers, Martin
On 09/08/2017 05:15 PM, Carlo Capelli wrote:
>
>
> 2017-09-08 12:48 GMT+02:00 Jan Burse <burs...@gmail.com
> <mailto:burs...@gmail.com>>:
>
> Since ZDD are little bit complex, why not discuss the API issue
> on the basis of CNF. Here is a nice paper, with a SICStus
> solution. Can this be done in SWI-Prolog. If yes, how? If no, why?
>
> A Pearl on SAT Solving in Prolog
> Jacob M. Howe and Andy King, 2010
> http://www.staff.city.ac.uk/~jacob/solver/flops.pdf
> <http://www.staff.city.ac.uk/%7Ejacob/solver/flops.pdf>
>
>
> Jan, thanks so much. It's really a pearl !
> I simply copied the ~20 lines into SWI-Prolog IDE, commented out the :-
> block (is it important ?), and tried:
>
> ?- L = [[false-X, true-Y], [false-X,false-Z]], sat(L, [X,Y,Z]), writeln(L).
> [[false-false,true-true],[false-false,false-true]]
> L = [[false-false, true-true], [false-false, false-true]],
> X = false,
> Y = Z, Z = true ;
> ...
>
> <snip>
>
> --
> You received this message because you are subscribed to the Google
> Groups "SWI-Prolog" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to swi-prolog+unsubscribe@googlegroups.com
> <mailto:swi-prolog+unsub...@googlegroups.com>.
> Visit this group at https://groups.google.com/group/swi-prolog.
> For more options, visit https://groups.google.com/d/optout.
--
You received this message because you are subscribed to the Google Groups "SWI-Prolog" group.
To unsubscribe from this group and stop receiving emails from it, send an email to swi-prolog+unsubscribe@googlegroups.com.
Am Freitag, 8. September 2017 17:39:40 UTC+2 schrieb cc.carlo.cap:A Hitchhiker’s Guide to Reinventing a Prolog Machine( btw, I've started a (lazy) attempt to port from Java to Javascript )
--
You received this message because you are subscribed to the Google Groups "SWI-Prolog" group.
To unsubscribe from this group and stop receiving emails from it, send an email to swi-prolog+unsubscribe@googlegroups.com.