[m-users.] delay declarations in Mercury
zoltan.somogyi at runbox.com
Fri Jan 23 21:40:22 AEDT 2015
On Fri, 23 Jan 2015 10:47:23 +0100, Matthias Guedemann <matthias.guedemann at googlemail.com> wrote:
> > The
> > Mercury compiler does have such a transformation, but it won't handle
> > every situation you may want it to.
> Could you point me to where to find more information about this, please?
You can enable the optimization via the Mercury compiler option
--constraint-propagation. If you want to know how it works, you can
read Simon Taylor's honours thesis (attached), the relevant papers
it references (such as refs 8 and 16), or the Mercury compiler
module that implements it, which is in compiler/constraints.m in the
> I am asking about the delay declarations, as I have found a paper
> describing an elegant implementation of a SAT solver in Prolog.
It may be elegant, but it is also uncompetitive. A quote from page 15
of that paper:
Owing to the issues outlined above, the solver presented in this paper is
not going to be competitive on the large, difficult problems set as
challenges in the international SAT  and SMT  competitions.
And I am pretty sure that is a severe understatement. In that field,
new advances often get orders-of-magnitude improvements.
And the idea of delaying constraints until the variables in them
are known is much older than that paper, so there have been *many*
advances since it was invented.
> So, the watch is updated if either Var1 or Var2 becomes bound, and this
> is decided using the impure nonvar/1.
> My initial idea was to provide two different predicates for the update:
> one with mode "in" for Var1 and one with mode "in" for Var2, in order to
> eliminate nonvar/1; and to use the disjunction of these two predicates
> in the predicate watch (and watch with two different modes). Would this
Would this work in what language? In Mercury, no. In Prolog, I don't know.
I used to know pretty well how delay declarations and the like worked,
but that was several years ago, and they have probably changed since then.
> My goal is not to have the most efficient SAT solver, but to have a
> simple implementation to try out different approaches to SAT-based
> model-checking on top.
Try them out for what purpose? If you just want to learn, fine; if you
want software to use, you are far better off using, or at least starting with,
an established system.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 122912 bytes
Desc: not available
More information about the users