Skip to content

Files

Latest commit

5d76455 · Mar 8, 2023

History

History
This branch is 3672 commits behind google/or-tools:stable.

sat

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
Feb 6, 2023
Feb 10, 2023
Mar 6, 2023
Mar 6, 2023
Mar 2, 2023
Mar 6, 2023
Feb 10, 2023
Feb 10, 2023
Feb 10, 2023
Jun 16, 2022
Jun 16, 2022
Jun 16, 2022
Jun 16, 2022
Jun 16, 2022
Sep 21, 2022
Jun 16, 2022
Feb 6, 2023
Feb 6, 2023
Jun 16, 2022
Jun 16, 2022
Jan 5, 2023
Jan 5, 2023
Feb 16, 2023
Dec 12, 2022
Oct 17, 2022
Feb 13, 2023
Sep 9, 2022
Feb 13, 2023
Jan 3, 2023
Feb 17, 2023
Feb 16, 2023
Feb 13, 2023
Jun 16, 2022
Jun 16, 2022
Jun 16, 2022
Jun 16, 2022
Mar 8, 2023
Mar 8, 2023
Feb 15, 2023
Nov 29, 2022
Oct 3, 2022
Mar 8, 2023
Dec 20, 2022
Dec 15, 2022
Jun 16, 2022
Mar 8, 2023
Mar 8, 2023
Sep 21, 2022
Jun 16, 2022
Jun 23, 2022
Aug 18, 2022
Feb 3, 2023
Feb 3, 2023
Jun 16, 2022
Jun 16, 2022
Jan 20, 2023
Aug 18, 2022
Aug 18, 2022
Aug 18, 2022
Jan 3, 2023
Dec 12, 2022
Jun 16, 2022
Jun 16, 2022
Jun 16, 2022
Jun 16, 2022
Oct 5, 2022
Jun 16, 2022
Sep 21, 2022
Jun 16, 2022
Feb 15, 2023
Jun 16, 2022
Feb 15, 2023
Feb 15, 2023
Dec 5, 2022
Mar 2, 2023
Mar 2, 2023
Jan 27, 2023
Feb 20, 2023
Feb 15, 2023
Dec 15, 2022
Sep 23, 2022
Sep 23, 2022
Oct 19, 2022
Jun 16, 2022
Feb 6, 2023
Nov 18, 2022
Mar 2, 2023
Feb 1, 2023
Feb 3, 2023
Feb 1, 2023
Oct 11, 2022
Oct 17, 2022
Feb 15, 2023
Jan 16, 2023
Feb 1, 2023
Jan 5, 2023
Oct 13, 2022
Jun 16, 2022
Sep 27, 2022
Feb 10, 2023
Dec 15, 2022
Dec 15, 2022
Jan 5, 2023
Jun 16, 2022
Jun 16, 2022
Oct 25, 2022
Oct 3, 2022
Oct 3, 2022
Mar 8, 2023
Mar 8, 2023
Dec 5, 2022
Dec 5, 2022
Feb 15, 2023
Oct 17, 2022
Feb 10, 2023
Dec 15, 2022
Jun 16, 2022
Jun 16, 2022
Jun 16, 2022
Jun 16, 2022
Jan 5, 2023
Jan 5, 2023
Mar 2, 2023
Feb 10, 2023
Feb 15, 2023
Jun 16, 2022
Dec 12, 2022
Jun 16, 2022
Feb 6, 2023
Feb 10, 2023
Feb 15, 2023
Feb 15, 2023
Oct 3, 2022
Jun 16, 2022
Mar 6, 2023
Aug 18, 2022
Sep 21, 2022
Jun 16, 2022
Nov 29, 2022
Nov 29, 2022
Jan 31, 2023
Feb 6, 2023
Jun 16, 2022
Jun 16, 2022
Jun 16, 2022
Jun 16, 2022
Mar 2, 2023
Mar 2, 2023
Jun 16, 2022
Jun 16, 2022
Jun 16, 2022
Jun 16, 2022
Sep 9, 2022
Sep 9, 2022
Oct 5, 2022
Jun 16, 2022
Jan 20, 2023
Oct 25, 2022
Dec 12, 2022
Jul 27, 2022
Oct 25, 2022
Jun 16, 2022

README.md

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.

The technology started in 2009. A complete presentation is available here.

CP-SAT was described during the CPAIOR 2020 masterclass. The recording is available here.

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

Model

The optimization model description and related utilities:

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 automaton 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, 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.