1# CP/SAT
2
3This directory contains a next-gen Constraint Programming (CP) solver with
4clause learning. It is built on top of an efficient SAT/max-SAT solver whose
5code is also in this directory.
6
7The technology started in 2009. A complete presentation is available
8[here](https://people.eng.unimelb.edu.au/pstuckey/PPDP2013.pdf).
9
10CP-SAT was described during the CPAIOR 2020 masterclass. The recording is
11available [here](https://www.youtube.com/watch?v=lmy1ddn4cyw).
12
13To begin, skim
14[cp_model.proto](../cp_model.proto) to
15understand how optimization problems can be modeled using the solver. You can
16then solve a model with the functions in
17[cp_model_solver.h](../sat/cp_model_solver.h).
18
19
20## Parameters
21
22*   [sat_parameters.proto](../sat/sat_parameters.proto):
23    The SAT solver parameters. Also contains max-SAT and CP parameters.
24
25## Model
26
27The optimization model description and related utilities:
28
29*   [cp_model.proto](../cp_model.proto):
30    Proto describing a general Constraint Programming model.
31*   [cp_model_utils.h](../sat/cp_model_utils.h):
32    Utilities to manipulate and create a cp_model.proto.
33*   [cp_model_checker.h](../sat/cp_model_checker.h):
34    Tools to validate cp_model.proto and test a solution feasibility.
35*   [cp_model_solver.h](../sat/cp_model_solver.h):
36    The solver API.
37*   [cp_model_presolve.h](../sat/cp_model_presolve.h):
38    Presolve a cp_model.proto by applying simple rules to simplify a subsequent
39    solve.
40
41## SAT solver
42
43Stand-alone SAT solver and related files. Note that this is more than a basic
44SAT solver as it already includes non-clause constraints. However, these do not
45work on the general integer problems that the CP solver handles.
46
47Pure SAT solver:
48
49*   [sat_base.h](../sat/sat_base.h): SAT
50    core classes.
51*   [clause.h](../sat/clause.h): SAT clause
52    propagator with the two-watcher mechanism. Also contains propagators for
53    binary clauses.
54*   [sat_solver.h](../sat/sat_solver.h):
55    The SatSolver code.
56*   [simplification.h](../sat/simplification.h):
57    SAT postsolver and presolver.
58*   [symmetry.h](../sat/symmetry.h):
59    Dynamic symmetry breaking constraint in SAT. Not used by default.
60
61Extension:
62
63*   [pb_constraint.h](../sat/pb_constraint.h):
64    Implementation of a Pseudo-Boolean constraint propagator for SAT.
65    Pseudo-Boolean constraints are simply another name used in the SAT community
66    for linear constraints on Booleans.
67*   [no_cycle.h](../sat/no_cycle.h):
68    Implementation of a no-cycle constraint on a graph whose arc presences are
69    controlled by Boolean. This is a SAT propagator, not used in CP.
70*   [encoding.h](../sat/encoding.h): Basic
71    algorithm to encode integer variables into a binary representation. This is
72    not used by the CP solver, just by the max-SAT core based algorithm in
73    optimization.h.
74
75Input/output:
76
77*   [drat_writer.h](../sat/drat_writer.h):
78    Write UNSAT proof in the DRAT format. This allows to check the correctness
79    of an UNSAT proof with the third party program DRAT-trim.
80*   [opb_reader.h](../sat/opb_reader.h):
81    Parser for the .opb format for Pseudo-Boolean optimization problems.
82*   [sat_cnf_reader.h](../sat/sat_cnf_reader.h):
83    Parser for the classic SAT .cnf format. Also parses max-SAT files.
84*   [boolean_problem.proto](../sat/boolean_problem.proto):
85    Deprecated by cp_model.proto.
86
87## CP solver
88
89CP solver built on top of the SAT solver:
90
91*   [integer.h](../sat/integer.h): The
92    entry point, which defines the core of the solver.
93
94Basic constraints:
95
96*   [all_different.h](../sat/all_different.h):
97    Propagation algorithms for the AllDifferent constraint.
98*   [integer_expr.h](../sat/integer_expr.h):
99    Propagation algorithms for integer expression (linear, max, min, div, mod,
100    ...).
101*   [table.h](../sat/table.h): Propagation
102    algorithms for the table and automaton constraints.
103*   [precedences.h](../sat/precedences.h):
104    Propagation algorithms for integer inequalities (integer difference logic
105    theory).
106*   [cp_constraints.h](../sat/cp_constraints.h):
107    Propagation algorithms for other classic CP constraints (XOR, circuit,
108    non-overlapping rectangles, ...)
109*   [linear_programming_constraint.h](../sat/linear_programming_constraint.h):
110    Constraint that solves an LP relaxation of a set of constraints and uses the
111    dual-ray to explain an eventual infeasibility. Also implements reduced-cost
112    fixing.
113*   [flow_costs.h](../sat/flow_costs.h):
114    Deprecated. Network flow constraint. We use the generic
115    linear_programming_constraint instead.
116
117Scheduling constraints:
118
119*   [intervals.h](../sat/intervals.h):
120    Definition and utility for manipulating "interval" variables (a.k.a. task or
121    activities). This is the basic CP variable type used in scheduling problems.
122*   [disjunctive.h](../sat/disjunctive.h):
123    Propagation algorithms for the disjunctive scheduling constraint.
124*   [cumulative.h](../sat/cumulative.h),
125    [timetable.h](../sat/timetable.h),
126    [timetable_edgefinding.h](../sat/timetable_edgefinding.h):
127    Propagation algorithms for the cumulative scheduling constraint.
128*   [cumulative_energy.h](../sat/cumulative_energy.h):
129    Propagation algorithms for a more general cumulative constraint.
130*   [theta_tree.h](../sat/theta_tree.h):
131    Data structure used in the cumulative/disjunctive propagation algorithm.
132
133## Other
134
135*   [model.h](../sat/model.h): Generic
136    class that implements a basic dependency injection framework for singleton
137    objects and manages the memory ownership of all the solver classes.
138*   [optimization.h](../sat/optimization.h):
139    Algorithms to solve an optimization problem using a satisfiability solver as
140    a black box.
141*   [lp_utils.h](../sat/lp_utils.h):
142    Utility to scale and convert a MIP model into CP.
143
144## Recipes
145
146You can find a set a code recipes in
147[the documentation directory](doc/README.md).
148