[m-users.] delay declarations in Mercury

[Zoltan Somogyi]

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
Mercury distribution.

> I am asking about the delay declarations, as I have found a paper
> describing an elegant implementation of a SAT solver in Prolog[1].

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 [22] and SMT [1] 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
> work?

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.

Zoltan.


-------------- next part --------------
A non-text attachment was scrubbed...
Name: stayl_hons.ps.gz
Type: application/gzip
Size: 122912 bytes
Desc: not available
URL: <http://lists.mercurylang.org/archives/users/attachments/20150123/605211b1/attachment.gz>