b027e57e95
- Currently not implemented... Add abseil patch - Add patches/absl-config.cmake Makefile: Add abseil-cpp on unix - Force abseil-cpp SHA1 to 45221cc note: Just before the PR #136 which break all CMake Makefile: Add abseil-cpp on windows - Force abseil-cpp SHA1 to 45221cc note: Just before the PR #136 which break all CMake CMake: Add abseil-cpp - Force abseil-cpp SHA1 to 45221cc note: Just before the PR #136 which break all CMake port to absl: C++ Part - Fix warning with the use of ABSL_MUST_USE_RESULT > The macro must appear as the very first part of a function declaration or definition: ... Note: past advice was to place the macro after the argument list. src: dependencies/sources/abseil-cpp-master/absl/base/attributes.h:418 - Rename enum after windows clash - Remove non compact table constraints - Change index type from int64 to int in routing library - Fix file_nonport compilation on windows - Fix another naming conflict with windows (NO_ERROR is a macro) - Cleanup hash containers; work on sat internals - Add optional_boolean sub-proto Sync cpp examples with internal code - reenable issue173 after reducing number of loops port to absl: Python Part - Add back cp_model.INT32_MIN|MAX for examples Update Python examples - Add random_tsp.py - Run words_square example - Run magic_square in python tests port to absl: Java Part - Fix compilation of the new routing parameters in java - Protect some code from SWIG parsing Update Java Examples port to absl: .Net Part Update .Net examples work on sat internals; Add C++ CP-SAT CpModelBuilder API; update sample code and recipes to use the new API; sync with internal code Remove VS 2015 in Appveyor-CI - abseil-cpp does not support VS 2015... improve tables upgrade C++ sat examples to use the new API; work on sat internals update license dates rewrite jobshop_ft06_distance.py to use the CP-SAT solver rename last example revert last commit more work on SAT internals fix
CP/SAT
This directory contains a next-gen Constraint Programming (CP) solver with clause learning. It is built on top of an efficient SAT/max-SAT solver whose code is also in this directory.
To begin, skim cp_model.proto to understand how optimization problems can be modeled using the solver. You can then solve a model with the functions in cp_model_solver.h.
Parameters
- sat_parameters.proto: The SAT solver parameters. Also contains max-SAT and CP parameters.
Model
The optimization model description and related utilities:
- cp_model.proto: Proto describing a general Constraint Programming model.
- cp_model_utils.h: Utilities to manipulate and create a cp_model.proto.
- cp_model_checker.h: Tools to validate cp_model.proto and test a solution feasibility.
- cp_model_solver.h: The solver API.
- cp_model_presolve.h: Presolve a cp_model.proto by applying simple rules to simplify a subsequent solve.
SAT solver
Stand-alone SAT solver and related files. Note that this is more than a basic SAT solver as it already includes non-clause constraints. However, these do not work on the general integer problems that the CP solver handles.
Pure SAT solver:
- sat_base.h: SAT core classes.
- clause.h: SAT clause propagator with the two-watcher mechanism. Also contains propagators for binary clauses.
- sat_solver.h: The SatSolver code.
- simplification.h: SAT postsolver and presolver.
- symmetry.h: Dynamic symmetry breaking constraint in SAT. Not used by default.
Extension:
- pb_constraint.h: Implementation of a Pseudo-Boolean constraint propagator for SAT. Pseudo-Boolean constraints are simply another name used in the SAT community for linear constraints on Booleans.
- no_cycle.h: Implementation of a no-cycle constraint on a graph whose arc presences are controlled by Boolean. This is a SAT propagator, not used in CP.
- encoding.h: Basic algorithm to encode integer variables into a binary representation. This is not used by the CP solver, just by the max-SAT core based algorithm in optimization.h.
Input/output:
- drat_writer.h: Write UNSAT proof in the DRAT format. This allows to check the correctness of an UNSAT proof with the third party program DRAT-trim.
- opb_reader.h: Parser for the .opb format for Pseudo-Boolean optimization problems.
- sat_cnf_reader.h: Parser for the classic SAT .cnf format. Also parses max-SAT files.
- boolean_problem.proto: Deprecated by cp_model.proto.
CP solver
CP solver built on top of the SAT solver:
- integer.h: The entry point, which defines the core of the solver.
Basic constraints:
- all_different.h: Propagation algorithms for the AllDifferent constraint.
- integer_expr.h: Propagation algorithms for integer expression (linear, max, min, div, mod, ...).
- table.h: Propagation algorithms for the table and automata constraints.
- precedences.h: Propagation algorithms for integer inequalities (integer difference logic theory).
- cp_constraints.h: Propagation algorithms for other classic CP constraints (XOR, circuit, non-overlapping rectangles, ...)
- linear_programming_constraint.h: Constraint that solves an LP relaxation of a set of constraints and uses the dual-ray to explain an eventual infeasibility. Also implements reduced-cost fixing.
- flow_costs.h: Deprecated. Network flow constraint. We use the generic linear_programming_constraint instead.
Scheduling constraints:
- intervals.h: Definition and utility for manipulating "interval" variables (a.k.a. task or activities). This is the basic CP variable type used in scheduling problems.
- disjunctive.h: Propagation algorithms for the disjunctive scheduling constraint.
- cumulative.h, timetable.h, overload_checker.h, timetable_edgefinding.h: Propagation algorithms for the cumulative scheduling constraint.
- cumulative_energy.h: Propagation algorithms for a more general cumulative constraint.
- theta_tree.h: Data structure used in the cumulative/disjunctive propagation algorithm.
Other
- model.h: Generic class that implements a basic dependency injection framework for singleton objects and manages the memory ownership of all the solver classes.
- optimization.h: Algorithms to solve an optimization problem using a satisfiability solver as a black box.
- lp_utils.h: Utility to scale and convert a MIP model into CP.
Recipes
You can find a set a code recipes in the documentation directory.