MiniZinc: the lazy clause generation solver
In the following two papers (for CP2009), a new Zinc/MiniZinc solver using both finite domain and SAT is discussed: the lazy clause generation solver:
- T. Feydy and P.J. Stuckey: Lazy clause generation reengineered:
Abstract Lazy clause generation is a powerful hybrid approach to com-
binatorial optimization that combines features from SAT solving and fi-
nite domain (FD) propagation. In lazy clause generation finite domain
propagators are considered as clause generators that create a SAT de-
scription of their behaviour for a SAT solver. The ability of the SAT
solver to explain and record failure and perform conflict directed back-
jumping are then applicable to FD problems. The original implemen-
tation of lazy clause generation was constructed as a cut down finite
domain propagation engine inside a SAT solver. In this paper we show
how to engineer a lazy clause generation solver by embedding a SAT
solver inside an FD solver. The resulting solver is flexible, efficient and
easy to use. We give experiments illustrating the effect of different design
choices in engineering the solver.
- A. Schutt, T. Feydy, P.J. Stuckey, and M. Wallace: Why cumulative decomposition is not as bad as it sounds.
AbstractThe global cumulative constraint was proposed for mod-
elling cumulative resources in scheduling problems for finite domain (FD)
propagation. Since that time a great deal of research has investigated new
stronger and faster filtering techniques for cumulative, but still most of
these techniques only pay off in limited cases or are not scalable. Re-
cently, the “lazy clause generation” hybrid solving approach has been
devised which allows a finite domain propagation engine possible to take
advantage of advanced SAT technology, by “lazily” creating a SAT model
of an FD problem as computation progresses. This allows the solver to
make use of SAT nogood learning and autonomous search capabilities.
In this paper we show that using lazy clause generation where we model
cumulative constraint by decomposition gives a very competitive im-
plementation of cumulative resource problems. We are able to close a
number of open problems from the well-established PSPlib benchmark
library of resource-constrained project scheduling problems.
This solver (the lazy solver) has been included in the MiniZinc distribution since version 1.0, and has been improved each version, e.g. by adding primitives it supports. See the NEWS file for more information.
I have tested the lazy solver with some problems, for example nonogram.mzn (which is implemented inefficient without the regular constraint), and am very impressed by it. It is very fast, though it cannot solve the P200 problem in a reasonable time.
Some comments about the lazy solver (some limitation is hopefully lifted in the future):
- it cannot handle set vars.
- all decision variables must be explicit bounded, e.g.
var int: x;will not work, instead use something likevar 1..10: x;.
- Labeling: The papers state that the default labeling (e.g.
solve satisfy) is often very good.
Conclusion: The lazy solver is definitely worth more testing.