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

[David Overton]

On Thu, Dec 23, 2004 at 01:14:49PM +1100, Ralph Becket wrote:
> 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!

This sounds like a good approach.

> 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
> performance.

The contraint solver on the mode constraints branch already treats 2-SAT
constraints differently to general contraints.  They are extracted from
the ROBDD and solved using resolution.  We didn't describe this in the
conference paper due to space limits, but the details are in section 6.5
of my thesis.  You might want to try using a more sophisticated 2-SAT
solver on these.   However the majority of the solving time was still
spent with the remaining ROBDD (conjunctions and if-then-else are rather
common constructs in Mercury programs!) so you may want to concentrate
on a replacement for these.  One complication is that the algorithm I
used for extracting the 2-SAT constraints is closely tied to the
structure of the ROBDD graph.

David
-- 
David Overton
WWW: http://www.overtons.id.au/
Mobile Phone (UK): +44 7799 344 322
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------