this repo has no description
dekker.one
1Chuffed - A lazy clause solver
2
3Geoffrey Chu, Peter J. Stuckey, Andreas Schutt, Thorsten Ehlers, Graeme Gange, Kathryn Francis
4
5Data61, CSIRO, Australia
6
7Department of Computing and Information Systems
8University of Melbourne, Australia
9
10
11Chuffed is a state of the art lazy clause solver designed from the ground up
12with lazy clause generation in mind. Lazy clause generation is a hybrid
13approach to constraint solving that combines features of finite domain
14propagation and Boolean satisfiability. Finite domain propagation is
15instrumented to record the reasons for each propagation step. This creates an
16implication graph like that built by a SAT solver, which may be used to create
17efficient nogoods that record the reasons for failure. These nogoods can be
18propagated efficiently using SAT unit propagation technology. The resulting
19hybrid system combines some of the advantages of finite domain constraint
20programming (high level model and programmable search) with some of the
21advantages of SAT solvers (reduced search by nogood creation, and effective
22autonomous search using variable activities).
23
24The FD components of Chuffed are very tightly integrated with a SAT solver. For
25"small" variables (|D| <= 1000), SAT variables representing [x = v] or [x >= v]
26are eagerly created at the start of the problem. Channelling constraints are
27natively enforced by the variable objects in order to keep the FD solver and
28the SAT solver's view of the domains fully consistent at all times. For "large"
29variables (|D| > 1000), the SAT variables are lazily generated as needed. Every
30propagator in Chuffed has been instrumented so that all propagation can be
31explained by some combination of the literals in the SAT solver. An explanation
32is of the form a_1 /\ ... /\ a_n -> d, where a_i represent domain restrictions
33which are currently true, and d represents the domain change that is implied.
34e.g. Suppose z >= x + y, and we have x >= 3, y >= 2. Then the propagator would
35propagate x >= 5 with explanation clause x >= 3 /\ y >= 2 -> z >= 5.
36
37The explanations for each propagation form an implication graph. This allows us
38to do three very important things. Firstly, we can derive a nogood to explain
39each failure. Such nogoods often allow us to avoid a very large amount of
40redundant work, thus producing search trees which are orders of magnitude
41smaller. Secondly, nogoods allow us to make informed choices about
42non-chronological back-jumping. When no literal from a decision level appears
43in the nogood, it is indicative of the fact that the decision made at that
44level was completely irrelevant to the search. Thus by back-jumping over such
45decisions, we retrospectively avoid making such bad decisions, and hopefully
46make good decisions instead which drive the search towards failure. Thirdly, by
47analysing the conflict, we can actively gain some information about what good
48decision choices are. The Variable State Independent Decaying Sum (VSIDS)
49heuristic is an extremely effective search heuristic for SAT problems, and is
50also extremely good for a range of CP problems. Each variables has an
51associated activity, which is increased whenever the variable is involved in
52the conflict. Variables with the highest activity is chosen as the decision
53variable at each node. The activities are decayed to reflect the fact that the
54set of important variables changes with time.
55
56Although Chuffed implements lazy clause generation, which is cutting edge and
57rather complex, the FD parts of Chuffed are relatively simple. In fact, it is
58quite minimalistic. Chuffed only supports 3 different propagator priorities.
59Chuffed implements a number of global propagators (alldiff, inverse,
60minimum, table, regular, mdd, cumulative, disjunctive, circuit, difference).
61It also only supports two kinds of integer variables. Small integer variables
62for which the domain is represented by a byte string.
63And large integer variables for which the domain is represented only by its
64upper and lower bound (no holes allowed). All boolean variables and boolean
65constraints are handled by the builtin SAT solver.
66
67Great pains have been taken to make everything as simple and efficient as
68possible. The solver, when run with lazy clause generation disabled, is
69somewhat comparable in speed with older versions of Gecode. The overhead from
70lazy clause generation ranges from negligible to perhaps around 100%. The
71search reduction, however, can reach orders of magnitude on appropriate
72problems. Thus lazy clause generation is an extremely important and useful
73technology. The theory behind lazy clause generation is described in much
74greater detail in various papers.