this repo has no description
dekker.one
1# Chuffed, a lazy clause generation 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## Usage
11
12The easiest way to use Chuffed is as a backend to the [MiniZinc constraint modelling language](http://www.minizinc.org). Compiling Chuffed using the
13instructions below will create the `fzn-chuffed` executable that can interpret
14MiniZinc's FlatZinc solver language.
15
16You can also use Chuffed directly from C++. Take a look at the files in the
17`examples` folder to get started.
18
19## Compilation
20
21Chuffed can be compiled on Windows, macOS and Linux.
22
23#### Prerequisites
24
25You need a recent C++
26compiler that supports C++11 (e.g. Microsoft Visual Studio 2013, gcc 4.8, clang), as well as the CMake build tool (at least version 3.1).
27
28#### CMake & Co
29
30To build the `fzn-chuffed` executable:
31
32 mkdir build
33 cd build
34 cmake ..
35 cmake --build .
36
37To install `fzn-chuffed` run the following command in the build directory:
38`cmake --build . --target install`. The installation directory can be chosen by
39appending `-DCMAKE_INSTALL_PREFIX=$LOCATION` with the chosen location to the
40initial CMake command.
41
42To build the C++ examples:
43
44 mkdir build
45 cd build
46 cmake ..
47 cmake --build . --target examples
48
49To build a debug or release, chosen by default, version use the following command instead of `cmake ..`:
50
51 cmake -DCMAKE_BUILD_TYPE=[Debug|Release] ..
52
53#### Integration with CP Profiler
54
55The [CP Profiler tool](https://github.com/cp-profiler) can be used with Chuffed
56to visualise the search trees and analyse the nogoods that Chuffed explores
57when solving a problem. In order to enable profiling support, you need to fetch the profiler connection code as a submodule by executing the following command
58in the root directory of your local copy of the Chuffed git repository:
59
60 git submodule update --init
61
62After that, you can run `cmake` and compile `fzn-chuffed` as described above.
63
64## Description
65
66Chuffed is a state of the art lazy clause solver designed from the ground up
67with lazy clause generation in mind. Lazy clause generation is a hybrid
68approach to constraint solving that combines features of finite domain
69propagation and Boolean satisfiability. Finite domain propagation is
70instrumented to record the reasons for each propagation step. This creates an
71implication graph like that built by a SAT solver, which may be used to create
72efficient nogoods that record the reasons for failure. These nogoods can be
73propagated efficiently using SAT unit propagation technology. The resulting
74hybrid system combines some of the advantages of finite domain constraint
75programming (high level model and programmable search) with some of the
76advantages of SAT solvers (reduced search by nogood creation, and effective
77autonomous search using variable activities).
78
79The FD components of Chuffed are very tightly integrated with a SAT solver. For
80"small" variables (|D| <= 1000), SAT variables representing [x = v] or [x >= v]
81are eagerly created at the start of the problem. Channelling constraints are
82natively enforced by the variable objects in order to keep the FD solver and
83the SAT solver's view of the domains fully consistent at all times. For "large"
84variables (|D| > 1000), the SAT variables are lazily generated as needed. Every
85propagator in Chuffed has been instrumented so that all propagation can be
86explained by some combination of the literals in the SAT solver. An explanation
87is of the form a_1 /\ ... /\ a_n -> d, where a_i represent domain restrictions
88which are currently true, and d represents the domain change that is implied.
89e.g. Suppose z >= x + y, and we have x >= 3, y >= 2. Then the propagator would
90propagate x >= 5 with explanation clause x >= 3 /\ y >= 2 -> z >= 5.
91
92The explanations for each propagation form an implication graph. This allows us
93to do three very important things. Firstly, we can derive a nogood to explain
94each failure. Such nogoods often allow us to avoid a very large amount of
95redundant work, thus producing search trees which are orders of magnitude
96smaller. Secondly, nogoods allow us to make informed choices about
97non-chronological back-jumping. When no literal from a decision level appears
98in the nogood, it is indicative of the fact that the decision made at that
99level was completely irrelevant to the search. Thus by back-jumping over such
100decisions, we retrospectively avoid making such bad decisions, and hopefully
101make good decisions instead which drive the search towards failure. Thirdly, by
102analysing the conflict, we can actively gain some information about what good
103decision choices are. The Variable State Independent Decaying Sum (VSIDS)
104heuristic is an extremely effective search heuristic for SAT problems, and is
105also extremely good for a range of CP problems. Each variables has an
106associated activity, which is increased whenever the variable is involved in
107the conflict. Variables with the highest activity is chosen as the decision
108variable at each node. The activities are decayed to reflect the fact that the
109set of important variables changes with time.
110
111Although Chuffed implements lazy clause generation, which is cutting edge and
112rather complex, the FD parts of Chuffed are relatively simple. In fact, it is
113quite minimalistic. Chuffed only supports 3 different propagator priorities.
114Chuffed implements a number of global propagators (alldiff, inverse,
115minimum, table, regular, mdd, cumulative, disjunctive, circuit, difference).
116It also only supports two kinds of integer variables. Small integer variables
117for which the domain is represented by a byte string.
118And large integer variables for which the domain is represented only by its
119upper and lower bound (no holes allowed). All boolean variables and boolean
120constraints are handled by the builtin SAT solver.
121
122Great pains have been taken to make everything as simple and efficient as
123possible. The solver, when run with lazy clause generation disabled, is
124somewhat comparable in speed with older versions of Gecode. The overhead from
125lazy clause generation ranges from negligible to perhaps around 100%. The
126search reduction, however, can reach orders of magnitude on appropriate
127problems. Thus lazy clause generation is an extremely important and useful
128technology. The theory behind lazy clause generation is described in much
129greater detail in various papers.