[m-dev.] The mode constraints branch summer project

Ralph Becket rafe at cs.mu.OZ.AU
Thu Dec 23 13:14:49 AEDT 2004

Richard Fothergill is working on the mode constraints branch project,
the aim of which is to try alternatives to the ROBDD solver to see if we
can appreciably reduce the analysis time.

Since Richard is only with us until the end of January, it seems a bit
much to expect him in that time to (a) learn enough about constraint
based mode analysis, (b) learn about building effective propagating SAT
solvers, and (c) implement a solver, plug it into the Mercury compiler,
debug the connection, then obtain performance results.

An alternative approach which I think is easily doable and will yield
valuable data is this: take two public domain best-of-breed SAT solvers
(e.g. zChaff and something lighter, but less cunning), get the
constraints branch compiler to also output the constraints it's sending
to the ROBDD solver in the format that these SAT solvers understand
(DIMACS is a standard, straightforward format that they all parse; it's
trivial to generate), and then see how long these solvers take compared
to the ROBDD solver.  This last part can be done off-line.  If these
solvers are fast enough, it will save us much implementation effort!

One other point: from the paper "Constraint-based mode analysis of
Mercury", with two exceptions, only binary constraints are necessary.
2-SAT is apparently *much* easier to tackle than the general SAT
problem.  The two exceptions are (1) when deciding whether a variable is
produced by a conjunction and (2) when deciding whether a variable is
produced by an if-then-else.  There could be a very fast solution for
the problem if we could handle the two exceptions without destroying

-- Ralph
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au

More information about the developers mailing list