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