OR-Tools  9.6
operations_research::sat Namespace Reference

Classes

class  AllDifferentConstraint
 
class  AllDifferentBoundsPropagator
 
class  CircuitPropagator
 
class  NoCyclePropagator
 
class  CircuitCoveringPropagator
 
class  SccGraph
 
class  SatClause
 
struct  ClauseInfo
 
class  LiteralWatchers
 
struct  BinaryClause
 
class  BinaryClauseManager
 
class  BinaryImplicationGraph
 
class  BooleanXorPropagator
 
class  GreaterThanAtLeastOneOfPropagator
 
class  BoolVar
 A Boolean variable. More...
 
class  IntVar
 An integer variable. More...
 
class  LinearExpr
 A dedicated container for linear expressions. More...
 
class  DoubleLinearExpr
 A dedicated container for linear expressions with double coefficients. More...
 
class  IntervalVar
 Represents a Interval variable. More...
 
class  Constraint
 A constraint. More...
 
class  CircuitConstraint
 Specialized circuit constraint. More...
 
class  MultipleCircuitConstraint
 Specialized circuit constraint. More...
 
class  TableConstraint
 Specialized assignment constraint. More...
 
class  ReservoirConstraint
 Specialized reservoir constraint. More...
 
class  AutomatonConstraint
 Specialized automaton constraint. More...
 
class  NoOverlap2DConstraint
 Specialized no_overlap2D constraint. More...
 
class  CumulativeConstraint
 Specialized cumulative constraint. More...
 
class  CpModelBuilder
 Wrapper class around the cp_model proto. More...
 
struct  Neighborhood
 
class  NeighborhoodGeneratorHelper
 
class  NeighborhoodGenerator
 
class  RelaxRandomVariablesGenerator
 
class  RelaxRandomConstraintsGenerator
 
class  VariableGraphNeighborhoodGenerator
 
class  ConstraintGraphNeighborhoodGenerator
 
class  RelaxObjectiveVariablesGenerator
 
class  RandomIntervalSchedulingNeighborhoodGenerator
 
class  RandomPrecedenceSchedulingNeighborhoodGenerator
 
class  SchedulingTimeWindowNeighborhoodGenerator
 
class  SchedulingResourceWindowsNeighborhoodGenerator
 
class  RoutingRandomNeighborhoodGenerator
 
class  RoutingPathNeighborhoodGenerator
 
class  RoutingFullPathNeighborhoodGenerator
 
class  RelaxationInducedNeighborhoodGenerator
 
struct  ObjectiveDefinition
 
class  CpModelMapping
 
class  CpModelPresolver
 
class  ModelCopy
 
struct  VarValue
 
class  CpModelView
 
struct  SolutionObservers
 
struct  IndexReferences
 
class  CumulativeEnergyConstraint
 
class  CumulativeIsAfterSubsetConstraint
 
struct  CutGenerator
 
struct  CutTerm
 
struct  CutData
 
class  CutDataBuilder
 
class  ImpliedBoundsProcessor
 
struct  FlowInfo
 
struct  SingleNodeFlow
 
class  FlowCoverCutHelper
 
struct  RoundingOptions
 
class  IntegerRoundingCutHelper
 
class  CoverCutHelper
 
class  SumOfAllDiffLowerBounder
 
class  NonOverlappingRectanglesDisjunctivePropagator
 
struct  Rectangle
 
struct  IndexedInterval
 
class  CapacityProfile
 
struct  DiophantineSolution
 
class  TaskSet
 
class  DisjunctiveOverloadChecker
 
class  DisjunctiveDetectablePrecedences
 
class  AllIntervalsHelper
 
class  CombinedDisjunctive
 
class  DisjunctiveNotLast
 
class  DisjunctiveEdgeFinding
 
class  DisjunctivePrecedences
 
class  DisjunctiveWithTwoItems
 
class  DratChecker
 
class  DratProofHandler
 
class  DratWriter
 
class  EncodingNode
 
class  FeasibilityPump
 
struct  ImpliedBoundEntry
 
class  ImpliedBounds
 
class  ProductDetector
 
class  CompactVectorVector
 
class  InclusionDetector
 
struct  IntegerLiteral
 
struct  AffineExpression
 
struct  IntegerDomains
 
struct  DebugSolution
 
struct  ValueLiteralPair
 
struct  LiteralValueValue
 
struct  DelayedRootLevelDeduction
 
class  IntegerEncoder
 
class  IntegerTrail
 
class  PropagatorInterface
 
class  RevIntRepository
 
class  RevIntegerValueRepository
 
class  GenericLiteralWatcher
 
class  IntegerSumLE
 
class  LevelZeroEquality
 
class  MinPropagator
 
class  LinMinPropagator
 
class  ProductPropagator
 
class  DivisionPropagator
 
class  FixedDivisionPropagator
 
class  FixedModuloPropagator
 
class  SquarePropagator
 
struct  BooleanOrIntegerLiteral
 
struct  SearchHeuristics
 
struct  LevelZeroCallbackHelper
 
struct  BooleanOrIntegerVariable
 
class  IntegerSearchHelper
 
class  ContinuousProber
 
class  IntervalsRepository
 
struct  TaskTime
 
class  SchedulingConstraintHelper
 
class  SchedulingDemandHelper
 
class  LbTreeSearch
 
struct  LinearConstraint
 
struct  LinearExpression
 
class  LinearConstraintBuilder
 
class  LinearConstraintManager
 
class  TopN
 
class  TopNCuts
 
struct  LinearProgrammingConstraintLpSolution
 
struct  LPSolveInfo
 
class  ScatteredIntegerVector
 
class  LinearProgrammingConstraint
 
class  LinearProgrammingDispatcher
 
class  LinearProgrammingConstraintCollection
 
class  CustomFifoQueue
 
class  EnforcementPropagator
 
class  LinearPropagator
 
struct  LinearRelaxation
 
class  HittingSetOptimizer
 
class  Model
 Class that owns everything related to a particular optimization model. More...
 
class  OpbReader
 
class  CoreBasedOptimizer
 
struct  LiteralWithCoeff
 
class  CanonicalBooleanLinearProblem
 
class  MutableUpperBoundedLinearConstraint
 
struct  PbConstraintsEnqueueHelper
 
class  UpperBoundedLinearConstraint
 
class  PbConstraints
 
class  VariableWithSameReasonIdentifier
 
class  PrecedencesPropagator
 
class  SavedLiteral
 
class  SavedVariable
 
class  PresolveContext
 
class  DomainDeductions
 
class  ActivityBoundHelper
 
class  ClauseWithOneMissingHasher
 
class  Prober
 
struct  ProbingOptions
 
class  PseudoCosts
 
class  RestartPolicy
 
struct  LPVariable
 
struct  LPVariables
 
struct  RINSNeighborhood
 
class  Literal
 
class  VariablesAssignment
 
struct  AssignmentInfo
 
struct  AssignmentType
 
class  Trail
 
class  SatPropagator
 
struct  LinearBooleanProblemWrapper
 
struct  CpModelProtoWrapper
 
class  SatCnfReader
 
class  SatDecisionPolicy
 
struct  PostsolveClauses
 
struct  SatPresolveOptions
 
class  Inprocessing
 
class  StampingSimplifier
 
class  BlockedClauseSimplifier
 
class  BoundedVariableElimination
 
class  SatSolver
 
class  SelectedMinPropagator
 
struct  EnergyEvent
 
struct  CachedIntervalData
 
struct  BaseEvent
 
struct  CtEvent
 
struct  PermutableEvent
 
class  PropagationGraph
 
class  SatPostsolver
 
class  SatPresolver
 
class  SubSolver
 
class  SynchronizationPoint
 
class  SymmetryPropagator
 
class  SharedSolutionRepository
 
class  SharedRelaxationSolutionRepository
 
class  SharedLPSolutionRepository
 
class  SharedIncompleteSolutionManager
 
struct  CpSolverResponseStatisticCallbacks
 
class  SharedResponseManager
 
class  SharedBoundsManager
 
class  SharedClausesManager
 
class  SharedStatistics
 
class  ThetaLambdaTree
 
class  ReservoirTimeTabling
 
class  TimeTablingPerTask
 
class  TimeTableEdgeFinding
 
class  ModelRandomGenerator
 
class  ModelSharedTimeLimit
 
class  MaxBoundedSubsetSum
 
class  BasicKnapsackSolver
 
class  IncrementalAverage
 
class  ExponentialMovingAverage
 
class  Percentile
 
class  VarDomination
 
class  DualBoundStrengthening
 
class  ZeroHalfCutHelper
 

Typedefs

using InlinedIntegerLiteralVector = absl::InlinedVector< IntegerLiteral, 2 >
 
using InlinedIntegerValueVector = absl::InlinedVector< std::pair< IntegerVariable, IntegerValue >, 2 >
 

Enumerations

enum  SatFormat { DIMACS , DRAT }
 
enum  EnforcementStatus { IS_FALSE = 0 , CANNOT_PROPAGATE = 1 , CAN_PROPAGATE = 2 , IS_ENFORCED = 3 }
 
enum  LogBehavior { DEFAULT_LOG , STDOUT_LOG }
 

Functions

void SolveFzWithCpModelProto (const fz::Model &fz_model, const fz::FlatzincSatParameters &p, const std::string &sat_params, SolverLogger *logger, SolverLogger *solution_logger)
 
std::function< void(Model *)> AllDifferentBinary (const std::vector< IntegerVariable > &vars)
 
std::function< void(Model *)> AllDifferentOnBounds (const std::vector< AffineExpression > &expressions)
 
std::function< void(Model *)> AllDifferentOnBounds (const std::vector< IntegerVariable > &vars)
 
std::function< void(Model *)> AllDifferentAC (const std::vector< IntegerVariable > &variables)
 
void ExtractAssignment (const LinearBooleanProblem &problem, const SatSolver &solver, std::vector< bool > *assignment)
 
absl::Status ValidateBooleanProblem (const LinearBooleanProblem &problem)
 
CpModelProto BooleanProblemToCpModelproto (const LinearBooleanProblem &problem)
 
void ChangeOptimizationDirection (LinearBooleanProblem *problem)
 
bool LoadBooleanProblem (const LinearBooleanProblem &problem, SatSolver *solver)
 
bool LoadAndConsumeBooleanProblem (LinearBooleanProblem *problem, SatSolver *solver)
 
void UseObjectiveForSatAssignmentPreference (const LinearBooleanProblem &problem, SatSolver *solver)
 
bool AddObjectiveUpperBound (const LinearBooleanProblem &problem, Coefficient upper_bound, SatSolver *solver)
 
bool AddObjectiveConstraint (const LinearBooleanProblem &problem, bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, SatSolver *solver)
 
Coefficient ComputeObjectiveValue (const LinearBooleanProblem &problem, const std::vector< bool > &assignment)
 
bool IsAssignmentValid (const LinearBooleanProblem &problem, const std::vector< bool > &assignment)
 
std::string LinearBooleanProblemToCnfString (const LinearBooleanProblem &problem)
 
void StoreAssignment (const VariablesAssignment &assignment, BooleanAssignment *output)
 
void ExtractSubproblem (const LinearBooleanProblem &problem, const std::vector< int > &constraint_indices, LinearBooleanProblem *subproblem)
 
template<typename Graph >
Graph * GenerateGraphForSymmetryDetection (const LinearBooleanProblem &problem, std::vector< int > *initial_equivalence_classes)
 
void MakeAllLiteralsPositive (LinearBooleanProblem *problem)
 
void FindLinearBooleanProblemSymmetries (const LinearBooleanProblem &problem, std::vector< std::unique_ptr< SparsePermutation >> *generators)
 
void ApplyLiteralMappingToBooleanProblem (const absl::StrongVector< LiteralIndex, LiteralIndex > &mapping, LinearBooleanProblem *problem)
 
void ProbeAndSimplifyProblem (SatPostsolver *postsolver, LinearBooleanProblem *problem)
 
double AddOffsetAndScaleObjectiveValue (const LinearBooleanProblem &problem, Coefficient v)
 
std::function< void(Model *)> ExactlyOnePerRowAndPerColumn (const std::vector< std::vector< Literal >> &graph)
 
std::function< void(Model *)> SubcircuitConstraint (int num_nodes, const std::vector< int > &tails, const std::vector< int > &heads, const std::vector< Literal > &literals, bool multiple_subcircuit_through_zero)
 
std::function< void(Model *)> CircuitCovering (const std::vector< std::vector< Literal >> &graph, const std::vector< int > &distinguished_nodes)
 
template<class IntContainer >
int ReindexArcs (IntContainer *tails, IntContainer *heads, absl::flat_hash_map< int, int > *mapping_output=nullptr)
 
std::vector< IntegerValue > ToIntegerValueVector (const std::vector< int64_t > &input)
 
std::function< void(Model *)> LiteralXorIs (const std::vector< Literal > &literals, bool value)
 
std::function< void(Model *)> GreaterThanAtLeastOneOf (IntegerVariable target_var, const absl::Span< const IntegerVariable > vars, const absl::Span< const IntegerValue > offsets, const absl::Span< const Literal > selectors)
 
std::function< void(Model *)> GreaterThanAtLeastOneOf (IntegerVariable target_var, const absl::Span< const IntegerVariable > vars, const absl::Span< const IntegerValue > offsets, const absl::Span< const Literal > selectors, const absl::Span< const Literal > enforcements)
 
std::function< void(Model *)> PartialIsOneOfVar (IntegerVariable target_var, const std::vector< IntegerVariable > &vars, const std::vector< Literal > &selectors)
 
BoolVar Not (BoolVar x)
 A convenient wrapper so we can write Not(x) instead of x.Not() which is sometimes clearer. More...
 
std::ostream & operator<< (std::ostream &os, const BoolVar &var)
 
std::string VarDebugString (const CpModelProto &proto, int index)
 
std::ostream & operator<< (std::ostream &os, const IntVar &var)
 
std::ostream & operator<< (std::ostream &os, const LinearExpr &e)
 
std::ostream & operator<< (std::ostream &os, const DoubleLinearExpr &e)
 
std::ostream & operator<< (std::ostream &os, const IntervalVar &var)
 
int64_t SolutionIntegerValue (const CpSolverResponse &r, const LinearExpr &expr)
 Evaluates the value of an linear expression in a solver response. More...
 
bool SolutionBooleanValue (const CpSolverResponse &r, BoolVar x)
 Evaluates the value of a Boolean literal in a solver response. More...
 
template<typename H >
AbslHashValue (H h, const IntVar &i)
 
template<typename H >
AbslHashValue (H h, const IntervalVar &i)
 
LinearExpr operator- (LinearExpr expr)
 
LinearExpr operator+ (const LinearExpr &lhs, const LinearExpr &rhs)
 
LinearExpr operator+ (LinearExpr &&lhs, const LinearExpr &rhs)
 
LinearExpr operator+ (const LinearExpr &lhs, LinearExpr &&rhs)
 
LinearExpr operator+ (LinearExpr &&lhs, LinearExpr &&rhs)
 
LinearExpr operator- (const LinearExpr &lhs, const LinearExpr &rhs)
 
LinearExpr operator- (LinearExpr &&lhs, const LinearExpr &rhs)
 
LinearExpr operator- (const LinearExpr &lhs, LinearExpr &&rhs)
 
LinearExpr operator- (LinearExpr &&lhs, LinearExpr &&rhs)
 
LinearExpr operator* (LinearExpr expr, int64_t factor)
 
LinearExpr operator* (int64_t factor, LinearExpr expr)
 
DoubleLinearExpr operator- (DoubleLinearExpr expr)
 
DoubleLinearExpr operator+ (const DoubleLinearExpr &lhs, const DoubleLinearExpr &rhs)
 
DoubleLinearExpr operator+ (DoubleLinearExpr &&lhs, const DoubleLinearExpr &rhs)
 
DoubleLinearExpr operator+ (const DoubleLinearExpr &lhs, DoubleLinearExpr &&rhs)
 
DoubleLinearExpr operator+ (DoubleLinearExpr &&lhs, DoubleLinearExpr &&rhs)
 
DoubleLinearExpr operator+ (DoubleLinearExpr expr, double rhs)
 
DoubleLinearExpr operator+ (double lhs, DoubleLinearExpr expr)
 
DoubleLinearExpr operator- (const DoubleLinearExpr &lhs, const DoubleLinearExpr &rhs)
 
DoubleLinearExpr operator- (DoubleLinearExpr &&lhs, const DoubleLinearExpr &rhs)
 
DoubleLinearExpr operator- (const DoubleLinearExpr &lhs, DoubleLinearExpr &&rhs)
 
DoubleLinearExpr operator- (DoubleLinearExpr &&lhs, DoubleLinearExpr &&rhs)
 
DoubleLinearExpr operator- (DoubleLinearExpr epxr, double rhs)
 
DoubleLinearExpr operator- (double lhs, DoubleLinearExpr expr)
 
DoubleLinearExpr operator* (DoubleLinearExpr expr, double factor)
 
DoubleLinearExpr operator* (double factor, DoubleLinearExpr expr)
 
bool PossibleIntegerOverflow (const CpModelProto &model, absl::Span< const int > vars, absl::Span< const int64_t > coeffs, int64_t offset)
 
std::string ValidateCpModel (const CpModelProto &model, bool after_presolve)
 
std::string ValidateInputCpModel (const SatParameters &params, const CpModelProto &model)
 
bool SolutionIsFeasible (const CpModelProto &model, absl::Span< const int64_t > variable_values, const CpModelProto *mapping_proto, const std::vector< int > *postsolve_mapping)
 
void PropagateAutomaton (const AutomatonConstraintProto &proto, const PresolveContext &context, std::vector< absl::flat_hash_set< int64_t >> *states, std::vector< absl::flat_hash_set< int64_t >> *labels)
 
void ExpandCpModel (PresolveContext *context)
 
void FinalExpansionForLinearConstraint (PresolveContext *context)
 
Neighborhood GenerateSchedulingNeighborhoodFromIntervalPrecedences (const absl::Span< const std::pair< int, int >> precedences, const CpSolverResponse &initial_solution, const NeighborhoodGeneratorHelper &helper)
 
Neighborhood GenerateSchedulingNeighborhoodFromRelaxedIntervals (const absl::Span< const int > intervals_to_relax, const CpSolverResponse &initial_solution, absl::BitGenRef random, const NeighborhoodGeneratorHelper &helper)
 
void LoadVariables (const CpModelProto &model_proto, bool view_all_booleans_as_integers, Model *m)
 
void LoadBooleanSymmetries (const CpModelProto &model_proto, Model *m)
 
void ExtractEncoding (const CpModelProto &model_proto, Model *m)
 
void ExtractElementEncoding (const CpModelProto &model_proto, Model *m)
 
void PropagateEncodingFromEquivalenceRelations (const CpModelProto &model_proto, Model *m)
 
void DetectOptionalVariables (const CpModelProto &model_proto, Model *m)
 
void AddFullEncodingFromSearchBranching (const CpModelProto &model_proto, Model *m)
 
void LoadBoolOrConstraint (const ConstraintProto &ct, Model *m)
 
void LoadBoolAndConstraint (const ConstraintProto &ct, Model *m)
 
void LoadAtMostOneConstraint (const ConstraintProto &ct, Model *m)
 
void LoadExactlyOneConstraint (const ConstraintProto &ct, Model *m)
 
void LoadBoolXorConstraint (const ConstraintProto &ct, Model *m)
 
void SplitAndLoadIntermediateConstraints (bool lb_required, bool ub_required, std::vector< IntegerVariable > *vars, std::vector< int64_t > *coeffs, Model *m)
 
void LoadLinearConstraint (const ConstraintProto &ct, Model *m)
 
void LoadAllDiffConstraint (const ConstraintProto &ct, Model *m)
 
void LoadIntProdConstraint (const ConstraintProto &ct, Model *m)
 
void LoadIntDivConstraint (const ConstraintProto &ct, Model *m)
 
void LoadIntModConstraint (const ConstraintProto &ct, Model *m)
 
void LoadLinMaxConstraint (const ConstraintProto &ct, Model *m)
 
void LoadNoOverlapConstraint (const ConstraintProto &ct, Model *m)
 
void LoadNoOverlap2dConstraint (const ConstraintProto &ct, Model *m)
 
void LoadCumulativeConstraint (const ConstraintProto &ct, Model *m)
 
void LoadReservoirConstraint (const ConstraintProto &ct, Model *m)
 
void LoadCircuitConstraint (const ConstraintProto &ct, Model *m)
 
void LoadRoutesConstraint (const ConstraintProto &ct, Model *m)
 
bool LoadConstraint (const ConstraintProto &ct, Model *m)
 
void LoadIntMinConstraint (const ConstraintProto &ct, Model *m)
 
void LoadIntMaxConstraint (const ConstraintProto &ct, Model *m)
 
void LoadCircuitCoveringConstraint (const ConstraintProto &ct, Model *m)
 
void EncodeObjectiveAsSingleVariable (CpModelProto *cp_model)
 
void PostsolveClause (const ConstraintProto &ct, std::vector< Domain > *domains)
 
void PostsolveExactlyOne (const ConstraintProto &ct, std::vector< Domain > *domains)
 
void SetEnforcementLiteralToFalse (const ConstraintProto &ct, std::vector< Domain > *domains)
 
void PostsolveLinear (const ConstraintProto &ct, std::vector< Domain > *domains)
 
void PostsolveLinMax (const ConstraintProto &ct, std::vector< Domain > *domains)
 
void PostsolveElement (const ConstraintProto &ct, std::vector< Domain > *domains)
 
void PostsolveResponse (const int64_t num_variables_in_original_model, const CpModelProto &mapping_proto, const std::vector< int > &postsolve_mapping, std::vector< int64_t > *solution)
 
bool ImportModelWithBasicPresolveIntoContext (const CpModelProto &in_model, PresolveContext *context)
 
void CopyEverythingExceptVariablesAndConstraintsFieldsIntoContext (const CpModelProto &in_model, PresolveContext *context)
 
CpSolverStatus PresolveCpModel (PresolveContext *context, std::vector< int > *postsolve_mapping)
 
void ApplyVariableMapping (const std::vector< int > &mapping, const PresolveContext &context)
 
std::vector< std::pair< int, int > > FindDuplicateConstraints (const CpModelProto &model_proto, bool ignore_enforcement)
 
const std::function< BooleanOrIntegerLiteral()> ConstructSearchStrategyInternal (const std::vector< DecisionStrategyProto > &strategies, Model *model)
 
std::function< BooleanOrIntegerLiteral()> ConstructUserSearchStrategy (const CpModelProto &cp_model_proto, Model *model)
 
std::function< BooleanOrIntegerLiteral()> ConstructFixedSearchStrategy (const CpModelProto &cp_model_proto, const std::vector< IntegerVariable > &variable_mapping, IntegerVariable objective_var, Model *model)
 
std::function< BooleanOrIntegerLiteral()> InstrumentSearchStrategy (const CpModelProto &cp_model_proto, const std::vector< IntegerVariable > &variable_mapping, const std::function< BooleanOrIntegerLiteral()> &instrumented_strategy, Model *model)
 
std::vector< SatParameters > GetDiverseSetOfParameters (const SatParameters &base_params, const CpModelProto &cp_model)
 
std::vector< SatParameters > GetFirstSolutionParams (const SatParameters &base_params, const CpModelProto &cp_model, int num_params_to_generate)
 
std::string CpSatSolverVersion ()
 Returns a string that describes the version of the solver. More...
 
std::string CpModelStats (const CpModelProto &model)
 Returns a string with some statistics on the given CpModelProto. More...
 
std::string CpSolverResponseStats (const CpSolverResponse &response, bool has_objective=true)
 Returns a string with some statistics on the solver response. More...
 
std::function< void(Model *)> NewFeasibleSolutionObserver (const std::function< void(const CpSolverResponse &response)> &observer)
 Creates a solution observer with the model with model.Add(NewFeasibleSolutionObserver([](response){...}));. More...
 
std::function< SatParameters(Model *)> NewSatParameters (const std::string &params)
 Creates parameters for the solver, which you can add to the model with. More...
 
std::function< SatParameters(Model *)> NewSatParameters (const sat::SatParameters &parameters)
 
CpSolverResponse SolveCpModel (const CpModelProto &model_proto, Model *model)
 Solves the given CpModelProto. More...
 
CpSolverResponse Solve (const CpModelProto &model_proto)
 Solves the given CpModelProto and returns an instance of CpSolverResponse. More...
 
CpSolverResponse SolveWithParameters (const CpModelProto &model_proto, const SatParameters &params)
 Solves the given CpModelProto with the given parameters. More...
 
CpSolverResponse SolveWithParameters (const CpModelProto &model_proto, const std::string &params)
 Solves the given CpModelProto with the given sat parameters as string in JSon format, and returns an instance of CpSolverResponse. More...
 
std::function< SatParameters(Model *)> NewSatParameters (const SatParameters &parameters)
 
void FindCpModelSymmetries (const SatParameters &params, const CpModelProto &problem, std::vector< std::unique_ptr< SparsePermutation >> *generators, double deterministic_limit, SolverLogger *logger)
 
void DetectAndAddSymmetryToProto (const SatParameters &params, CpModelProto *proto, SolverLogger *logger)
 
bool DetectAndExploitSymmetriesInPresolve (PresolveContext *context)
 
void SetToNegatedLinearExpression (const LinearExpressionProto &input_expr, LinearExpressionProto *output_negated_expr)
 
IndexReferences GetReferencesUsedByConstraint (const ConstraintProto &ct)
 
void ApplyToAllLiteralIndices (const std::function< void(int *)> &f, ConstraintProto *ct)
 
void ApplyToAllVariableIndices (const std::function< void(int *)> &f, ConstraintProto *ct)
 
void ApplyToAllIntervalIndices (const std::function< void(int *)> &f, ConstraintProto *ct)
 
std::string ConstraintCaseName (ConstraintProto::ConstraintCase constraint_case)
 
std::vector< int > UsedVariables (const ConstraintProto &ct)
 
std::vector< int > UsedIntervals (const ConstraintProto &ct)
 
int64_t ComputeInnerObjective (const CpObjectiveProto &objective, absl::Span< const int64_t > solution)
 
bool ExpressionContainsSingleRef (const LinearExpressionProto &expr)
 
bool ExpressionIsAffine (const LinearExpressionProto &expr)
 
int GetSingleRefFromExpression (const LinearExpressionProto &expr)
 
void AddLinearExpressionToLinearConstraint (const LinearExpressionProto &expr, int64_t coefficient, LinearConstraintProto *linear)
 
bool LinearExpressionProtosAreEqual (const LinearExpressionProto &a, const LinearExpressionProto &b, int64_t b_scaling)
 
uint64_t FingerprintExpression (const LinearExpressionProto &lin, uint64_t seed)
 
uint64_t FingerprintModel (const CpModelProto &model, uint64_t seed)
 
void SetupTextFormatPrinter (google::protobuf::TextFormat::Printer *printer)
 
int NegatedRef (int ref)
 
int PositiveRef (int ref)
 
bool RefIsPositive (int ref)
 
bool HasEnforcementLiteral (const ConstraintProto &ct)
 
int EnforcementLiteral (const ConstraintProto &ct)
 
template<typename ProtoWithDomain >
bool DomainInProtoContains (const ProtoWithDomain &proto, int64_t value)
 
template<typename ProtoWithDomain >
void FillDomainInProto (const Domain &domain, ProtoWithDomain *proto)
 
template<typename ProtoWithDomain >
Domain ReadDomainFromProto (const ProtoWithDomain &proto)
 
template<typename ProtoWithDomain >
std::vector< int64_t > AllValuesInDomain (const ProtoWithDomain &proto)
 
double ScaleObjectiveValue (const CpObjectiveProto &proto, int64_t value)
 
int64_t ScaleInnerObjectiveValue (const CpObjectiveProto &proto, int64_t value)
 
double UnscaleObjectiveValue (const CpObjectiveProto &proto, double value)
 
template<class T >
uint64_t FingerprintRepeatedField (const google::protobuf::RepeatedField< T > &sequence, uint64_t seed)
 
template<class T >
uint64_t FingerprintSingleField (const T &field, uint64_t seed)
 
template<class M >
bool WriteModelProtoToFile (const M &proto, absl::string_view filename)
 
std::function< void(Model *)> Cumulative (const std::vector< IntervalVariable > &vars, const std::vector< AffineExpression > &demands, AffineExpression capacity, SchedulingConstraintHelper *helper)
 
std::function< void(Model *)> CumulativeTimeDecomposition (const std::vector< IntervalVariable > &vars, const std::vector< AffineExpression > &demands, AffineExpression capacity, SchedulingConstraintHelper *helper)
 
std::function< void(Model *)> CumulativeUsingReservoir (const std::vector< IntervalVariable > &vars, const std::vector< AffineExpression > &demands, AffineExpression capacity, SchedulingConstraintHelper *helper)
 
void AddCumulativeOverloadChecker (AffineExpression capacity, SchedulingConstraintHelper *helper, SchedulingDemandHelper *demands, Model *model)
 
IntegerValue GetFactorT (IntegerValue rhs_remainder, IntegerValue divisor, IntegerValue max_magnitude)
 
std::function< IntegerValue(IntegerValue)> GetSuperAdditiveRoundingFunction (IntegerValue rhs_remainder, IntegerValue divisor, IntegerValue t, IntegerValue max_scaling)
 
CutGenerator CreatePositiveMultiplicationCutGenerator (AffineExpression z, AffineExpression x, AffineExpression y, int linearization_level, Model *model)
 
LinearConstraint ComputeHyperplanAboveSquare (AffineExpression x, AffineExpression square, IntegerValue x_lb, IntegerValue x_ub, Model *model)
 
LinearConstraint ComputeHyperplanBelowSquare (AffineExpression x, AffineExpression square, IntegerValue x_value, Model *model)
 
CutGenerator CreateSquareCutGenerator (AffineExpression y, AffineExpression x, int linearization_level, Model *model)
 
CutGenerator CreateAllDifferentCutGenerator (const std::vector< AffineExpression > &exprs, Model *model)
 
CutGenerator CreateLinMaxCutGenerator (const IntegerVariable target, const std::vector< LinearExpression > &exprs, const std::vector< IntegerVariable > &z_vars, Model *model)
 
bool BuildMaxAffineUpConstraint (const LinearExpression &target, IntegerVariable var, const std::vector< std::pair< IntegerValue, IntegerValue >> &affines, Model *model, LinearConstraintBuilder *builder)
 
CutGenerator CreateMaxAffineCutGenerator (LinearExpression target, IntegerVariable var, std::vector< std::pair< IntegerValue, IntegerValue >> affines, const std::string cut_name, Model *model)
 
CutGenerator CreateCliqueCutGenerator (const std::vector< IntegerVariable > &base_variables, Model *model)
 
void AddDiffnCumulativeRelationOnX (SchedulingConstraintHelper *x, SchedulingConstraintHelper *y, Model *model)
 
std::function< void(Model *)> NonOverlappingRectangles (const std::vector< IntervalVariable > &x, const std::vector< IntervalVariable > &y, bool is_strict)
 
std::vector< absl::Span< int > > GetOverlappingRectangleComponents (const std::vector< Rectangle > &rectangles, absl::Span< int > active_rectangles)
 
bool ReportEnergyConflict (Rectangle bounding_box, absl::Span< const int > boxes, SchedulingConstraintHelper *x, SchedulingConstraintHelper *y)
 
bool BoxesAreInEnergyConflict (const std::vector< Rectangle > &rectangles, const std::vector< IntegerValue > &energies, absl::Span< const int > boxes, Rectangle *conflict)
 
bool AnalyzeIntervals (bool transpose, absl::Span< const int > local_boxes, const std::vector< Rectangle > &rectangles, const std::vector< IntegerValue > &rectangle_energies, IntegerValue *x_threshold, IntegerValue *y_threshold, Rectangle *conflict)
 
absl::Span< int > FilterBoxesAndRandomize (const std::vector< Rectangle > &cached_rectangles, absl::Span< int > boxes, IntegerValue threshold_x, IntegerValue threshold_y, absl::BitGenRef random)
 
absl::Span< int > FilterBoxesThatAreTooLarge (const std::vector< Rectangle > &cached_rectangles, const std::vector< IntegerValue > &energies, absl::Span< int > boxes)
 
std::ostream & operator<< (std::ostream &out, const IndexedInterval &interval)
 
void ConstructOverlappingSets (bool already_sorted, std::vector< IndexedInterval > *intervals, std::vector< std::vector< int >> *result)
 
void GetOverlappingIntervalComponents (std::vector< IndexedInterval > *intervals, std::vector< std::vector< int >> *components)
 
std::vector< int > GetIntervalArticulationPoints (std::vector< IndexedInterval > *intervals)
 
void ReduceModuloBasis (const std::vector< std::vector< absl::int128 >> &basis, const int elements_to_consider, std::vector< absl::int128 > &v)
 
std::vector< int > GreedyFastDecreasingGcd (const absl::Span< const int64_t > coeffs)
 
DiophantineSolution SolveDiophantine (absl::Span< const int64_t > coeffs, int64_t rhs, absl::Span< const int64_t > var_lbs, absl::Span< const int64_t > var_ubs)
 
std::function< void(Model *)> Disjunctive (const std::vector< IntervalVariable > &intervals)
 
void AddDisjunctiveWithBooleanPrecedencesOnly (const std::vector< IntervalVariable > &intervals, Model *model)
 
void AddDisjunctiveWithBooleanPrecedences (const std::vector< IntervalVariable > &intervals, Model *model)
 
bool ContainsLiteral (absl::Span< const Literal > clause, Literal literal)
 
bool Resolve (absl::Span< const Literal > clause, absl::Span< const Literal > other_clause, Literal complementary_literal, VariablesAssignment *assignment, std::vector< Literal > *resolvent)
 
bool AddProblemClauses (const std::string &file_path, DratChecker *drat_checker)
 
bool AddInferedAndDeletedClauses (const std::string &file_path, DratChecker *drat_checker)
 
bool PrintClauses (const std::string &file_path, SatFormat format, const std::vector< std::vector< Literal >> &clauses, int num_variables)
 
 DEFINE_STRONG_INDEX_TYPE (ClauseIndex)
 
const ClauseIndex kNoClauseIndex (-1)
 
EncodingNode LazyMerge (EncodingNode *a, EncodingNode *b, SatSolver *solver)
 
void IncreaseNodeSize (EncodingNode *node, SatSolver *solver)
 
EncodingNode FullMerge (Coefficient upper_bound, EncodingNode *a, EncodingNode *b, SatSolver *solver)
 
EncodingNodeMergeAllNodesWithDeque (Coefficient upper_bound, const std::vector< EncodingNode * > &nodes, SatSolver *solver, std::deque< EncodingNode > *repository)
 
EncodingNodeLazyMergeAllNodeWithPQAndIncreaseLb (Coefficient weight, const std::vector< EncodingNode * > &nodes, SatSolver *solver, std::deque< EncodingNode > *repository)
 
std::vector< EncodingNode * > CreateInitialEncodingNodes (const std::vector< Literal > &literals, const std::vector< Coefficient > &coeffs, Coefficient *offset, std::deque< EncodingNode > *repository)
 
std::vector< EncodingNode * > CreateInitialEncodingNodes (const LinearObjective &objective_proto, Coefficient *offset, std::deque< EncodingNode > *repository)
 
std::vector< LiteralReduceNodesAndExtractAssumptions (Coefficient upper_bound, Coefficient stratified_lower_bound, Coefficient *lower_bound, std::vector< EncodingNode * > *nodes, SatSolver *solver)
 
Coefficient ComputeCoreMinWeight (const std::vector< EncodingNode * > &nodes, const std::vector< Literal > &core)
 
Coefficient MaxNodeWeightSmallerThan (const std::vector< EncodingNode * > &nodes, Coefficient upper_bound)
 
bool ProcessCore (const std::vector< Literal > &core, Coefficient min_weight, std::deque< EncodingNode > *repository, std::vector< EncodingNode * > *nodes, SatSolver *solver)
 
bool ProcessCoreWithAlternativeEncoding (const std::vector< Literal > &core, Coefficient min_weight, std::deque< EncodingNode > *repository, std::vector< EncodingNode * > *nodes, SatSolver *solver)
 
std::string EncodingStr (const std::vector< ValueLiteralPair > &enc)
 
std::vector< LiteralValueValueTryToReconcileEncodings (const AffineExpression &size2_affine, const AffineExpression &affine, const std::vector< ValueLiteralPair > &affine_var_encoding, bool put_affine_left_in_result, Model *model)
 
std::vector< LiteralValueValueTryToReconcileSize2Encodings (const AffineExpression &left, const AffineExpression &right, Model *model)
 
std::vector< LiteralValueValueTryToDecomposeProduct (const AffineExpression &left, const AffineExpression &right, Model *model)
 
bool DetectLinearEncodingOfProducts (const AffineExpression &left, const AffineExpression &right, Model *model, LinearConstraintBuilder *builder)
 
template<typename Storage >
 InclusionDetector (const Storage &storage) -> InclusionDetector< Storage >
 
std::vector< IntegerVariable > NegationOf (const std::vector< IntegerVariable > &vars)
 
std::ostream & operator<< (std::ostream &os, const ValueLiteralPair &p)
 
std::function< void(Model *)> ExcludeCurrentSolutionWithoutIgnoredVariableAndBacktrack ()
 
 DEFINE_STRONG_INT64_TYPE (IntegerValue)
 
constexpr IntegerValue kMaxIntegerValue (std::numeric_limits< IntegerValue::ValueType >::max() - 1)
 
constexpr IntegerValue kMinIntegerValue (-kMaxIntegerValue.value())
 
double ToDouble (IntegerValue value)
 
template<class IntType >
IntType IntTypeAbs (IntType t)
 
IntegerValue CeilRatio (IntegerValue dividend, IntegerValue positive_divisor)
 
IntegerValue FloorRatio (IntegerValue dividend, IntegerValue positive_divisor)
 
IntegerValue PositiveRemainder (IntegerValue dividend, IntegerValue positive_divisor)
 
bool AddProductTo (IntegerValue a, IntegerValue b, IntegerValue *result)
 
 DEFINE_STRONG_INDEX_TYPE (IntegerVariable)
 
const IntegerVariable kNoIntegerVariable (-1)
 
IntegerVariable NegationOf (IntegerVariable i)
 
bool VariableIsPositive (IntegerVariable i)
 
IntegerVariable PositiveVariable (IntegerVariable i)
 
 DEFINE_STRONG_INDEX_TYPE (PositiveOnlyIndex)
 
PositiveOnlyIndex GetPositiveOnlyIndex (IntegerVariable var)
 
std::string IntegerTermDebugString (IntegerVariable var, IntegerValue coeff)
 
std::ostream & operator<< (std::ostream &os, IntegerLiteral i_lit)
 
std::ostream & operator<< (std::ostream &os, absl::Span< const IntegerLiteral > literals)
 
std::function< BooleanVariable(Model *)> NewBooleanVariable ()
 
std::function< IntegerVariable(Model *)> ConstantIntegerVariable (int64_t value)
 
std::function< IntegerVariable(Model *)> NewIntegerVariable (int64_t lb, int64_t ub)
 
std::function< IntegerVariable(Model *)> NewIntegerVariable (const Domain &domain)
 
std::function< IntegerVariable(Model *)> NewIntegerVariableFromLiteral (Literal lit)
 
std::function< int64_t(const Model &)> LowerBound (IntegerVariable v)
 
std::function< int64_t(const Model &)> UpperBound (IntegerVariable v)
 
std::function< bool(const Model &)> IsFixed (IntegerVariable v)
 
std::function< int64_t(const Model &)> Value (IntegerVariable v)
 
std::function< void(Model *)> GreaterOrEqual (IntegerVariable v, int64_t lb)
 
std::function< void(Model *)> LowerOrEqual (IntegerVariable v, int64_t ub)
 
std::function< void(Model *)> Equality (IntegerVariable v, int64_t value)
 
std::function< void(Model *)> Implication (const std::vector< Literal > &enforcement_literals, IntegerLiteral i)
 
std::function< void(Model *)> ImpliesInInterval (Literal in_interval, IntegerVariable v, int64_t lb, int64_t ub)
 
std::function< std::vector< ValueLiteralPair >Model *)> FullyEncodeVariable (IntegerVariable var)
 
std::function< void(Model *)> IsOneOf (IntegerVariable var, const std::vector< Literal > &selectors, const std::vector< IntegerValue > &values)
 
template<typename VectorInt >
std::function< void(Model *)> WeightedSumLowerOrEqual (const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64_t upper_bound)
 
template<typename VectorInt >
std::function< void(Model *)> WeightedSumGreaterOrEqual (const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64_t lower_bound)
 
template<typename VectorInt >
std::function< void(Model *)> FixedWeightedSum (const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64_t value)
 
template<typename VectorInt >
std::function< void(Model *)> ConditionalWeightedSumLowerOrEqual (const std::vector< Literal > &enforcement_literals, const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64_t upper_bound)
 
template<typename VectorInt >
std::function< void(Model *)> ConditionalWeightedSumGreaterOrEqual (const std::vector< Literal > &enforcement_literals, const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64_t lower_bound)
 
template<typename VectorInt >
std::function< void(Model *)> WeightedSumLowerOrEqualReif (Literal is_le, const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64_t upper_bound)
 
template<typename VectorInt >
std::function< void(Model *)> WeightedSumGreaterOrEqualReif (Literal is_ge, const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64_t lower_bound)
 
void LoadLinearConstraint (const LinearConstraint &cst, Model *model)
 
void LoadConditionalLinearConstraint (const absl::Span< const Literal > enforcement_literals, const LinearConstraint &cst, Model *model)
 
void AddConditionalAffinePrecedence (const std::vector< Literal > &enforcement_literals, AffineExpression left, AffineExpression right, Model *model)
 
template<typename VectorInt >
std::function< void(Model *)> FixedWeightedSumReif (Literal is_eq, const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64_t value)
 
template<typename VectorInt >
std::function< void(Model *)> WeightedSumNotEqual (const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64_t value)
 
template<typename VectorInt >
std::function< IntegerVariable(Model *)> NewWeightedSum (const VectorInt &coefficients, const std::vector< IntegerVariable > &vars)
 
std::function< void(Model *)> IsEqualToMinOf (IntegerVariable min_var, const std::vector< IntegerVariable > &vars)
 
std::function< void(Model *)> IsEqualToMinOf (const LinearExpression &min_expr, const std::vector< LinearExpression > &exprs)
 
std::function< void(Model *)> IsEqualToMaxOf (IntegerVariable max_var, const std::vector< IntegerVariable > &vars)
 
template<class T >
void RegisterAndTransferOwnership (Model *model, T *ct)
 
std::function< void(Model *)> ProductConstraint (AffineExpression a, AffineExpression b, AffineExpression p)
 
std::function< void(Model *)> DivisionConstraint (AffineExpression num, AffineExpression denom, AffineExpression div)
 
std::function< void(Model *)> FixedDivisionConstraint (AffineExpression a, IntegerValue b, AffineExpression c)
 
std::function< void(Model *)> FixedModuloConstraint (AffineExpression a, IntegerValue b, AffineExpression c)
 
IntegerLiteral AtMinValue (IntegerVariable var, IntegerTrail *integer_trail)
 
IntegerLiteral ChooseBestObjectiveValue (IntegerVariable var, Model *model)
 
IntegerLiteral GreaterOrEqualToMiddleValue (IntegerVariable var, IntegerTrail *integer_trail)
 
IntegerLiteral SplitAroundGivenValue (IntegerVariable var, IntegerValue value, Model *model)
 
IntegerLiteral SplitAroundLpValue (IntegerVariable var, Model *model)
 
IntegerLiteral SplitUsingBestSolutionValueInRepository (IntegerVariable var, const SharedSolutionRepository< int64_t > &solution_repo, Model *model)
 
std::function< BooleanOrIntegerLiteral()> FirstUnassignedVarAtItsMinHeuristic (const std::vector< IntegerVariable > &vars, Model *model)
 
std::function< BooleanOrIntegerLiteral()> UnassignedVarWithLowestMinAtItsMinHeuristic (const std::vector< IntegerVariable > &vars, Model *model)
 
std::function< BooleanOrIntegerLiteral()> SequentialSearch (std::vector< std::function< BooleanOrIntegerLiteral()>> heuristics)
 
std::function< BooleanOrIntegerLiteral()> SequentialValueSelection (std::vector< std::function< IntegerLiteral(IntegerVariable)>> value_selection_heuristics, std::function< BooleanOrIntegerLiteral()> var_selection_heuristic, Model *model)
 
bool LinearizedPartIsLarge (Model *model)
 
std::function< BooleanOrIntegerLiteral()> IntegerValueSelectionHeuristic (std::function< BooleanOrIntegerLiteral()> var_selection_heuristic, Model *model)
 
std::function< BooleanOrIntegerLiteral()> SatSolverHeuristic (Model *model)
 
std::function< BooleanOrIntegerLiteral()> ShaveObjectiveLb (Model *model)
 
std::function< BooleanOrIntegerLiteral()> PseudoCost (Model *model)
 
std::function< BooleanOrIntegerLiteral()> SchedulingSearchHeuristic (Model *model)
 
std::function< BooleanOrIntegerLiteral()> RandomizeOnRestartHeuristic (Model *model)
 
std::function< BooleanOrIntegerLiteral()> FollowHint (const std::vector< BooleanOrIntegerVariable > &vars, const std::vector< IntegerValue > &values, Model *model)
 
std::function< bool()> RestartEveryKFailures (int k, SatSolver *solver)
 
std::function< bool()> SatSolverRestartPolicy (Model *model)
 
void ConfigureSearchHeuristics (Model *model)
 
std::vector< std::function< BooleanOrIntegerLiteral()> > CompleteHeuristics (const std::vector< std::function< BooleanOrIntegerLiteral()>> &incomplete_heuristics, const std::function< BooleanOrIntegerLiteral()> &completion_heuristic)
 
SatSolver::Status ResetAndSolveIntegerProblem (const std::vector< Literal > &assumptions, Model *model)
 
SatSolver::Status SolveIntegerProblemWithLazyEncoding (Model *model)
 
IntegerLiteral SplitDomainUsingBestSolutionValue (IntegerVariable var, Model *model)
 
SatSolver::Status ContinuousProbing (const std::vector< BooleanVariable > &bool_vars, const std::vector< IntegerVariable > &int_vars, Model *model)
 
IntegerValue ComputeEnergyMinInWindow (IntegerValue start_min, IntegerValue start_max, IntegerValue end_min, IntegerValue end_max, IntegerValue size_min, IntegerValue demand_min, const std::vector< LiteralValueValue > &filtered_energy, IntegerValue window_start, IntegerValue window_end)
 
 DEFINE_STRONG_INDEX_TYPE (IntervalVariable)
 
const IntervalVariable kNoIntervalVariable (-1)
 
std::function< IntegerVariable(const Model &)> StartVar (IntervalVariable v)
 
std::function< IntegerVariable(const Model &)> EndVar (IntervalVariable v)
 
std::function< IntegerVariable(const Model &)> SizeVar (IntervalVariable v)
 
std::function< int64_t(const Model &)> MinSize (IntervalVariable v)
 
std::function< int64_t(const Model &)> MaxSize (IntervalVariable v)
 
std::function< bool(const Model &)> IsOptional (IntervalVariable v)
 
std::function< Literal(const Model &)> IsPresentLiteral (IntervalVariable v)
 
std::function< IntervalVariable(Model *)> NewInterval (int64_t min_start, int64_t max_end, int64_t size)
 
std::function< IntervalVariable(Model *)> NewInterval (IntegerVariable start, IntegerVariable end, IntegerVariable size)
 
std::function< IntervalVariable(Model *)> NewIntervalWithVariableSize (int64_t min_start, int64_t max_end, int64_t min_size, int64_t max_size)
 
std::function< IntervalVariable(Model *)> NewOptionalInterval (int64_t min_start, int64_t max_end, int64_t size, Literal is_present)
 
std::function< IntervalVariable(Model *)> NewOptionalIntervalWithOptionalVariables (int64_t min_start, int64_t max_end, int64_t size, Literal is_present)
 
std::function< IntervalVariable(Model *)> NewOptionalInterval (IntegerVariable start, IntegerVariable end, IntegerVariable size, Literal is_present)
 
std::function< IntervalVariable(Model *)> NewOptionalIntervalWithVariableSize (int64_t min_start, int64_t max_end, int64_t min_size, int64_t max_size, Literal is_present)
 
std::function< void(Model *)> IntervalWithAlternatives (IntervalVariable parent, const std::vector< IntervalVariable > &members)
 
double ComputeActivity (const LinearConstraint &constraint, const absl::StrongVector< IntegerVariable, double > &values)
 
double ComputeL2Norm (const LinearConstraint &constraint)
 
IntegerValue ComputeInfinityNorm (const LinearConstraint &constraint)
 
double ScalarProduct (const LinearConstraint &constraint1, const LinearConstraint &constraint2)
 
void DivideByGCD (LinearConstraint *constraint)
 
void RemoveZeroTerms (LinearConstraint *constraint)
 
void MakeAllCoefficientsPositive (LinearConstraint *constraint)
 
void MakeAllVariablesPositive (LinearConstraint *constraint)
 
void CanonicalizeConstraint (LinearConstraint *ct)
 
bool NoDuplicateVariable (const LinearConstraint &ct)
 
LinearExpression CanonicalizeExpr (const LinearExpression &expr)
 
bool ValidateLinearConstraintForOverflow (const LinearConstraint &constraint, const IntegerTrail &integer_trail)
 
LinearExpression NegationOf (const LinearExpression &expr)
 
LinearExpression PositiveVarExpr (const LinearExpression &expr)
 
IntegerValue GetCoefficient (const IntegerVariable var, const LinearExpression &expr)
 
IntegerValue GetCoefficientOfPositiveVar (const IntegerVariable var, const LinearExpression &expr)
 
std::ostream & operator<< (std::ostream &os, const LinearConstraint &ct)
 
template<class ClassWithVarsAndCoeffs >
void CleanTermsAndFillConstraint (std::vector< std::pair< IntegerVariable, IntegerValue >> *terms, ClassWithVarsAndCoeffs *output)
 
bool PossibleOverflow (const IntegerTrail &integer_trail, const LinearConstraint &constraint)
 
void PreventOverflow (const IntegerTrail &integer_trail, LinearConstraint *constraint)
 
std::ostream & operator<< (std::ostream &os, const EnforcementStatus &e)
 
 DEFINE_STRONG_INDEX_TYPE (EnforcementId)
 
bool AppendFullEncodingRelaxation (IntegerVariable var, const Model &model, LinearRelaxation *relaxation)
 
void AppendRelaxationForEqualityEncoding (IntegerVariable var, const Model &model, LinearRelaxation *relaxation, int *num_tight, int *num_loose)
 
void AppendPartialGreaterThanEncodingRelaxation (IntegerVariable var, const Model &model, LinearRelaxation *relaxation)
 
void AppendBoolOrRelaxation (const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
 
void AppendBoolAndRelaxation (const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation, ActivityBoundHelper *activity_helper)
 
void AppendAtMostOneRelaxation (const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
 
void AppendExactlyOneRelaxation (const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
 
std::vector< LiteralCreateAlternativeLiteralsWithView (int num_literals, Model *model, LinearRelaxation *relaxation)
 
void AppendCircuitRelaxation (const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
 
void AppendRoutesRelaxation (const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
 
void AddCircuitCutGenerator (const ConstraintProto &ct, Model *m, LinearRelaxation *relaxation)
 
void AddRoutesCutGenerator (const ConstraintProto &ct, Model *m, LinearRelaxation *relaxation)
 
int DetectMakespan (const std::vector< IntervalVariable > &intervals, const std::vector< AffineExpression > &demands, const AffineExpression &capacity, Model *model)
 
void AppendNoOverlapRelaxationAndCutGenerator (const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
 
void AppendCumulativeRelaxationAndCutGenerator (const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
 
void AddCumulativeRelaxation (const AffineExpression &capacity, SchedulingConstraintHelper *helper, SchedulingDemandHelper *demands_helper, const std::optional< AffineExpression > &makespan, Model *model, LinearRelaxation *relaxation)
 
void AppendNoOverlap2dRelaxation (const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
 
void AppendLinMaxRelaxationPart1 (const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
 
void AppendMaxAffineRelaxation (const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
 
void AddMaxAffineCutGenerator (const ConstraintProto &ct, Model *model, LinearRelaxation *relaxation)
 
void AppendLinMaxRelaxationPart2 (IntegerVariable target, const std::vector< Literal > &alternative_literals, const std::vector< LinearExpression > &exprs, Model *model, LinearRelaxation *relaxation)
 
void AppendLinearConstraintRelaxation (const ConstraintProto &ct, bool linearize_enforced_constraints, Model *model, LinearRelaxation *relaxation, ActivityBoundHelper *activity_helper)
 
void TryToLinearizeConstraint (const CpModelProto &model_proto, const ConstraintProto &ct, int linearization_level, Model *model, LinearRelaxation *relaxation, ActivityBoundHelper *activity_helper)
 
void AddIntProdCutGenerator (const ConstraintProto &ct, int linearization_level, Model *m, LinearRelaxation *relaxation)
 
void AppendSquareRelaxation (const ConstraintProto &ct, Model *m, LinearRelaxation *relaxation)
 
void AddSquareCutGenerator (const ConstraintProto &ct, int linearization_level, Model *m, LinearRelaxation *relaxation)
 
void AddAllDiffRelaxationAndCutGenerator (const ConstraintProto &ct, int linearization_level, Model *m, LinearRelaxation *relaxation)
 
bool IntervalIsVariable (const IntervalVariable interval, IntervalsRepository *intervals_repository)
 
void AddCumulativeCutGenerator (const AffineExpression &capacity, SchedulingConstraintHelper *helper, SchedulingDemandHelper *demands_helper, const std::optional< AffineExpression > &makespan, Model *m, LinearRelaxation *relaxation)
 
void AddNoOverlapCutGenerator (SchedulingConstraintHelper *helper, const std::optional< AffineExpression > &makespan, Model *m, LinearRelaxation *relaxation)
 
void AddNoOverlap2dCutGenerator (const ConstraintProto &ct, Model *m, LinearRelaxation *relaxation)
 
void AddLinMaxCutGenerator (const ConstraintProto &ct, Model *m, LinearRelaxation *relaxation)
 
void AppendElementEncodingRelaxation (Model *m, LinearRelaxation *relaxation)
 
LinearRelaxation ComputeLinearRelaxation (const CpModelProto &model_proto, Model *m)
 
std::vector< double > ScaleContinuousVariables (double scaling, double max_bound, MPModelProto *mp_model)
 
int64_t FindRationalFactor (double x, int64_t limit, double tolerance)
 
bool MakeBoundsOfIntegerVariablesInteger (const SatParameters &params, MPModelProto *mp_model, SolverLogger *logger)
 
void RemoveNearZeroTerms (const SatParameters &params, MPModelProto *mp_model, SolverLogger *logger)
 
bool MPModelProtoValidationBeforeConversion (const SatParameters &params, const MPModelProto &mp_model, SolverLogger *logger)
 
std::vector< double > DetectImpliedIntegers (MPModelProto *mp_model, SolverLogger *logger)
 
double FindBestScalingAndComputeErrors (const std::vector< double > &coefficients, const std::vector< double > &lower_bounds, const std::vector< double > &upper_bounds, int64_t max_absolute_activity, double wanted_absolute_activity_precision, double *relative_coeff_error, double *scaled_sum_error)
 
bool ConvertMPModelProtoToCpModelProto (const SatParameters &params, const MPModelProto &mp_model, CpModelProto *cp_model, SolverLogger *logger)
 
bool ConvertCpModelProtoToMPModelProto (const CpModelProto &input, MPModelProto *output)
 
bool ScaleAndSetObjective (const SatParameters &params, const std::vector< std::pair< int, double >> &objective, double objective_offset, bool maximize, CpModelProto *cp_model, SolverLogger *logger)
 
bool ConvertBinaryMPModelProtoToBooleanProblem (const MPModelProto &mp_model, LinearBooleanProblem *problem)
 
void ConvertBooleanProblemToLinearProgram (const LinearBooleanProblem &problem, glop::LinearProgram *lp)
 
double ComputeTrueObjectiveLowerBound (const CpModelProto &model_proto_with_floating_point_objective, const CpObjectiveProto &integer_objective, const int64_t inner_integer_objective_lower_bound)
 
void MinimizeCoreWithPropagation (TimeLimit *limit, SatSolver *solver, std::vector< Literal > *core)
 
SatSolver::Status SolveWithFuMalik (LogBehavior log, const LinearBooleanProblem &problem, SatSolver *solver, std::vector< bool > *solution)
 
SatSolver::Status SolveWithWPM1 (LogBehavior log, const LinearBooleanProblem &problem, SatSolver *solver, std::vector< bool > *solution)
 
SatSolver::Status SolveWithRandomParameters (LogBehavior log, const LinearBooleanProblem &problem, int num_times, absl::BitGenRef random, SatSolver *solver, std::vector< bool > *solution)
 
SatSolver::Status SolveWithLinearScan (LogBehavior log, const LinearBooleanProblem &problem, SatSolver *solver, std::vector< bool > *solution)
 
SatSolver::Status SolveWithCardinalityEncoding (LogBehavior log, const LinearBooleanProblem &problem, SatSolver *solver, std::vector< bool > *solution)
 
SatSolver::Status SolveWithCardinalityEncodingAndCore (LogBehavior log, const LinearBooleanProblem &problem, SatSolver *solver, std::vector< bool > *solution)
 
SatSolver::Status MinimizeIntegerVariableWithLinearScanAndLazyEncoding (IntegerVariable objective_var, const std::function< void()> &feasible_solution_observer, Model *model)
 
void RestrictObjectiveDomainWithBinarySearch (IntegerVariable objective_var, const std::function< void()> &feasible_solution_observer, Model *model)
 
void PresolveBooleanLinearExpression (std::vector< Literal > *literals, std::vector< Coefficient > *coefficients, Coefficient *offset)
 
std::string ValidateParameters (const SatParameters &params)
 
bool ComputeBooleanLinearExpressionCanonicalForm (std::vector< LiteralWithCoeff > *cst, Coefficient *bound_shift, Coefficient *max_value)
 
bool ApplyLiteralMapping (const absl::StrongVector< LiteralIndex, LiteralIndex > &mapping, std::vector< LiteralWithCoeff > *cst, Coefficient *bound_shift, Coefficient *max_value)
 
bool BooleanLinearExpressionIsCanonical (const std::vector< LiteralWithCoeff > &cst)
 
void SimplifyCanonicalBooleanLinearConstraint (std::vector< LiteralWithCoeff > *cst, Coefficient *rhs)
 
Coefficient ComputeCanonicalRhs (Coefficient upper_bound, Coefficient bound_shift, Coefficient max_value)
 
Coefficient ComputeNegatedCanonicalRhs (Coefficient lower_bound, Coefficient bound_shift, Coefficient max_value)
 
 DEFINE_STRONG_INT64_TYPE (Coefficient)
 
const Coefficient kCoefficientMax (std::numeric_limits< Coefficient::ValueType >::max())
 
template<typename H >
AbslHashValue (H h, const LiteralWithCoeff &term)
 
std::ostream & operator<< (std::ostream &os, LiteralWithCoeff term)
 
std::function< void(Model *)> LowerOrEqual (IntegerVariable a, IntegerVariable b)
 
std::function< void(Model *)> LowerOrEqualWithOffset (IntegerVariable a, IntegerVariable b, int64_t offset)
 
std::function< void(Model *)> Sum2LowerOrEqual (IntegerVariable a, IntegerVariable b, int64_t ub)
 
std::function< void(Model *)> ConditionalSum2LowerOrEqual (IntegerVariable a, IntegerVariable b, int64_t ub, const std::vector< Literal > &enforcement_literals)
 
std::function< void(Model *)> Sum3LowerOrEqual (IntegerVariable a, IntegerVariable b, IntegerVariable c, int64_t ub)
 
std::function< void(Model *)> ConditionalSum3LowerOrEqual (IntegerVariable a, IntegerVariable b, IntegerVariable c, int64_t ub, const std::vector< Literal > &enforcement_literals)
 
std::function< void(Model *)> GreaterOrEqual (IntegerVariable a, IntegerVariable b)
 
std::function< void(Model *)> Equality (IntegerVariable a, IntegerVariable b)
 
std::function< void(Model *)> EqualityWithOffset (IntegerVariable a, IntegerVariable b, int64_t offset)
 
std::function< void(Model *)> ConditionalLowerOrEqualWithOffset (IntegerVariable a, IntegerVariable b, int64_t offset, Literal is_le)
 
bool LoadModelForProbing (PresolveContext *context, Model *local_model)
 
bool SubstituteVariable (int var, int64_t var_coeff_in_definition, const ConstraintProto &definition, ConstraintProto *ct)
 
bool ClauseIsEnforcementImpliesLiteral (absl::Span< const int > clause, absl::Span< const int > enforcement, int literal)
 
bool LookForTrivialSatSolution (double deterministic_time_limit, Model *model)
 
bool FailedLiteralProbingRound (ProbingOptions options, Model *model)
 
int SUniv (int i)
 
void RecordLPRelaxationValues (Model *model)
 
RINSNeighborhood GetRINSNeighborhood (const SharedResponseManager *response_manager, const SharedRelaxationSolutionRepository *relaxation_solutions, const SharedLPSolutionRepository *lp_solutions, SharedIncompleteSolutionManager *incomplete_solutions, absl::BitGenRef random)
 
void GenerateInterestingSubsets (int num_nodes, const std::vector< std::pair< int, int >> &arcs, int min_subset_size, int stop_at_num_components, std::vector< int > *subset_data, std::vector< absl::Span< const int >> *subsets)
 
void SeparateSubtourInequalities (int num_nodes, const std::vector< int > &tails, const std::vector< int > &heads, const std::vector< Literal > &literals, const absl::StrongVector< IntegerVariable, double > &lp_values, absl::Span< const int64_t > demands, int64_t capacity, LinearConstraintManager *manager, Model *model)
 
CutGenerator CreateStronglyConnectedGraphCutGenerator (int num_nodes, std::vector< int > tails, std::vector< int > heads, std::vector< Literal > literals, Model *model)
 
CutGenerator CreateCVRPCutGenerator (int num_nodes, std::vector< int > tails, std::vector< int > heads, std::vector< Literal > literals, std::vector< int64_t > demands, int64_t capacity, Model *model)
 
void SeparateFlowInequalities (int num_nodes, const std::vector< int > &tails, const std::vector< int > &heads, const std::vector< AffineExpression > &arc_capacities, std::function< void(const std::vector< bool > &in_subset, IntegerValue *min_incoming_flow, IntegerValue *min_outgoing_flow)> get_flows, const absl::StrongVector< IntegerVariable, double > &lp_values, LinearConstraintManager *manager, Model *model)
 
CutGenerator CreateFlowCutGenerator (int num_nodes, const std::vector< int > &tails, const std::vector< int > &heads, const std::vector< AffineExpression > &arc_capacities, std::function< void(const std::vector< bool > &in_subset, IntegerValue *min_incoming_flow, IntegerValue *min_outgoing_flow)> get_flows, Model *model)
 
 DEFINE_STRONG_INDEX_TYPE (BooleanVariable)
 
const BooleanVariable kNoBooleanVariable (-1)
 
 DEFINE_STRONG_INDEX_TYPE (LiteralIndex)
 
const LiteralIndex kNoLiteralIndex (-1)
 
const LiteralIndex kTrueLiteralIndex (-2)
 
const LiteralIndex kFalseLiteralIndex (-3)
 
std::ostream & operator<< (std::ostream &os, Literal literal)
 
std::ostream & operator<< (std::ostream &os, absl::Span< const Literal > literals)
 
std::string SatStatusString (SatSolver::Status status)
 
void MinimizeCore (SatSolver *solver, std::vector< Literal > *core)
 
std::function< void(Model *)> BooleanLinearConstraint (int64_t lower_bound, int64_t upper_bound, std::vector< LiteralWithCoeff > *cst)
 
std::function< void(Model *)> CardinalityConstraint (int64_t lower_bound, int64_t upper_bound, const std::vector< Literal > &literals)
 
std::function< void(Model *)> ExactlyOneConstraint (const std::vector< Literal > &literals)
 
std::function< void(Model *)> AtMostOneConstraint (const std::vector< Literal > &literals)
 
std::function< void(Model *)> ClauseConstraint (absl::Span< const Literal > literals)
 
std::function< void(Model *)> Implication (Literal a, Literal b)
 
std::function< void(Model *)> Equality (Literal a, Literal b)
 
std::function< void(Model *)> ReifiedBoolOr (const std::vector< Literal > &literals, Literal r)
 
std::function< void(Model *)> EnforcedClause (absl::Span< const Literal > enforcement_literals, absl::Span< const Literal > clause)
 
std::function< void(Model *)> ReifiedBoolAnd (const std::vector< Literal > &literals, Literal r)
 
std::function< void(Model *)> ReifiedBoolLe (Literal a, Literal b, Literal r)
 
std::function< int64_t(const Model &)> Value (Literal l)
 
std::function< int64_t(const Model &)> Value (BooleanVariable b)
 
std::function< void(Model *)> ExcludeCurrentSolutionAndBacktrack ()
 
std::ostream & operator<< (std::ostream &os, SatSolver::Status status)
 
std::function< void(Model *)> EqualMinOfSelectedVariables (Literal enforcement_literal, AffineExpression target, const std::vector< AffineExpression > &exprs, const std::vector< Literal > &selectors)
 
std::function< void(Model *)> EqualMaxOfSelectedVariables (Literal enforcement_literal, AffineExpression target, const std::vector< AffineExpression > &exprs, const std::vector< Literal > &selectors)
 
std::function< void(Model *)> SpanOfIntervals (IntervalVariable span, const std::vector< IntervalVariable > &intervals)
 
void GenerateCumulativeEnergeticCutsWithMakespanAndFixedCapacity (const std::string &cut_name, const absl::StrongVector< IntegerVariable, double > &lp_values, std::vector< EnergyEvent > events, IntegerValue capacity, AffineExpression makespan, TimeLimit *time_limit, Model *model, LinearConstraintManager *manager)
 
void GenerateCumulativeEnergeticCuts (const std::string &cut_name, const absl::StrongVector< IntegerVariable, double > &lp_values, std::vector< EnergyEvent > events, const AffineExpression capacity, TimeLimit *time_limit, Model *model, LinearConstraintManager *manager)
 
void AppendVariablesToCumulativeCut (const AffineExpression &capacity, SchedulingDemandHelper *demands_helper, Model *model, std::vector< IntegerVariable > *vars)
 
CutGenerator CreateCumulativeEnergyCutGenerator (SchedulingConstraintHelper *helper, SchedulingDemandHelper *demands_helper, const AffineExpression &capacity, const std::optional< AffineExpression > &makespan, Model *model)
 
CutGenerator CreateNoOverlapEnergyCutGenerator (SchedulingConstraintHelper *helper, const std::optional< AffineExpression > &makespan, Model *model)
 
void GenerateNoOverlap2dEnergyCut (const std::vector< std::vector< LiteralValueValue >> &energies, absl::Span< int > rectangles, const std::string &cut_name, const absl::StrongVector< IntegerVariable, double > &lp_values, Model *model, LinearConstraintManager *manager, SchedulingConstraintHelper *x_helper, SchedulingConstraintHelper *y_helper, SchedulingDemandHelper *y_demands_helper)
 
CutGenerator CreateNoOverlap2dEnergyCutGenerator (const std::vector< IntervalVariable > &x_intervals, const std::vector< IntervalVariable > &y_intervals, Model *model)
 
CutGenerator CreateCumulativeTimeTableCutGenerator (SchedulingConstraintHelper *helper, SchedulingDemandHelper *demands_helper, const AffineExpression &capacity, Model *model)
 
void GenerateCutsBetweenPairOfNonOverlappingTasks (const std::string &cut_name, const absl::StrongVector< IntegerVariable, double > &lp_values, std::vector< CachedIntervalData > events, IntegerValue capacity_max, Model *model, LinearConstraintManager *manager)
 
CutGenerator CreateCumulativePrecedenceCutGenerator (SchedulingConstraintHelper *helper, SchedulingDemandHelper *demands_helper, const AffineExpression &capacity, Model *model)
 
CutGenerator CreateNoOverlapPrecedenceCutGenerator (SchedulingConstraintHelper *helper, Model *model)
 
bool ComputeMinSumOfWeightedEndMins (std::vector< PermutableEvent > &events, IntegerValue capacity_max, IntegerValue &min_sum_of_end_mins, IntegerValue &min_sum_of_weighted_end_mins, IntegerValue unweighted_threshold, IntegerValue weighted_threshold)
 
void GenerateShortCompletionTimeCutsWithExactBound (const std::string &cut_name, const absl::StrongVector< IntegerVariable, double > &lp_values, std::vector< CtEvent > events, IntegerValue capacity_max, Model *model, LinearConstraintManager *manager)
 
void GenerateCompletionTimeCutsWithEnergy (const std::string &cut_name, const absl::StrongVector< IntegerVariable, double > &lp_values, std::vector< CtEvent > events, bool use_lifting, bool skip_low_sizes, Model *model, LinearConstraintManager *manager)
 
CutGenerator CreateNoOverlapCompletionTimeCutGenerator (SchedulingConstraintHelper *helper, Model *model)
 
CutGenerator CreateCumulativeCompletionTimeCutGenerator (SchedulingConstraintHelper *helper, SchedulingDemandHelper *demands_helper, const AffineExpression &capacity, Model *model)
 
CutGenerator CreateNoOverlap2dCompletionTimeCutGenerator (const std::vector< IntervalVariable > &x_intervals, const std::vector< IntervalVariable > &y_intervals, Model *model)
 
bool SimplifyClause (const std::vector< Literal > &a, std::vector< Literal > *b, LiteralIndex *opposite_literal, int64_t *num_inspected_literals)
 
LiteralIndex DifferAtGivenLiteral (const std::vector< Literal > &a, const std::vector< Literal > &b, Literal l)
 
bool ComputeResolvant (Literal x, const std::vector< Literal > &a, const std::vector< Literal > &b, std::vector< Literal > *out)
 
int ComputeResolvantSize (Literal x, const std::vector< Literal > &a, const std::vector< Literal > &b)
 
void ProbeAndFindEquivalentLiteral (SatSolver *solver, SatPostsolver *postsolver, DratProofHandler *drat_proof_handler, absl::StrongVector< LiteralIndex, LiteralIndex > *mapping)
 
SatSolver::Status SolveWithPresolve (std::unique_ptr< SatSolver > *solver, TimeLimit *time_limit, std::vector< bool > *solution, DratProofHandler *drat_proof_handler, SolverLogger *logger)
 
void SequentialLoop (const std::vector< std::unique_ptr< SubSolver >> &subsolvers)
 
void DeterministicLoop (const std::vector< std::unique_ptr< SubSolver >> &subsolvers, int num_threads, int batch_size)
 
void NonDeterministicLoop (const std::vector< std::unique_ptr< SubSolver >> &subsolvers, int num_threads)
 
std::vector< std::vector< int > > BasicOrbitopeExtraction (const std::vector< std::unique_ptr< SparsePermutation >> &generators)
 
std::vector< int > GetOrbits (int n, const std::vector< std::unique_ptr< SparsePermutation >> &generators)
 
std::vector< int > GetOrbitopeOrbits (int n, const std::vector< std::vector< int >> &orbitope)
 
void TransformToGeneratorOfStabilizer (int to_stabilize, std::vector< std::unique_ptr< SparsePermutation >> *generators)
 
void FillSolveStatsInResponse (Model *model, CpSolverResponse *response)
 
std::string ExtractSubSolverName (const std::string &improvement_info)
 
std::function< void(Model *)> LiteralTableConstraint (const std::vector< std::vector< Literal >> &literal_tuples, const std::vector< Literal > &line_literals)
 
template<typename IntegerType >
constexpr IntegerType IntegerTypeMinimumValue ()
 
template<>
constexpr IntegerValue IntegerTypeMinimumValue ()
 
void AddReservoirConstraint (std::vector< AffineExpression > times, std::vector< AffineExpression > deltas, std::vector< Literal > presences, int64_t min_level, int64_t max_level, Model *model)
 
std::string FormatCounter (int64_t num)
 
void RandomizeDecisionHeuristic (absl::BitGenRef random, SatParameters *parameters)
 
int64_t ModularInverse (int64_t x, int64_t m)
 
int64_t PositiveMod (int64_t x, int64_t m)
 
int64_t ProductWithModularInverse (int64_t coeff, int64_t mod, int64_t rhs)
 
bool SolveDiophantineEquationOfSizeTwo (int64_t &a, int64_t &b, int64_t &cte, int64_t &x0, int64_t &y0)
 
int64_t FloorSquareRoot (int64_t a)
 
int64_t CeilSquareRoot (int64_t a)
 
int64_t ClosestMultiple (int64_t value, int64_t base)
 
bool LinearInequalityCanBeReducedWithClosestMultiple (int64_t base, const std::vector< int64_t > &coeffs, const std::vector< int64_t > &lbs, const std::vector< int64_t > &ubs, int64_t rhs, int64_t *new_rhs)
 
int MoveOneUnprocessedLiteralLast (const absl::btree_set< LiteralIndex > &processed, int relevant_prefix_size, std::vector< Literal > *literals)
 
void CompressTuples (absl::Span< const int64_t > domain_sizes, std::vector< std::vector< int64_t >> *tuples)
 
std::vector< std::vector< absl::InlinedVector< int64_t, 2 > > > FullyCompressTuples (absl::Span< const int64_t > domain_sizes, std::vector< std::vector< int64_t >> *tuples)
 
int64_t SafeDoubleToInt64 (double value)
 
bool IsNegatableInt64 (absl::int128 x)
 
template<typename IntType , bool ceil>
IntType CeilOrFloorOfRatio (IntType numerator, IntType denominator)
 
template<typename IntType >
IntType CeilOfRatio (IntType numerator, IntType denominator)
 
template<typename IntType >
IntType FloorOfRatio (IntType numerator, IntType denominator)
 
void DetectDominanceRelations (const PresolveContext &context, VarDomination *var_domination, DualBoundStrengthening *dual_bound_strengthening)
 
bool ExploitDominanceRelations (const VarDomination &var_domination, PresolveContext *context)
 

Variables

constexpr uint64_t kDefaultFingerprintSeed = 0xa5b85c5e198ed849
 
constexpr int kObjectiveConstraint = -1
 
constexpr int kAffineRelationConstraint = -2
 
constexpr int kAssumptionsConstraint = -3
 
const int kUnsatTrailIndex = -1
 
constexpr int64_t kTableAnyValue = std::numeric_limits<int64_t>::min()
 

Typedef Documentation

◆ InlinedIntegerLiteralVector

using InlinedIntegerLiteralVector = absl::InlinedVector<IntegerLiteral, 2>

Definition at line 242 of file integer.h.

◆ InlinedIntegerValueVector

using InlinedIntegerValueVector = absl::InlinedVector<std::pair<IntegerVariable, IntegerValue>, 2>

Definition at line 243 of file integer.h.

Enumeration Type Documentation

◆ EnforcementStatus

Enumerator
IS_FALSE 
CANNOT_PROPAGATE 
CAN_PROPAGATE 
IS_ENFORCED 

Definition at line 77 of file linear_propagation.h.

◆ LogBehavior

Enumerator
DEFAULT_LOG 
STDOUT_LOG 

Definition at line 51 of file optimization.h.

◆ SatFormat

enum SatFormat
Enumerator
DIMACS 
DRAT 

Definition at line 330 of file drat_checker.h.

Function Documentation

◆ AbslHashValue() [1/3]

H operations_research::sat::AbslHashValue ( h,
const IntervalVar i 
)

Definition at line 515 of file cp_model.h.

◆ AbslHashValue() [2/3]

H operations_research::sat::AbslHashValue ( h,
const IntVar i 
)

Definition at line 510 of file cp_model.h.

◆ AbslHashValue() [3/3]

H operations_research::sat::AbslHashValue ( h,
const LiteralWithCoeff term 
)

Definition at line 65 of file pb_constraint.h.

◆ AddAllDiffRelaxationAndCutGenerator()

void AddAllDiffRelaxationAndCutGenerator ( const ConstraintProto &  ct,
int  linearization_level,
Model m,
LinearRelaxation relaxation 
)

Definition at line 1432 of file linear_relaxation.cc.

◆ AddCircuitCutGenerator()

void AddCircuitCutGenerator ( const ConstraintProto &  ct,
Model m,
LinearRelaxation relaxation 
)

Definition at line 601 of file linear_relaxation.cc.

◆ AddConditionalAffinePrecedence()

void operations_research::sat::AddConditionalAffinePrecedence ( const std::vector< Literal > &  enforcement_literals,
AffineExpression  left,
AffineExpression  right,
Model model 
)
inline

Definition at line 639 of file integer_expr.h.

◆ AddCumulativeCutGenerator()

void AddCumulativeCutGenerator ( const AffineExpression capacity,
SchedulingConstraintHelper helper,
SchedulingDemandHelper demands_helper,
const std::optional< AffineExpression > &  makespan,
Model m,
LinearRelaxation relaxation 
)

Definition at line 1498 of file linear_relaxation.cc.

◆ AddCumulativeOverloadChecker()

void AddCumulativeOverloadChecker ( AffineExpression  capacity,
SchedulingConstraintHelper helper,
SchedulingDemandHelper demands,
Model model 
)

Definition at line 32 of file cumulative_energy.cc.

◆ AddCumulativeRelaxation()

void AddCumulativeRelaxation ( const AffineExpression capacity,
SchedulingConstraintHelper helper,
SchedulingDemandHelper demands_helper,
const std::optional< AffineExpression > &  makespan,
Model model,
LinearRelaxation relaxation 
)

Definition at line 765 of file linear_relaxation.cc.

◆ AddDiffnCumulativeRelationOnX()

void AddDiffnCumulativeRelationOnX ( SchedulingConstraintHelper x,
SchedulingConstraintHelper y,
Model model 
)

Definition at line 87 of file sat/diffn.cc.

◆ AddDisjunctiveWithBooleanPrecedences()

void AddDisjunctiveWithBooleanPrecedences ( const std::vector< IntervalVariable > &  intervals,
Model model 
)

Definition at line 209 of file disjunctive.cc.

◆ AddDisjunctiveWithBooleanPrecedencesOnly()

void AddDisjunctiveWithBooleanPrecedencesOnly ( const std::vector< IntervalVariable > &  intervals,
Model model 
)

Definition at line 142 of file disjunctive.cc.

◆ AddFullEncodingFromSearchBranching()

void AddFullEncodingFromSearchBranching ( const CpModelProto &  model_proto,
Model m 
)

Definition at line 861 of file cp_model_loader.cc.

◆ AddInferedAndDeletedClauses()

bool AddInferedAndDeletedClauses ( const std::string &  file_path,
DratChecker drat_checker 
)

Definition at line 564 of file drat_checker.cc.

◆ AddIntProdCutGenerator()

void AddIntProdCutGenerator ( const ConstraintProto &  ct,
int  linearization_level,
Model m,
LinearRelaxation relaxation 
)

Definition at line 1330 of file linear_relaxation.cc.

◆ AddLinearExpressionToLinearConstraint()

void AddLinearExpressionToLinearConstraint ( const LinearExpressionProto &  expr,
int64_t  coefficient,
LinearConstraintProto *  linear 
)

Definition at line 548 of file cp_model_utils.cc.

◆ AddLinMaxCutGenerator()

void AddLinMaxCutGenerator ( const ConstraintProto &  ct,
Model m,
LinearRelaxation relaxation 
)

Definition at line 1600 of file linear_relaxation.cc.

◆ AddMaxAffineCutGenerator()

void operations_research::sat::AddMaxAffineCutGenerator ( const ConstraintProto &  ct,
Model model,
LinearRelaxation relaxation 
)

Definition at line 992 of file linear_relaxation.cc.

◆ AddNoOverlap2dCutGenerator()

void AddNoOverlap2dCutGenerator ( const ConstraintProto &  ct,
Model m,
LinearRelaxation relaxation 
)

Definition at line 1555 of file linear_relaxation.cc.

◆ AddNoOverlapCutGenerator()

void AddNoOverlapCutGenerator ( SchedulingConstraintHelper helper,
const std::optional< AffineExpression > &  makespan,
Model m,
LinearRelaxation relaxation 
)

Definition at line 1532 of file linear_relaxation.cc.

◆ AddObjectiveConstraint()

bool AddObjectiveConstraint ( const LinearBooleanProblem &  problem,
bool  use_lower_bound,
Coefficient  lower_bound,
bool  use_upper_bound,
Coefficient  upper_bound,
SatSolver solver 
)

Definition at line 348 of file boolean_problem.cc.

◆ AddObjectiveUpperBound()

bool AddObjectiveUpperBound ( const LinearBooleanProblem &  problem,
Coefficient  upper_bound,
SatSolver solver 
)

Definition at line 340 of file boolean_problem.cc.

◆ AddOffsetAndScaleObjectiveValue()

double operations_research::sat::AddOffsetAndScaleObjectiveValue ( const LinearBooleanProblem &  problem,
Coefficient  v 
)
inline

Definition at line 39 of file boolean_problem.h.

◆ AddProblemClauses()

bool AddProblemClauses ( const std::string &  file_path,
DratChecker drat_checker 
)

Definition at line 515 of file drat_checker.cc.

◆ AddProductTo()

bool operations_research::sat::AddProductTo ( IntegerValue  a,
IntegerValue  b,
IntegerValue *  result 
)
inline

Definition at line 121 of file integer.h.

◆ AddReservoirConstraint()

void AddReservoirConstraint ( std::vector< AffineExpression times,
std::vector< AffineExpression deltas,
std::vector< Literal presences,
int64_t  min_level,
int64_t  max_level,
Model model 
)

Definition at line 32 of file timetable.cc.

◆ AddRoutesCutGenerator()

void AddRoutesCutGenerator ( const ConstraintProto &  ct,
Model m,
LinearRelaxation relaxation 
)

Definition at line 615 of file linear_relaxation.cc.

◆ AddSquareCutGenerator()

void AddSquareCutGenerator ( const ConstraintProto &  ct,
int  linearization_level,
Model m,
LinearRelaxation relaxation 
)

Definition at line 1408 of file linear_relaxation.cc.

◆ AllDifferentAC()

std::function< void(Model *)> AllDifferentAC ( const std::vector< IntegerVariable > &  variables)

Definition at line 98 of file all_different.cc.

◆ AllDifferentBinary()

std::function< void(Model *)> AllDifferentBinary ( const std::vector< IntegerVariable > &  vars)

Definition at line 37 of file all_different.cc.

◆ AllDifferentOnBounds() [1/2]

std::function< void(Model *)> AllDifferentOnBounds ( const std::vector< AffineExpression > &  expressions)

Definition at line 71 of file all_different.cc.

◆ AllDifferentOnBounds() [2/2]

std::function< void(Model *)> AllDifferentOnBounds ( const std::vector< IntegerVariable > &  vars)

Definition at line 82 of file all_different.cc.

◆ AllValuesInDomain()

std::vector<int64_t> operations_research::sat::AllValuesInDomain ( const ProtoWithDomain &  proto)

Definition at line 125 of file cp_model_utils.h.

◆ AnalyzeIntervals()

bool AnalyzeIntervals ( bool  transpose,
absl::Span< const int >  local_boxes,
const std::vector< Rectangle > &  rectangles,
const std::vector< IntegerValue > &  rectangle_energies,
IntegerValue *  x_threshold,
IntegerValue *  y_threshold,
Rectangle *  conflict 
)

Definition at line 166 of file diffn_util.cc.

◆ AppendAtMostOneRelaxation()

void AppendAtMostOneRelaxation ( const ConstraintProto &  ct,
Model model,
LinearRelaxation relaxation 
)

Definition at line 436 of file linear_relaxation.cc.

◆ AppendBoolAndRelaxation()

void AppendBoolAndRelaxation ( const ConstraintProto &  ct,
Model model,
LinearRelaxation relaxation,
ActivityBoundHelper activity_helper 
)

Definition at line 367 of file linear_relaxation.cc.

◆ AppendBoolOrRelaxation()

void AppendBoolOrRelaxation ( const ConstraintProto &  ct,
Model model,
LinearRelaxation relaxation 
)

Definition at line 353 of file linear_relaxation.cc.

◆ AppendCircuitRelaxation()

void AppendCircuitRelaxation ( const ConstraintProto &  ct,
Model model,
LinearRelaxation relaxation 
)

Definition at line 507 of file linear_relaxation.cc.

◆ AppendCumulativeRelaxationAndCutGenerator()

void AppendCumulativeRelaxationAndCutGenerator ( const ConstraintProto &  ct,
Model model,
LinearRelaxation relaxation 
)

Definition at line 725 of file linear_relaxation.cc.

◆ AppendElementEncodingRelaxation()

void operations_research::sat::AppendElementEncodingRelaxation ( Model m,
LinearRelaxation relaxation 
)

Definition at line 1650 of file linear_relaxation.cc.

◆ AppendExactlyOneRelaxation()

void AppendExactlyOneRelaxation ( const ConstraintProto &  ct,
Model model,
LinearRelaxation relaxation 
)

Definition at line 445 of file linear_relaxation.cc.

◆ AppendFullEncodingRelaxation()

bool operations_research::sat::AppendFullEncodingRelaxation ( IntegerVariable  var,
const Model model,
LinearRelaxation relaxation 
)

Definition at line 56 of file linear_relaxation.cc.

◆ AppendLinearConstraintRelaxation()

void AppendLinearConstraintRelaxation ( const ConstraintProto &  ct,
bool  linearize_enforced_constraints,
Model model,
LinearRelaxation relaxation,
ActivityBoundHelper activity_helper 
)

Definition at line 1090 of file linear_relaxation.cc.

◆ AppendLinMaxRelaxationPart1()

void AppendLinMaxRelaxationPart1 ( const ConstraintProto &  ct,
Model model,
LinearRelaxation relaxation 
)

Definition at line 950 of file linear_relaxation.cc.

◆ AppendLinMaxRelaxationPart2()

void AppendLinMaxRelaxationPart2 ( IntegerVariable  target,
const std::vector< Literal > &  alternative_literals,
const std::vector< LinearExpression > &  exprs,
Model model,
LinearRelaxation relaxation 
)

Definition at line 1016 of file linear_relaxation.cc.

◆ AppendMaxAffineRelaxation()

void AppendMaxAffineRelaxation ( const ConstraintProto &  ct,
Model model,
LinearRelaxation relaxation 
)

Definition at line 972 of file linear_relaxation.cc.

◆ AppendNoOverlap2dRelaxation()

void operations_research::sat::AppendNoOverlap2dRelaxation ( const ConstraintProto &  ct,
Model model,
LinearRelaxation relaxation 
)

Definition at line 880 of file linear_relaxation.cc.

◆ AppendNoOverlapRelaxationAndCutGenerator()

void AppendNoOverlapRelaxationAndCutGenerator ( const ConstraintProto &  ct,
Model model,
LinearRelaxation relaxation 
)

Definition at line 691 of file linear_relaxation.cc.

◆ AppendPartialGreaterThanEncodingRelaxation()

void AppendPartialGreaterThanEncodingRelaxation ( IntegerVariable  var,
const Model model,
LinearRelaxation relaxation 
)

Definition at line 284 of file linear_relaxation.cc.

◆ AppendRelaxationForEqualityEncoding()

void AppendRelaxationForEqualityEncoding ( IntegerVariable  var,
const Model model,
LinearRelaxation relaxation,
int *  num_tight,
int *  num_loose 
)

Definition at line 178 of file linear_relaxation.cc.

◆ AppendRoutesRelaxation()

void AppendRoutesRelaxation ( const ConstraintProto &  ct,
Model model,
LinearRelaxation relaxation 
)

Definition at line 548 of file linear_relaxation.cc.

◆ AppendSquareRelaxation()

void AppendSquareRelaxation ( const ConstraintProto &  ct,
Model m,
LinearRelaxation relaxation 
)

Definition at line 1366 of file linear_relaxation.cc.

◆ AppendVariablesToCumulativeCut()

void operations_research::sat::AppendVariablesToCumulativeCut ( const AffineExpression capacity,
SchedulingDemandHelper demands_helper,
Model model,
std::vector< IntegerVariable > *  vars 
)

Definition at line 614 of file scheduling_cuts.cc.

◆ ApplyLiteralMapping()

bool ApplyLiteralMapping ( const absl::StrongVector< LiteralIndex, LiteralIndex > &  mapping,
std::vector< LiteralWithCoeff > *  cst,
Coefficient *  bound_shift,
Coefficient *  max_value 
)

Definition at line 115 of file pb_constraint.cc.

◆ ApplyLiteralMappingToBooleanProblem()

void ApplyLiteralMappingToBooleanProblem ( const absl::StrongVector< LiteralIndex, LiteralIndex > &  mapping,
LinearBooleanProblem *  problem 
)

Definition at line 756 of file boolean_problem.cc.

◆ ApplyToAllIntervalIndices()

void ApplyToAllIntervalIndices ( const std::function< void(int *)> &  f,
ConstraintProto *  ct 
)

Definition at line 329 of file cp_model_utils.cc.

◆ ApplyToAllLiteralIndices()

void ApplyToAllLiteralIndices ( const std::function< void(int *)> &  f,
ConstraintProto *  ct 
)

Definition at line 168 of file cp_model_utils.cc.

◆ ApplyToAllVariableIndices()

void ApplyToAllVariableIndices ( const std::function< void(int *)> &  f,
ConstraintProto *  ct 
)

Definition at line 231 of file cp_model_utils.cc.

◆ ApplyVariableMapping()

void ApplyVariableMapping ( const std::vector< int > &  mapping,
const PresolveContext context 
)

Definition at line 10922 of file cp_model_presolve.cc.

◆ AtMinValue()

IntegerLiteral AtMinValue ( IntegerVariable  var,
IntegerTrail integer_trail 
)

Definition at line 53 of file integer_search.cc.

◆ AtMostOneConstraint()

std::function<void(Model*)> operations_research::sat::AtMostOneConstraint ( const std::vector< Literal > &  literals)
inline

Definition at line 932 of file sat_solver.h.

◆ BasicOrbitopeExtraction()

std::vector< std::vector< int > > BasicOrbitopeExtraction ( const std::vector< std::unique_ptr< SparsePermutation >> &  generators)

Definition at line 28 of file symmetry_util.cc.

◆ BooleanLinearConstraint()

std::function<void(Model*)> operations_research::sat::BooleanLinearConstraint ( int64_t  lower_bound,
int64_t  upper_bound,
std::vector< LiteralWithCoeff > *  cst 
)
inline

Definition at line 893 of file sat_solver.h.

◆ BooleanLinearExpressionIsCanonical()

bool BooleanLinearExpressionIsCanonical ( const std::vector< LiteralWithCoeff > &  cst)

Definition at line 148 of file pb_constraint.cc.

◆ BooleanProblemToCpModelproto()

CpModelProto BooleanProblemToCpModelproto ( const LinearBooleanProblem &  problem)

Definition at line 163 of file boolean_problem.cc.

◆ BoxesAreInEnergyConflict()

bool BoxesAreInEnergyConflict ( const std::vector< Rectangle > &  rectangles,
const std::vector< IntegerValue > &  energies,
absl::Span< const int >  boxes,
Rectangle *  conflict 
)

Definition at line 99 of file diffn_util.cc.

◆ BuildMaxAffineUpConstraint()

bool BuildMaxAffineUpConstraint ( const LinearExpression target,
IntegerVariable  var,
const std::vector< std::pair< IntegerValue, IntegerValue >> &  affines,
Model model,
LinearConstraintBuilder builder 
)

Definition at line 2271 of file cuts.cc.

◆ CanonicalizeConstraint()

void CanonicalizeConstraint ( LinearConstraint ct)

Definition at line 365 of file linear_constraint.cc.

◆ CanonicalizeExpr()

LinearExpression CanonicalizeExpr ( const LinearExpression expr)

Definition at line 399 of file linear_constraint.cc.

◆ CardinalityConstraint()

std::function<void(Model*)> operations_research::sat::CardinalityConstraint ( int64_t  lower_bound,
int64_t  upper_bound,
const std::vector< Literal > &  literals 
)
inline

Definition at line 903 of file sat_solver.h.

◆ CeilOfRatio()

IntType operations_research::sat::CeilOfRatio ( IntType  numerator,
IntType  denominator 
)

Definition at line 428 of file sat/util.h.

◆ CeilOrFloorOfRatio()

IntType operations_research::sat::CeilOrFloorOfRatio ( IntType  numerator,
IntType  denominator 
)

Definition at line 408 of file sat/util.h.

◆ CeilRatio()

IntegerValue operations_research::sat::CeilRatio ( IntegerValue  dividend,
IntegerValue  positive_divisor 
)
inline

Definition at line 89 of file integer.h.

◆ CeilSquareRoot()

int64_t CeilSquareRoot ( int64_t  a)

Definition at line 220 of file sat/util.cc.

◆ ChangeOptimizationDirection()

void ChangeOptimizationDirection ( LinearBooleanProblem *  problem)

Definition at line 220 of file boolean_problem.cc.

◆ ChooseBestObjectiveValue()

IntegerLiteral ChooseBestObjectiveValue ( IntegerVariable  var,
Model model 
)

Definition at line 61 of file integer_search.cc.

◆ CircuitCovering()

std::function< void(Model *)> CircuitCovering ( const std::vector< std::vector< Literal >> &  graph,
const std::vector< int > &  distinguished_nodes 
)

Definition at line 673 of file circuit.cc.

◆ ClauseConstraint()

std::function<void(Model*)> operations_research::sat::ClauseConstraint ( absl::Span< const Literal literals)
inline

Definition at line 946 of file sat_solver.h.

◆ ClauseIsEnforcementImpliesLiteral()

bool operations_research::sat::ClauseIsEnforcementImpliesLiteral ( absl::Span< const int >  clause,
absl::Span< const int >  enforcement,
int  literal 
)
inline

Definition at line 247 of file presolve_util.h.

◆ CleanTermsAndFillConstraint()

void operations_research::sat::CleanTermsAndFillConstraint ( std::vector< std::pair< IntegerVariable, IntegerValue >> *  terms,
ClassWithVarsAndCoeffs *  output 
)

Definition at line 296 of file sat/linear_constraint.h.

◆ ClosestMultiple()

int64_t ClosestMultiple ( int64_t  value,
int64_t  base 
)

Definition at line 228 of file sat/util.cc.

◆ CompleteHeuristics()

std::vector< std::function< BooleanOrIntegerLiteral()> > CompleteHeuristics ( const std::vector< std::function< BooleanOrIntegerLiteral()>> &  incomplete_heuristics,
const std::function< BooleanOrIntegerLiteral()> &  completion_heuristic 
)

Definition at line 830 of file integer_search.cc.

◆ CompressTuples()

void CompressTuples ( absl::Span< const int64_t >  domain_sizes,
std::vector< std::vector< int64_t >> *  tuples 
)

Definition at line 386 of file sat/util.cc.

◆ ComputeActivity()

double ComputeActivity ( const LinearConstraint constraint,
const absl::StrongVector< IntegerVariable, double > &  values 
)

Definition at line 164 of file linear_constraint.cc.

◆ ComputeBooleanLinearExpressionCanonicalForm()

bool ComputeBooleanLinearExpressionCanonicalForm ( std::vector< LiteralWithCoeff > *  cst,
Coefficient *  bound_shift,
Coefficient *  max_value 
)

Definition at line 53 of file pb_constraint.cc.

◆ ComputeCanonicalRhs()

Coefficient ComputeCanonicalRhs ( Coefficient  upper_bound,
Coefficient  bound_shift,
Coefficient  max_value 
)

Definition at line 172 of file pb_constraint.cc.

◆ ComputeCoreMinWeight()

Coefficient ComputeCoreMinWeight ( const std::vector< EncodingNode * > &  nodes,
const std::vector< Literal > &  core 
)

Definition at line 525 of file encoding.cc.

◆ ComputeEnergyMinInWindow()

IntegerValue ComputeEnergyMinInWindow ( IntegerValue  start_min,
IntegerValue  start_max,
IntegerValue  end_min,
IntegerValue  end_max,
IntegerValue  size_min,
IntegerValue  demand_min,
const std::vector< LiteralValueValue > &  filtered_energy,
IntegerValue  window_start,
IntegerValue  window_end 
)

Definition at line 647 of file intervals.cc.

◆ ComputeHyperplanAboveSquare()

LinearConstraint ComputeHyperplanAboveSquare ( AffineExpression  x,
AffineExpression  square,
IntegerValue  x_lb,
IntegerValue  x_ub,
Model model 
)

Definition at line 1393 of file cuts.cc.

◆ ComputeHyperplanBelowSquare()

LinearConstraint ComputeHyperplanBelowSquare ( AffineExpression  x,
AffineExpression  square,
IntegerValue  x_value,
Model model 
)

Definition at line 1405 of file cuts.cc.

◆ ComputeInfinityNorm()

IntegerValue ComputeInfinityNorm ( const LinearConstraint constraint)

Definition at line 208 of file linear_constraint.cc.

◆ ComputeInnerObjective()

int64_t ComputeInnerObjective ( const CpObjectiveProto &  objective,
absl::Span< const int64_t >  solution 
)

Definition at line 519 of file cp_model_utils.cc.

◆ ComputeL2Norm()

double ComputeL2Norm ( const LinearConstraint constraint)

Definition at line 200 of file linear_constraint.cc.

◆ ComputeLinearRelaxation()

LinearRelaxation ComputeLinearRelaxation ( const CpModelProto &  model_proto,
Model m 
)

Definition at line 1697 of file linear_relaxation.cc.

◆ ComputeMinSumOfWeightedEndMins()

bool ComputeMinSumOfWeightedEndMins ( std::vector< PermutableEvent > &  events,
IntegerValue  capacity_max,
IntegerValue &  min_sum_of_end_mins,
IntegerValue &  min_sum_of_weighted_end_mins,
IntegerValue  unweighted_threshold,
IntegerValue  weighted_threshold 
)

Definition at line 1410 of file scheduling_cuts.cc.

◆ ComputeNegatedCanonicalRhs()

Coefficient ComputeNegatedCanonicalRhs ( Coefficient  lower_bound,
Coefficient  bound_shift,
Coefficient  max_value 
)

Definition at line 190 of file pb_constraint.cc.

◆ ComputeObjectiveValue()

Coefficient ComputeObjectiveValue ( const LinearBooleanProblem &  problem,
const std::vector< bool > &  assignment 
)

Definition at line 358 of file boolean_problem.cc.

◆ ComputeResolvant()

bool ComputeResolvant ( Literal  x,
const std::vector< Literal > &  a,
const std::vector< Literal > &  b,
std::vector< Literal > *  out 
)

Definition at line 1023 of file simplification.cc.

◆ ComputeResolvantSize()

int ComputeResolvantSize ( Literal  x,
const std::vector< Literal > &  a,
const std::vector< Literal > &  b 
)

Definition at line 1058 of file simplification.cc.

◆ ComputeTrueObjectiveLowerBound()

double ComputeTrueObjectiveLowerBound ( const CpModelProto &  model_proto_with_floating_point_objective,
const CpObjectiveProto &  integer_objective,
const int64_t  inner_integer_objective_lower_bound 
)

Definition at line 1615 of file sat/lp_utils.cc.

◆ ConditionalLowerOrEqualWithOffset()

std::function<void(Model*)> operations_research::sat::ConditionalLowerOrEqualWithOffset ( IntegerVariable  a,
IntegerVariable  b,
int64_t  offset,
Literal  is_le 
)
inline

Definition at line 461 of file precedences.h.

◆ ConditionalSum2LowerOrEqual()

std::function<void(Model*)> operations_research::sat::ConditionalSum2LowerOrEqual ( IntegerVariable  a,
IntegerVariable  b,
int64_t  ub,
const std::vector< Literal > &  enforcement_literals 
)
inline

Definition at line 401 of file precedences.h.

◆ ConditionalSum3LowerOrEqual()

std::function<void(Model*)> operations_research::sat::ConditionalSum3LowerOrEqual ( IntegerVariable  a,
IntegerVariable  b,
IntegerVariable  c,
int64_t  ub,
const std::vector< Literal > &  enforcement_literals 
)
inline

Definition at line 423 of file precedences.h.

◆ ConditionalWeightedSumGreaterOrEqual()

std::function<void(Model*)> operations_research::sat::ConditionalWeightedSumGreaterOrEqual ( const std::vector< Literal > &  enforcement_literals,
const std::vector< IntegerVariable > &  vars,
const VectorInt &  coefficients,
int64_t  lower_bound 
)
inline

Definition at line 547 of file integer_expr.h.

◆ ConditionalWeightedSumLowerOrEqual()

std::function<void(Model*)> operations_research::sat::ConditionalWeightedSumLowerOrEqual ( const std::vector< Literal > &  enforcement_literals,
const std::vector< IntegerVariable > &  vars,
const VectorInt &  coefficients,
int64_t  upper_bound 
)
inline

Definition at line 449 of file integer_expr.h.

◆ ConfigureSearchHeuristics()

void ConfigureSearchHeuristics ( Model model)

Definition at line 703 of file integer_search.cc.

◆ ConstantIntegerVariable()

std::function<IntegerVariable(Model*)> operations_research::sat::ConstantIntegerVariable ( int64_t  value)
inline

Definition at line 1726 of file integer.h.

◆ ConstraintCaseName()

std::string ConstraintCaseName ( ConstraintProto::ConstraintCase  constraint_case)

Definition at line 390 of file cp_model_utils.cc.

◆ ConstructFixedSearchStrategy()

std::function< BooleanOrIntegerLiteral()> ConstructFixedSearchStrategy ( const CpModelProto &  cp_model_proto,
const std::vector< IntegerVariable > &  variable_mapping,
IntegerVariable  objective_var,
Model model 
)

Definition at line 322 of file cp_model_search.cc.

◆ ConstructOverlappingSets()

void ConstructOverlappingSets ( bool  already_sorted,
std::vector< IndexedInterval > *  intervals,
std::vector< std::vector< int >> *  result 
)

Definition at line 361 of file diffn_util.cc.

◆ ConstructSearchStrategyInternal()

const std::function<BooleanOrIntegerLiteral()> operations_research::sat::ConstructSearchStrategyInternal ( const std::vector< DecisionStrategyProto > &  strategies,
Model model 
)

Definition at line 170 of file cp_model_search.cc.

◆ ConstructUserSearchStrategy()

std::function< BooleanOrIntegerLiteral()> ConstructUserSearchStrategy ( const CpModelProto &  cp_model_proto,
Model model 
)

Definition at line 313 of file cp_model_search.cc.

◆ ContainsLiteral()

bool ContainsLiteral ( absl::Span< const Literal clause,
Literal  literal 
)

Definition at line 474 of file drat_checker.cc.

◆ ContinuousProbing()

SatSolver::Status operations_research::sat::ContinuousProbing ( const std::vector< BooleanVariable > &  bool_vars,
const std::vector< IntegerVariable > &  int_vars,
Model model 
)

◆ ConvertBinaryMPModelProtoToBooleanProblem()

bool ConvertBinaryMPModelProtoToBooleanProblem ( const MPModelProto &  mp_model,
LinearBooleanProblem *  problem 
)

Definition at line 1372 of file sat/lp_utils.cc.

◆ ConvertBooleanProblemToLinearProgram()

void ConvertBooleanProblemToLinearProgram ( const LinearBooleanProblem &  problem,
glop::LinearProgram lp 
)

Definition at line 1551 of file sat/lp_utils.cc.

◆ ConvertCpModelProtoToMPModelProto()

bool ConvertCpModelProtoToMPModelProto ( const CpModelProto &  input,
MPModelProto *  output 
)

Definition at line 1067 of file sat/lp_utils.cc.

◆ ConvertMPModelProtoToCpModelProto()

bool ConvertMPModelProtoToCpModelProto ( const SatParameters &  params,
const MPModelProto &  mp_model,
CpModelProto *  cp_model,
SolverLogger logger 
)

Definition at line 852 of file sat/lp_utils.cc.

◆ CopyEverythingExceptVariablesAndConstraintsFieldsIntoContext()

void CopyEverythingExceptVariablesAndConstraintsFieldsIntoContext ( const CpModelProto &  in_model,
PresolveContext context 
)

Definition at line 10271 of file cp_model_presolve.cc.

◆ CpModelStats()

std::string CpModelStats ( const CpModelProto &  model_proto)

Returns a string with some statistics on the given CpModelProto.

Definition at line 205 of file cp_model_solver.cc.

◆ CpSatSolverVersion()

std::string CpSatSolverVersion ( )

Returns a string that describes the version of the solver.

Definition at line 170 of file cp_model_solver.cc.

◆ CpSolverResponseStats()

std::string CpSolverResponseStats ( const CpSolverResponse &  response,
bool  has_objective = true 
)

Returns a string with some statistics on the solver response.

If the second argument is false, we will just display NA for the objective value instead of zero. It is not really needed but it makes things a bit clearer to see that there is no objective.

Definition at line 560 of file cp_model_solver.cc.

◆ CreateAllDifferentCutGenerator()

CutGenerator CreateAllDifferentCutGenerator ( const std::vector< AffineExpression > &  exprs,
Model model 
)

Definition at line 2075 of file cuts.cc.

◆ CreateAlternativeLiteralsWithView()

std::vector< Literal > CreateAlternativeLiteralsWithView ( int  num_literals,
Model model,
LinearRelaxation relaxation 
)

Definition at line 466 of file linear_relaxation.cc.

◆ CreateCliqueCutGenerator()

CutGenerator CreateCliqueCutGenerator ( const std::vector< IntegerVariable > &  base_variables,
Model model 
)

Definition at line 2333 of file cuts.cc.

◆ CreateCumulativeCompletionTimeCutGenerator()

CutGenerator CreateCumulativeCompletionTimeCutGenerator ( SchedulingConstraintHelper helper,
SchedulingDemandHelper demands_helper,
const AffineExpression capacity,
Model model 
)

Definition at line 1792 of file scheduling_cuts.cc.

◆ CreateCumulativeEnergyCutGenerator()

CutGenerator CreateCumulativeEnergyCutGenerator ( SchedulingConstraintHelper helper,
SchedulingDemandHelper demands_helper,
const AffineExpression capacity,
const std::optional< AffineExpression > &  makespan,
Model model 
)

Definition at line 640 of file scheduling_cuts.cc.

◆ CreateCumulativePrecedenceCutGenerator()

CutGenerator CreateCumulativePrecedenceCutGenerator ( SchedulingConstraintHelper helper,
SchedulingDemandHelper demands_helper,
const AffineExpression capacity,
Model model 
)

Definition at line 1255 of file scheduling_cuts.cc.

◆ CreateCumulativeTimeTableCutGenerator()

CutGenerator CreateCumulativeTimeTableCutGenerator ( SchedulingConstraintHelper helper,
SchedulingDemandHelper demands_helper,
const AffineExpression capacity,
Model model 
)

Definition at line 1000 of file scheduling_cuts.cc.

◆ CreateCVRPCutGenerator()

CutGenerator CreateCVRPCutGenerator ( int  num_nodes,
std::vector< int >  tails,
std::vector< int >  heads,
std::vector< Literal literals,
std::vector< int64_t >  demands,
int64_t  capacity,
Model model 
)

Definition at line 440 of file routing_cuts.cc.

◆ CreateFlowCutGenerator()

CutGenerator CreateFlowCutGenerator ( int  num_nodes,
const std::vector< int > &  tails,
const std::vector< int > &  heads,
const std::vector< AffineExpression > &  arc_capacities,
std::function< void(const std::vector< bool > &in_subset, IntegerValue *min_incoming_flow, IntegerValue *min_outgoing_flow)>  get_flows,
Model model 
)

Definition at line 607 of file routing_cuts.cc.

◆ CreateInitialEncodingNodes() [1/2]

std::vector< EncodingNode * > CreateInitialEncodingNodes ( const LinearObjective &  objective_proto,
Coefficient *  offset,
std::deque< EncodingNode > *  repository 
)

Definition at line 434 of file encoding.cc.

◆ CreateInitialEncodingNodes() [2/2]

std::vector< EncodingNode * > CreateInitialEncodingNodes ( const std::vector< Literal > &  literals,
const std::vector< Coefficient > &  coeffs,
Coefficient *  offset,
std::deque< EncodingNode > *  repository 
)

Definition at line 409 of file encoding.cc.

◆ CreateLinMaxCutGenerator()

CutGenerator CreateLinMaxCutGenerator ( const IntegerVariable  target,
const std::vector< LinearExpression > &  exprs,
const std::vector< IntegerVariable > &  z_vars,
Model model 
)

Definition at line 2187 of file cuts.cc.

◆ CreateMaxAffineCutGenerator()

CutGenerator CreateMaxAffineCutGenerator ( LinearExpression  target,
IntegerVariable  var,
std::vector< std::pair< IntegerValue, IntegerValue >>  affines,
const std::string  cut_name,
Model model 
)

Definition at line 2309 of file cuts.cc.

◆ CreateNoOverlap2dCompletionTimeCutGenerator()

CutGenerator CreateNoOverlap2dCompletionTimeCutGenerator ( const std::vector< IntervalVariable > &  x_intervals,
const std::vector< IntervalVariable > &  y_intervals,
Model model 
)

Definition at line 1851 of file scheduling_cuts.cc.

◆ CreateNoOverlap2dEnergyCutGenerator()

CutGenerator CreateNoOverlap2dEnergyCutGenerator ( const std::vector< IntervalVariable > &  x_intervals,
const std::vector< IntervalVariable > &  y_intervals,
Model model 
)

Definition at line 914 of file scheduling_cuts.cc.

◆ CreateNoOverlapCompletionTimeCutGenerator()

CutGenerator CreateNoOverlapCompletionTimeCutGenerator ( SchedulingConstraintHelper helper,
Model model 
)

Definition at line 1742 of file scheduling_cuts.cc.

◆ CreateNoOverlapEnergyCutGenerator()

CutGenerator CreateNoOverlapEnergyCutGenerator ( SchedulingConstraintHelper helper,
const std::optional< AffineExpression > &  makespan,
Model model 
)

Definition at line 697 of file scheduling_cuts.cc.

◆ CreateNoOverlapPrecedenceCutGenerator()

CutGenerator CreateNoOverlapPrecedenceCutGenerator ( SchedulingConstraintHelper helper,
Model model 
)

Definition at line 1288 of file scheduling_cuts.cc.

◆ CreatePositiveMultiplicationCutGenerator()

CutGenerator CreatePositiveMultiplicationCutGenerator ( AffineExpression  z,
AffineExpression  x,
AffineExpression  y,
int  linearization_level,
Model model 
)

Definition at line 1295 of file cuts.cc.

◆ CreateSquareCutGenerator()

CutGenerator CreateSquareCutGenerator ( AffineExpression  y,
AffineExpression  x,
int  linearization_level,
Model model 
)

Definition at line 1417 of file cuts.cc.

◆ CreateStronglyConnectedGraphCutGenerator()

CutGenerator CreateStronglyConnectedGraphCutGenerator ( int  num_nodes,
std::vector< int >  tails,
std::vector< int >  heads,
std::vector< Literal literals,
Model model 
)

Definition at line 422 of file routing_cuts.cc.

◆ Cumulative()

std::function< void(Model *)> Cumulative ( const std::vector< IntervalVariable > &  vars,
const std::vector< AffineExpression > &  demands,
AffineExpression  capacity,
SchedulingConstraintHelper helper 
)

Definition at line 41 of file cumulative.cc.

◆ CumulativeTimeDecomposition()

std::function< void(Model *)> CumulativeTimeDecomposition ( const std::vector< IntervalVariable > &  vars,
const std::vector< AffineExpression > &  demands,
AffineExpression  capacity,
SchedulingConstraintHelper helper 
)

Definition at line 265 of file cumulative.cc.

◆ CumulativeUsingReservoir()

std::function< void(Model *)> CumulativeUsingReservoir ( const std::vector< IntervalVariable > &  vars,
const std::vector< AffineExpression > &  demands,
AffineExpression  capacity,
SchedulingConstraintHelper helper 
)

Definition at line 346 of file cumulative.cc.

◆ DEFINE_STRONG_INDEX_TYPE() [1/7]

operations_research::sat::DEFINE_STRONG_INDEX_TYPE ( BooleanVariable  )

◆ DEFINE_STRONG_INDEX_TYPE() [2/7]

operations_research::sat::DEFINE_STRONG_INDEX_TYPE ( ClauseIndex  )

◆ DEFINE_STRONG_INDEX_TYPE() [3/7]

operations_research::sat::DEFINE_STRONG_INDEX_TYPE ( EnforcementId  )

◆ DEFINE_STRONG_INDEX_TYPE() [4/7]

operations_research::sat::DEFINE_STRONG_INDEX_TYPE ( IntegerVariable  )

◆ DEFINE_STRONG_INDEX_TYPE() [5/7]

operations_research::sat::DEFINE_STRONG_INDEX_TYPE ( IntervalVariable  )

◆ DEFINE_STRONG_INDEX_TYPE() [6/7]

operations_research::sat::DEFINE_STRONG_INDEX_TYPE ( LiteralIndex  )

◆ DEFINE_STRONG_INDEX_TYPE() [7/7]

operations_research::sat::DEFINE_STRONG_INDEX_TYPE ( PositiveOnlyIndex  )

◆ DEFINE_STRONG_INT64_TYPE() [1/2]

operations_research::sat::DEFINE_STRONG_INT64_TYPE ( Coefficient  )

◆ DEFINE_STRONG_INT64_TYPE() [2/2]

operations_research::sat::DEFINE_STRONG_INT64_TYPE ( IntegerValue  )

◆ DetectAndAddSymmetryToProto()

void DetectAndAddSymmetryToProto ( const SatParameters &  params,
CpModelProto *  proto,
SolverLogger logger 
)

Definition at line 568 of file cp_model_symmetries.cc.

◆ DetectAndExploitSymmetriesInPresolve()

bool DetectAndExploitSymmetriesInPresolve ( PresolveContext context)

Definition at line 680 of file cp_model_symmetries.cc.

◆ DetectDominanceRelations()

void DetectDominanceRelations ( const PresolveContext context,
VarDomination var_domination,
DualBoundStrengthening dual_bound_strengthening 
)

Definition at line 1077 of file var_domination.cc.

◆ DetectImpliedIntegers()

std::vector< double > DetectImpliedIntegers ( MPModelProto *  mp_model,
SolverLogger logger 
)

Definition at line 413 of file sat/lp_utils.cc.

◆ DetectLinearEncodingOfProducts()

bool DetectLinearEncodingOfProducts ( const AffineExpression left,
const AffineExpression right,
Model model,
LinearConstraintBuilder builder 
)

Definition at line 440 of file implied_bounds.cc.

◆ DetectMakespan()

int operations_research::sat::DetectMakespan ( const std::vector< IntervalVariable > &  intervals,
const std::vector< AffineExpression > &  demands,
const AffineExpression capacity,
Model model 
)

Definition at line 656 of file linear_relaxation.cc.

◆ DetectOptionalVariables()

void DetectOptionalVariables ( const CpModelProto &  model_proto,
Model m 
)

Definition at line 782 of file cp_model_loader.cc.

◆ DeterministicLoop()

void DeterministicLoop ( const std::vector< std::unique_ptr< SubSolver >> &  subsolvers,
int  num_threads,
int  batch_size 
)

Definition at line 94 of file subsolver.cc.

◆ DifferAtGivenLiteral()

LiteralIndex DifferAtGivenLiteral ( const std::vector< Literal > &  a,
const std::vector< Literal > &  b,
Literal  l 
)

Definition at line 989 of file simplification.cc.

◆ Disjunctive()

std::function< void(Model *)> Disjunctive ( const std::vector< IntervalVariable > &  intervals)

Definition at line 39 of file disjunctive.cc.

◆ DivideByGCD()

void DivideByGCD ( LinearConstraint constraint)

Definition at line 255 of file linear_constraint.cc.

◆ DivisionConstraint()

std::function<void(Model*)> operations_research::sat::DivisionConstraint ( AffineExpression  num,
AffineExpression  denom,
AffineExpression  div 
)
inline

Definition at line 841 of file integer_expr.h.

◆ DomainInProtoContains()

bool operations_research::sat::DomainInProtoContains ( const ProtoWithDomain &  proto,
int64_t  value 
)

Definition at line 91 of file cp_model_utils.h.

◆ EncodeObjectiveAsSingleVariable()

void EncodeObjectiveAsSingleVariable ( CpModelProto *  cp_model)

Definition at line 28 of file cp_model_objective.cc.

◆ EncodingStr()

std::string operations_research::sat::EncodingStr ( const std::vector< ValueLiteralPair > &  enc)

Definition at line 242 of file implied_bounds.cc.

◆ EndVar()

std::function<IntegerVariable(const Model&)> operations_research::sat::EndVar ( IntervalVariable  v)
inline

Definition at line 789 of file intervals.h.

◆ EnforcedClause()

std::function<void(Model*)> operations_research::sat::EnforcedClause ( absl::Span< const Literal enforcement_literals,
absl::Span< const Literal clause 
)
inline

Definition at line 986 of file sat_solver.h.

◆ EnforcementLiteral()

int operations_research::sat::EnforcementLiteral ( const ConstraintProto &  ct)
inline

Definition at line 49 of file cp_model_utils.h.

◆ Equality() [1/3]

std::function<void(Model*)> operations_research::sat::Equality ( IntegerVariable  a,
IntegerVariable  b 
)
inline

Definition at line 442 of file precedences.h.

◆ Equality() [2/3]

std::function<void(Model*)> operations_research::sat::Equality ( IntegerVariable  v,
int64_t  value 
)
inline

Definition at line 1832 of file integer.h.

◆ Equality() [3/3]

std::function<void(Model*)> operations_research::sat::Equality ( Literal  a,
Literal  b 
)
inline

Definition at line 962 of file sat_solver.h.

◆ EqualityWithOffset()

std::function<void(Model*)> operations_research::sat::EqualityWithOffset ( IntegerVariable  a,
IntegerVariable  b,
int64_t  offset 
)
inline

Definition at line 451 of file precedences.h.

◆ EqualMaxOfSelectedVariables()

std::function< void(Model *)> EqualMaxOfSelectedVariables ( Literal  enforcement_literal,
AffineExpression  target,
const std::vector< AffineExpression > &  exprs,
const std::vector< Literal > &  selectors 
)

Definition at line 303 of file scheduling_constraints.cc.

◆ EqualMinOfSelectedVariables()

std::function< void(Model *)> EqualMinOfSelectedVariables ( Literal  enforcement_literal,
AffineExpression  target,
const std::vector< AffineExpression > &  exprs,
const std::vector< Literal > &  selectors 
)

Definition at line 279 of file scheduling_constraints.cc.

◆ ExactlyOneConstraint()

std::function<void(Model*)> operations_research::sat::ExactlyOneConstraint ( const std::vector< Literal > &  literals)
inline

Definition at line 918 of file sat_solver.h.

◆ ExactlyOnePerRowAndPerColumn()

std::function< void(Model *)> ExactlyOnePerRowAndPerColumn ( const std::vector< std::vector< Literal >> &  graph)

Definition at line 612 of file circuit.cc.

◆ ExcludeCurrentSolutionAndBacktrack()

std::function<void(Model*)> operations_research::sat::ExcludeCurrentSolutionAndBacktrack ( )
inline

Definition at line 1051 of file sat_solver.h.

◆ ExcludeCurrentSolutionWithoutIgnoredVariableAndBacktrack()

std::function< void(Model *)> ExcludeCurrentSolutionWithoutIgnoredVariableAndBacktrack ( )

Definition at line 2336 of file integer.cc.

◆ ExpandCpModel()

void ExpandCpModel ( PresolveContext context)

Definition at line 2028 of file cp_model_expand.cc.

◆ ExploitDominanceRelations()

bool ExploitDominanceRelations ( const VarDomination var_domination,
PresolveContext context 
)

Definition at line 1316 of file var_domination.cc.

◆ ExpressionContainsSingleRef()

bool ExpressionContainsSingleRef ( const LinearExpressionProto &  expr)

Definition at line 532 of file cp_model_utils.cc.

◆ ExpressionIsAffine()

bool ExpressionIsAffine ( const LinearExpressionProto &  expr)

Definition at line 537 of file cp_model_utils.cc.

◆ ExtractAssignment()

void ExtractAssignment ( const LinearBooleanProblem &  problem,
const SatSolver solver,
std::vector< bool > *  assignment 
)

Definition at line 62 of file boolean_problem.cc.

◆ ExtractElementEncoding()

void ExtractElementEncoding ( const CpModelProto &  model_proto,
Model m 
)

Definition at line 642 of file cp_model_loader.cc.

◆ ExtractEncoding()

void ExtractEncoding ( const CpModelProto &  model_proto,
Model m 
)

Definition at line 374 of file cp_model_loader.cc.

◆ ExtractSubproblem()

void ExtractSubproblem ( const LinearBooleanProblem &  problem,
const std::vector< int > &  constraint_indices,
LinearBooleanProblem *  subproblem 
)

Definition at line 498 of file boolean_problem.cc.

◆ ExtractSubSolverName()

std::string operations_research::sat::ExtractSubSolverName ( const std::string &  improvement_info)

Definition at line 722 of file synchronization.cc.

◆ FailedLiteralProbingRound()

bool FailedLiteralProbingRound ( ProbingOptions  options,
Model model 
)

Definition at line 375 of file probing.cc.

◆ FillDomainInProto()

void operations_research::sat::FillDomainInProto ( const Domain domain,
ProtoWithDomain *  proto 
)

Definition at line 100 of file cp_model_utils.h.

◆ FillSolveStatsInResponse()

void FillSolveStatsInResponse ( Model model,
CpSolverResponse *  response 
)

Definition at line 152 of file synchronization.cc.

◆ FilterBoxesAndRandomize()

absl::Span< int > FilterBoxesAndRandomize ( const std::vector< Rectangle > &  cached_rectangles,
absl::Span< int >  boxes,
IntegerValue  threshold_x,
IntegerValue  threshold_y,
absl::BitGenRef  random 
)

Definition at line 318 of file diffn_util.cc.

◆ FilterBoxesThatAreTooLarge()

absl::Span< int > FilterBoxesThatAreTooLarge ( const std::vector< Rectangle > &  cached_rectangles,
const std::vector< IntegerValue > &  energies,
absl::Span< int >  boxes 
)

Definition at line 334 of file diffn_util.cc.

◆ FinalExpansionForLinearConstraint()

void FinalExpansionForLinearConstraint ( PresolveContext context)

Definition at line 2177 of file cp_model_expand.cc.

◆ FindBestScalingAndComputeErrors()

double FindBestScalingAndComputeErrors ( const std::vector< double > &  coefficients,
const std::vector< double > &  lower_bounds,
const std::vector< double > &  upper_bounds,
int64_t  max_absolute_activity,
double  wanted_absolute_activity_precision,
double *  relative_coeff_error,
double *  scaled_sum_error 
)

Definition at line 800 of file sat/lp_utils.cc.

◆ FindCpModelSymmetries()

void FindCpModelSymmetries ( const SatParameters &  params,
const CpModelProto &  problem,
std::vector< std::unique_ptr< SparsePermutation >> *  generators,
double  deterministic_limit,
SolverLogger logger 
)

Definition at line 471 of file cp_model_symmetries.cc.

◆ FindDuplicateConstraints()

std::vector< std::pair< int, int > > FindDuplicateConstraints ( const CpModelProto &  model_proto,
bool  ignore_enforcement 
)

Definition at line 11063 of file cp_model_presolve.cc.

◆ FindLinearBooleanProblemSymmetries()

void FindLinearBooleanProblemSymmetries ( const LinearBooleanProblem &  problem,
std::vector< std::unique_ptr< SparsePermutation >> *  generators 
)

Definition at line 682 of file boolean_problem.cc.

◆ FindRationalFactor()

int64_t FindRationalFactor ( double  x,
int64_t  limit,
double  tolerance 
)

Definition at line 130 of file sat/lp_utils.cc.

◆ FingerprintExpression()

uint64_t FingerprintExpression ( const LinearExpressionProto &  lin,
uint64_t  seed 
)

Definition at line 580 of file cp_model_utils.cc.

◆ FingerprintModel()

uint64_t FingerprintModel ( const CpModelProto &  model,
uint64_t  seed 
)

Definition at line 591 of file cp_model_utils.cc.

◆ FingerprintRepeatedField()

uint64_t operations_research::sat::FingerprintRepeatedField ( const google::protobuf::RepeatedField< T > &  sequence,
uint64_t  seed 
)
inline

Definition at line 205 of file cp_model_utils.h.

◆ FingerprintSingleField()

uint64_t operations_research::sat::FingerprintSingleField ( const T &  field,
uint64_t  seed 
)
inline

Definition at line 213 of file cp_model_utils.h.

◆ FirstUnassignedVarAtItsMinHeuristic()

std::function< BooleanOrIntegerLiteral()> FirstUnassignedVarAtItsMinHeuristic ( const std::vector< IntegerVariable > &  vars,
Model model 
)

Definition at line 168 of file integer_search.cc.

◆ FixedDivisionConstraint()

std::function<void(Model*)> operations_research::sat::FixedDivisionConstraint ( AffineExpression  a,
IntegerValue  b,
AffineExpression  c 
)
inline

Definition at line 860 of file integer_expr.h.

◆ FixedModuloConstraint()

std::function<void(Model*)> operations_research::sat::FixedModuloConstraint ( AffineExpression  a,
IntegerValue  b,
AffineExpression  c 
)
inline

Definition at line 874 of file integer_expr.h.

◆ FixedWeightedSum()

std::function<void(Model*)> operations_research::sat::FixedWeightedSum ( const std::vector< IntegerVariable > &  vars,
const VectorInt &  coefficients,
int64_t  value 
)
inline

Definition at line 438 of file integer_expr.h.

◆ FixedWeightedSumReif()

std::function<void(Model*)> operations_research::sat::FixedWeightedSumReif ( Literal  is_eq,
const std::vector< IntegerVariable > &  vars,
const VectorInt &  coefficients,
int64_t  value 
)
inline

Definition at line 651 of file integer_expr.h.

◆ FloorOfRatio()

IntType operations_research::sat::FloorOfRatio ( IntType  numerator,
IntType  denominator 
)

Definition at line 433 of file sat/util.h.

◆ FloorRatio()

IntegerValue operations_research::sat::FloorRatio ( IntegerValue  dividend,
IntegerValue  positive_divisor 
)
inline

Definition at line 98 of file integer.h.

◆ FloorSquareRoot()

int64_t FloorSquareRoot ( int64_t  a)

Definition at line 211 of file sat/util.cc.

◆ FollowHint()

std::function< BooleanOrIntegerLiteral()> FollowHint ( const std::vector< BooleanOrIntegerVariable > &  vars,
const std::vector< IntegerValue > &  values,
Model model 
)

Definition at line 627 of file integer_search.cc.

◆ FormatCounter()

std::string FormatCounter ( int64_t  num)

Definition at line 48 of file sat/util.cc.

◆ FullMerge()

EncodingNode FullMerge ( Coefficient  upper_bound,
EncodingNode a,
EncodingNode b,
SatSolver solver 
)

Definition at line 308 of file encoding.cc.

◆ FullyCompressTuples()

std::vector< std::vector< absl::InlinedVector< int64_t, 2 > > > FullyCompressTuples ( absl::Span< const int64_t >  domain_sizes,
std::vector< std::vector< int64_t >> *  tuples 
)

Definition at line 783 of file sat/util.cc.

◆ FullyEncodeVariable()

std::function<std::vector<ValueLiteralPair>Model*)> operations_research::sat::FullyEncodeVariable ( IntegerVariable  var)
inline

Definition at line 1894 of file integer.h.

◆ GenerateCompletionTimeCutsWithEnergy()

void operations_research::sat::GenerateCompletionTimeCutsWithEnergy ( const std::string &  cut_name,
const absl::StrongVector< IntegerVariable, double > &  lp_values,
std::vector< CtEvent events,
bool  use_lifting,
bool  skip_low_sizes,
Model model,
LinearConstraintManager manager 
)

Definition at line 1588 of file scheduling_cuts.cc.

◆ GenerateCumulativeEnergeticCuts()

void operations_research::sat::GenerateCumulativeEnergeticCuts ( const std::string &  cut_name,
const absl::StrongVector< IntegerVariable, double > &  lp_values,
std::vector< EnergyEvent events,
const AffineExpression  capacity,
TimeLimit time_limit,
Model model,
LinearConstraintManager manager 
)

Definition at line 514 of file scheduling_cuts.cc.

◆ GenerateCumulativeEnergeticCutsWithMakespanAndFixedCapacity()

void operations_research::sat::GenerateCumulativeEnergeticCutsWithMakespanAndFixedCapacity ( const std::string &  cut_name,
const absl::StrongVector< IntegerVariable, double > &  lp_values,
std::vector< EnergyEvent events,
IntegerValue  capacity,
AffineExpression  makespan,
TimeLimit time_limit,
Model model,
LinearConstraintManager manager 
)

Definition at line 308 of file scheduling_cuts.cc.

◆ GenerateCutsBetweenPairOfNonOverlappingTasks()

void operations_research::sat::GenerateCutsBetweenPairOfNonOverlappingTasks ( const std::string &  cut_name,
const absl::StrongVector< IntegerVariable, double > &  lp_values,
std::vector< CachedIntervalData events,
IntegerValue  capacity_max,
Model model,
LinearConstraintManager manager 
)

Definition at line 1159 of file scheduling_cuts.cc.

◆ GenerateGraphForSymmetryDetection()

Graph* operations_research::sat::GenerateGraphForSymmetryDetection ( const LinearBooleanProblem &  problem,
std::vector< int > *  initial_equivalence_classes 
)

Definition at line 544 of file boolean_problem.cc.

◆ GenerateInterestingSubsets()

void GenerateInterestingSubsets ( int  num_nodes,
const std::vector< std::pair< int, int >> &  arcs,
int  min_subset_size,
int  stop_at_num_components,
std::vector< int > *  subset_data,
std::vector< absl::Span< const int >> *  subsets 
)

Definition at line 126 of file routing_cuts.cc.

◆ GenerateNoOverlap2dEnergyCut()

void operations_research::sat::GenerateNoOverlap2dEnergyCut ( const std::vector< std::vector< LiteralValueValue >> &  energies,
absl::Span< int >  rectangles,
const std::string &  cut_name,
const absl::StrongVector< IntegerVariable, double > &  lp_values,
Model model,
LinearConstraintManager manager,
SchedulingConstraintHelper x_helper,
SchedulingConstraintHelper y_helper,
SchedulingDemandHelper y_demands_helper 
)

Definition at line 744 of file scheduling_cuts.cc.

◆ GenerateSchedulingNeighborhoodFromIntervalPrecedences()

Neighborhood GenerateSchedulingNeighborhoodFromIntervalPrecedences ( const absl::Span< const std::pair< int, int >>  precedences,
const CpSolverResponse &  initial_solution,
const NeighborhoodGeneratorHelper helper 
)

Definition at line 1433 of file cp_model_lns.cc.

◆ GenerateSchedulingNeighborhoodFromRelaxedIntervals()

Neighborhood GenerateSchedulingNeighborhoodFromRelaxedIntervals ( const absl::Span< const int >  intervals_to_relax,
const CpSolverResponse &  initial_solution,
absl::BitGenRef  random,
const NeighborhoodGeneratorHelper helper 
)

Definition at line 1497 of file cp_model_lns.cc.

◆ GenerateShortCompletionTimeCutsWithExactBound()

void operations_research::sat::GenerateShortCompletionTimeCutsWithExactBound ( const std::string &  cut_name,
const absl::StrongVector< IntegerVariable, double > &  lp_values,
std::vector< CtEvent events,
IntegerValue  capacity_max,
Model model,
LinearConstraintManager manager 
)

Definition at line 1453 of file scheduling_cuts.cc.

◆ GetCoefficient()

IntegerValue GetCoefficient ( const IntegerVariable  var,
const LinearExpression expr 
)

Definition at line 465 of file linear_constraint.cc.

◆ GetCoefficientOfPositiveVar()

IntegerValue GetCoefficientOfPositiveVar ( const IntegerVariable  var,
const LinearExpression expr 
)

Definition at line 477 of file linear_constraint.cc.

◆ GetDiverseSetOfParameters()

std::vector< SatParameters > GetDiverseSetOfParameters ( const SatParameters &  base_params,
const CpModelProto &  cp_model 
)

Definition at line 439 of file cp_model_search.cc.

◆ GetFactorT()

IntegerValue GetFactorT ( IntegerValue  rhs_remainder,
IntegerValue  divisor,
IntegerValue  max_magnitude 
)

Definition at line 292 of file cuts.cc.

◆ GetFirstSolutionParams()

std::vector< SatParameters > GetFirstSolutionParams ( const SatParameters &  base_params,
const CpModelProto &  cp_model,
int  num_params_to_generate 
)

Definition at line 778 of file cp_model_search.cc.

◆ GetIntervalArticulationPoints()

std::vector< int > GetIntervalArticulationPoints ( std::vector< IndexedInterval > *  intervals)

Definition at line 443 of file diffn_util.cc.

◆ GetOrbitopeOrbits()

std::vector< int > GetOrbitopeOrbits ( int  n,
const std::vector< std::vector< int >> &  orbitope 
)

Definition at line 183 of file symmetry_util.cc.

◆ GetOrbits()

std::vector< int > GetOrbits ( int  n,
const std::vector< std::unique_ptr< SparsePermutation >> &  generators 
)

Definition at line 151 of file symmetry_util.cc.

◆ GetOverlappingIntervalComponents()

void GetOverlappingIntervalComponents ( std::vector< IndexedInterval > *  intervals,
std::vector< std::vector< int >> *  components 
)

Definition at line 410 of file diffn_util.cc.

◆ GetOverlappingRectangleComponents()

std::vector< absl::Span< int > > GetOverlappingRectangleComponents ( const std::vector< Rectangle > &  rectangles,
absl::Span< int >  active_rectangles 
)

Definition at line 41 of file diffn_util.cc.

◆ GetPositiveOnlyIndex()

PositiveOnlyIndex operations_research::sat::GetPositiveOnlyIndex ( IntegerVariable  var)
inline

Definition at line 155 of file integer.h.

◆ GetReferencesUsedByConstraint()

IndexReferences GetReferencesUsedByConstraint ( const ConstraintProto &  ct)

Definition at line 50 of file cp_model_utils.cc.

◆ GetRINSNeighborhood()

RINSNeighborhood GetRINSNeighborhood ( const SharedResponseManager response_manager,
const SharedRelaxationSolutionRepository relaxation_solutions,
const SharedLPSolutionRepository lp_solutions,
SharedIncompleteSolutionManager incomplete_solutions,
absl::BitGenRef  random 
)

Definition at line 107 of file rins.cc.

◆ GetSingleRefFromExpression()

int GetSingleRefFromExpression ( const LinearExpressionProto &  expr)

Definition at line 543 of file cp_model_utils.cc.

◆ GetSuperAdditiveRoundingFunction()

std::function< IntegerValue(IntegerValue)> GetSuperAdditiveRoundingFunction ( IntegerValue  rhs_remainder,
IntegerValue  divisor,
IntegerValue  t,
IntegerValue  max_scaling 
)

Definition at line 306 of file cuts.cc.

◆ GreaterOrEqual() [1/2]

std::function<void(Model*)> operations_research::sat::GreaterOrEqual ( IntegerVariable  a,
IntegerVariable  b 
)
inline

Definition at line 434 of file precedences.h.

◆ GreaterOrEqual() [2/2]

std::function<void(Model*)> operations_research::sat::GreaterOrEqual ( IntegerVariable  v,
int64_t  lb 
)
inline

Definition at line 1803 of file integer.h.

◆ GreaterOrEqualToMiddleValue()

IntegerLiteral GreaterOrEqualToMiddleValue ( IntegerVariable  var,
IntegerTrail integer_trail 
)

Definition at line 73 of file integer_search.cc.

◆ GreaterThanAtLeastOneOf() [1/2]

std::function<void(Model*)> operations_research::sat::GreaterThanAtLeastOneOf ( IntegerVariable  target_var,
const absl::Span< const IntegerVariable >  vars,
const absl::Span< const IntegerValue >  offsets,
const absl::Span< const Literal selectors 
)
inline

Definition at line 125 of file cp_constraints.h.

◆ GreaterThanAtLeastOneOf() [2/2]

std::function<void(Model*)> operations_research::sat::GreaterThanAtLeastOneOf ( IntegerVariable  target_var,
const absl::Span< const IntegerVariable >  vars,
const absl::Span< const IntegerValue >  offsets,
const absl::Span< const Literal selectors,
const absl::Span< const Literal enforcements 
)
inline

Definition at line 138 of file cp_constraints.h.

◆ GreedyFastDecreasingGcd()

std::vector< int > GreedyFastDecreasingGcd ( const absl::Span< const int64_t >  coeffs)

Definition at line 64 of file diophantine.cc.

◆ HasEnforcementLiteral()

bool operations_research::sat::HasEnforcementLiteral ( const ConstraintProto &  ct)
inline

Definition at line 46 of file cp_model_utils.h.

◆ Implication() [1/2]

std::function<void(Model*)> operations_research::sat::Implication ( const std::vector< Literal > &  enforcement_literals,
IntegerLiteral  i 
)
inline

Definition at line 1845 of file integer.h.

◆ Implication() [2/2]

std::function<void(Model*)> operations_research::sat::Implication ( Literal  a,
Literal  b 
)
inline

Definition at line 955 of file sat_solver.h.

◆ ImpliesInInterval()

std::function<void(Model*)> operations_research::sat::ImpliesInInterval ( Literal  in_interval,
IntegerVariable  v,
int64_t  lb,
int64_t  ub 
)
inline

Definition at line 1872 of file integer.h.

◆ ImportModelWithBasicPresolveIntoContext()

bool ImportModelWithBasicPresolveIntoContext ( const CpModelProto &  in_model,
PresolveContext context 
)

Definition at line 10259 of file cp_model_presolve.cc.

◆ InclusionDetector()

operations_research::sat::InclusionDetector ( const Storage &  storage) -> InclusionDetector< Storage >

◆ IncreaseNodeSize()

void IncreaseNodeSize ( EncodingNode node,
SatSolver solver 
)

Definition at line 209 of file encoding.cc.

◆ InstrumentSearchStrategy()

std::function< BooleanOrIntegerLiteral()> InstrumentSearchStrategy ( const CpModelProto &  cp_model_proto,
const std::vector< IntegerVariable > &  variable_mapping,
const std::function< BooleanOrIntegerLiteral()> &  instrumented_strategy,
Model model 
)

Definition at line 359 of file cp_model_search.cc.

◆ IntegerTermDebugString()

std::string operations_research::sat::IntegerTermDebugString ( IntegerVariable  var,
IntegerValue  coeff 
)
inline

Definition at line 159 of file integer.h.

◆ IntegerTypeMinimumValue() [1/2]

constexpr IntegerType operations_research::sat::IntegerTypeMinimumValue ( )
constexpr

Definition at line 95 of file theta_tree.h.

◆ IntegerTypeMinimumValue() [2/2]

constexpr IntegerValue operations_research::sat::IntegerTypeMinimumValue ( )
constexpr

Definition at line 99 of file theta_tree.h.

◆ IntegerValueSelectionHeuristic()

std::function< BooleanOrIntegerLiteral()> IntegerValueSelectionHeuristic ( std::function< BooleanOrIntegerLiteral()>  var_selection_heuristic,
Model model 
)

Definition at line 279 of file integer_search.cc.

◆ IntervalIsVariable()

bool operations_research::sat::IntervalIsVariable ( const IntervalVariable  interval,
IntervalsRepository intervals_repository 
)

Definition at line 1477 of file linear_relaxation.cc.

◆ IntervalWithAlternatives()

std::function<void(Model*)> operations_research::sat::IntervalWithAlternatives ( IntervalVariable  parent,
const std::vector< IntervalVariable > &  members 
)
inline

Definition at line 907 of file intervals.h.

◆ IntTypeAbs()

IntType operations_research::sat::IntTypeAbs ( IntType  t)
inline

Definition at line 85 of file integer.h.

◆ IsAssignmentValid()

bool IsAssignmentValid ( const LinearBooleanProblem &  problem,
const std::vector< bool > &  assignment 
)

Definition at line 372 of file boolean_problem.cc.

◆ IsEqualToMaxOf()

std::function<void(Model*)> operations_research::sat::IsEqualToMaxOf ( IntegerVariable  max_var,
const std::vector< IntegerVariable > &  vars 
)
inline

Definition at line 790 of file integer_expr.h.

◆ IsEqualToMinOf() [1/2]

std::function<void(Model*)> operations_research::sat::IsEqualToMinOf ( const LinearExpression min_expr,
const std::vector< LinearExpression > &  exprs 
)
inline

Definition at line 738 of file integer_expr.h.

◆ IsEqualToMinOf() [2/2]

std::function<void(Model*)> operations_research::sat::IsEqualToMinOf ( IntegerVariable  min_var,
const std::vector< IntegerVariable > &  vars 
)
inline

Definition at line 721 of file integer_expr.h.

◆ IsFixed()

std::function<bool(const Model&)> operations_research::sat::IsFixed ( IntegerVariable  v)
inline

Definition at line 1787 of file integer.h.

◆ IsNegatableInt64()

bool operations_research::sat::IsNegatableInt64 ( absl::int128  x)
inline

Definition at line 399 of file sat/util.h.

◆ IsOneOf()

std::function< void(Model *)> IsOneOf ( IntegerVariable  var,
const std::vector< Literal > &  selectors,
const std::vector< IntegerValue > &  values 
)

Definition at line 1505 of file integer_expr.cc.

◆ IsOptional()

std::function<bool(const Model&)> operations_research::sat::IsOptional ( IntervalVariable  v)
inline

Definition at line 814 of file intervals.h.

◆ IsPresentLiteral()

std::function<Literal(const Model&)> operations_research::sat::IsPresentLiteral ( IntervalVariable  v)
inline

Definition at line 820 of file intervals.h.

◆ kCoefficientMax()

const Coefficient operations_research::sat::kCoefficientMax ( std::numeric_limits< Coefficient::ValueType >  ::max())

◆ kFalseLiteralIndex()

const LiteralIndex operations_research::sat::kFalseLiteralIndex ( 3)

◆ kMaxIntegerValue()

constexpr IntegerValue operations_research::sat::kMaxIntegerValue ( std::numeric_limits< IntegerValue::ValueType >::max() -  1)
constexpr

◆ kMinIntegerValue()

constexpr IntegerValue operations_research::sat::kMinIntegerValue ( -kMaxIntegerValue.  value())
constexpr

◆ kNoBooleanVariable()

const BooleanVariable operations_research::sat::kNoBooleanVariable ( 1)

◆ kNoClauseIndex()

const ClauseIndex operations_research::sat::kNoClauseIndex ( 1)

◆ kNoIntegerVariable()

const IntegerVariable operations_research::sat::kNoIntegerVariable ( 1)

◆ kNoIntervalVariable()

const IntervalVariable operations_research::sat::kNoIntervalVariable ( 1)

◆ kNoLiteralIndex()

const LiteralIndex operations_research::sat::kNoLiteralIndex ( 1)

◆ kTrueLiteralIndex()

const LiteralIndex operations_research::sat::kTrueLiteralIndex ( 2)

◆ LazyMerge()

EncodingNode LazyMerge ( EncodingNode a,
EncodingNode b,
SatSolver solver 
)

Definition at line 199 of file encoding.cc.

◆ LazyMergeAllNodeWithPQAndIncreaseLb()

EncodingNode * LazyMergeAllNodeWithPQAndIncreaseLb ( Coefficient  weight,
const std::vector< EncodingNode * > &  nodes,
SatSolver solver,
std::deque< EncodingNode > *  repository 
)

Definition at line 381 of file encoding.cc.

◆ LinearBooleanProblemToCnfString()

std::string LinearBooleanProblemToCnfString ( const LinearBooleanProblem &  problem)

Definition at line 402 of file boolean_problem.cc.

◆ LinearExpressionProtosAreEqual()

bool LinearExpressionProtosAreEqual ( const LinearExpressionProto &  a,
const LinearExpressionProto &  b,
int64_t  b_scaling 
)

Definition at line 563 of file cp_model_utils.cc.

◆ LinearInequalityCanBeReducedWithClosestMultiple()

bool LinearInequalityCanBeReducedWithClosestMultiple ( int64_t  base,
const std::vector< int64_t > &  coeffs,
const std::vector< int64_t > &  lbs,
const std::vector< int64_t > &  ubs,
int64_t  rhs,
int64_t *  new_rhs 
)

Definition at line 235 of file sat/util.cc.

◆ LinearizedPartIsLarge()

bool LinearizedPartIsLarge ( Model model)

Definition at line 263 of file integer_search.cc.

◆ LiteralTableConstraint()

std::function< void(Model *)> LiteralTableConstraint ( const std::vector< std::vector< Literal >> &  literal_tuples,
const std::vector< Literal > &  line_literals 
)

Definition at line 30 of file sat/table.cc.

◆ LiteralXorIs()

std::function<void(Model*)> operations_research::sat::LiteralXorIs ( const std::vector< Literal > &  literals,
bool  value 
)
inline

Definition at line 113 of file cp_constraints.h.

◆ LoadAllDiffConstraint()

void LoadAllDiffConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1296 of file cp_model_loader.cc.

◆ LoadAndConsumeBooleanProblem()

bool LoadAndConsumeBooleanProblem ( LinearBooleanProblem *  problem,
SatSolver solver 
)

Definition at line 271 of file boolean_problem.cc.

◆ LoadAtMostOneConstraint()

void LoadAtMostOneConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 911 of file cp_model_loader.cc.

◆ LoadBoolAndConstraint()

void LoadBoolAndConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 897 of file cp_model_loader.cc.

◆ LoadBooleanProblem()

bool LoadBooleanProblem ( const LinearBooleanProblem &  problem,
SatSolver solver 
)

Definition at line 231 of file boolean_problem.cc.

◆ LoadBooleanSymmetries()

void LoadBooleanSymmetries ( const CpModelProto &  model_proto,
Model m 
)

Definition at line 284 of file cp_model_loader.cc.

◆ LoadBoolOrConstraint()

void LoadBoolOrConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 885 of file cp_model_loader.cc.

◆ LoadBoolXorConstraint()

void LoadBoolXorConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 927 of file cp_model_loader.cc.

◆ LoadCircuitConstraint()

void LoadCircuitConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1426 of file cp_model_loader.cc.

◆ LoadCircuitCoveringConstraint()

void operations_research::sat::LoadCircuitCoveringConstraint ( const ConstraintProto &  ct,
Model m 
)

◆ LoadConditionalLinearConstraint()

void operations_research::sat::LoadConditionalLinearConstraint ( const absl::Span< const Literal enforcement_literals,
const LinearConstraint cst,
Model model 
)
inline

Definition at line 606 of file integer_expr.h.

◆ LoadConstraint()

bool LoadConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1451 of file cp_model_loader.cc.

◆ LoadCumulativeConstraint()

void LoadCumulativeConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1395 of file cp_model_loader.cc.

◆ LoadExactlyOneConstraint()

void LoadExactlyOneConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 917 of file cp_model_loader.cc.

◆ LoadIntDivConstraint()

void LoadIntDivConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1320 of file cp_model_loader.cc.

◆ LoadIntMaxConstraint()

void operations_research::sat::LoadIntMaxConstraint ( const ConstraintProto &  ct,
Model m 
)

◆ LoadIntMinConstraint()

void operations_research::sat::LoadIntMinConstraint ( const ConstraintProto &  ct,
Model m 
)

◆ LoadIntModConstraint()

void operations_research::sat::LoadIntModConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1339 of file cp_model_loader.cc.

◆ LoadIntProdConstraint()

void LoadIntProdConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1303 of file cp_model_loader.cc.

◆ LoadLinearConstraint() [1/2]

void LoadLinearConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1087 of file cp_model_loader.cc.

◆ LoadLinearConstraint() [2/2]

void operations_research::sat::LoadLinearConstraint ( const LinearConstraint cst,
Model model 
)
inline

Definition at line 585 of file integer_expr.h.

◆ LoadLinMaxConstraint()

void LoadLinMaxConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1351 of file cp_model_loader.cc.

◆ LoadModelForProbing()

bool LoadModelForProbing ( PresolveContext context,
Model local_model 
)

Definition at line 2066 of file presolve_context.cc.

◆ LoadNoOverlap2dConstraint()

void LoadNoOverlap2dConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1383 of file cp_model_loader.cc.

◆ LoadNoOverlapConstraint()

void LoadNoOverlapConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1369 of file cp_model_loader.cc.

◆ LoadReservoirConstraint()

void LoadReservoirConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1405 of file cp_model_loader.cc.

◆ LoadRoutesConstraint()

void LoadRoutesConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1438 of file cp_model_loader.cc.

◆ LoadVariables()

void LoadVariables ( const CpModelProto &  model_proto,
bool  view_all_booleans_as_integers,
Model m 
)

Definition at line 121 of file cp_model_loader.cc.

◆ LookForTrivialSatSolution()

bool LookForTrivialSatSolution ( double  deterministic_time_limit,
Model model 
)

Definition at line 297 of file probing.cc.

◆ LowerBound()

std::function<int64_t(const Model&)> operations_research::sat::LowerBound ( IntegerVariable  v)
inline

Definition at line 1775 of file integer.h.

◆ LowerOrEqual() [1/2]

std::function<void(Model*)> operations_research::sat::LowerOrEqual ( IntegerVariable  a,
IntegerVariable  b 
)
inline

Definition at line 376 of file precedences.h.

◆ LowerOrEqual() [2/2]

std::function<void(Model*)> operations_research::sat::LowerOrEqual ( IntegerVariable  v,
int64_t  ub 
)
inline

Definition at line 1818 of file integer.h.

◆ LowerOrEqualWithOffset()

std::function<void(Model*)> operations_research::sat::LowerOrEqualWithOffset ( IntegerVariable  a,
IntegerVariable  b,
int64_t  offset 
)
inline

Definition at line 384 of file precedences.h.

◆ MakeAllCoefficientsPositive()

void MakeAllCoefficientsPositive ( LinearConstraint constraint)

Definition at line 282 of file linear_constraint.cc.

◆ MakeAllLiteralsPositive()

void MakeAllLiteralsPositive ( LinearBooleanProblem *  problem)

Definition at line 647 of file boolean_problem.cc.

◆ MakeAllVariablesPositive()

void MakeAllVariablesPositive ( LinearConstraint constraint)

Definition at line 293 of file linear_constraint.cc.

◆ MakeBoundsOfIntegerVariablesInteger()

bool MakeBoundsOfIntegerVariablesInteger ( const SatParameters &  params,
MPModelProto *  mp_model,
SolverLogger logger 
)

Definition at line 201 of file sat/lp_utils.cc.

◆ MaxNodeWeightSmallerThan()

Coefficient MaxNodeWeightSmallerThan ( const std::vector< EncodingNode * > &  nodes,
Coefficient  upper_bound 
)

Definition at line 539 of file encoding.cc.

◆ MaxSize()

std::function<int64_t(const Model&)> operations_research::sat::MaxSize ( IntervalVariable  v)
inline

Definition at line 808 of file intervals.h.

◆ MergeAllNodesWithDeque()

EncodingNode * MergeAllNodesWithDeque ( Coefficient  upper_bound,
const std::vector< EncodingNode * > &  nodes,
SatSolver solver,
std::deque< EncodingNode > *  repository 
)

Definition at line 359 of file encoding.cc.

◆ MinimizeCore()

void MinimizeCore ( SatSolver solver,
std::vector< Literal > *  core 
)

Definition at line 2666 of file sat_solver.cc.

◆ MinimizeCoreWithPropagation()

void MinimizeCoreWithPropagation ( TimeLimit limit,
SatSolver solver,
std::vector< Literal > *  core 
)

Definition at line 222 of file optimization.cc.

◆ MinimizeIntegerVariableWithLinearScanAndLazyEncoding()

SatSolver::Status MinimizeIntegerVariableWithLinearScanAndLazyEncoding ( IntegerVariable  objective_var,
const std::function< void()> &  feasible_solution_observer,
Model model 
)

Definition at line 1074 of file optimization.cc.

◆ MinSize()

std::function<int64_t(const Model&)> operations_research::sat::MinSize ( IntervalVariable  v)
inline

Definition at line 802 of file intervals.h.

◆ ModularInverse()

int64_t ModularInverse ( int64_t  x,
int64_t  m 
)

Definition at line 104 of file sat/util.cc.

◆ MoveOneUnprocessedLiteralLast()

int MoveOneUnprocessedLiteralLast ( const absl::btree_set< LiteralIndex > &  processed,
int  relevant_prefix_size,
std::vector< Literal > *  literals 
)

Definition at line 299 of file sat/util.cc.

◆ MPModelProtoValidationBeforeConversion()

bool MPModelProtoValidationBeforeConversion ( const SatParameters &  params,
const MPModelProto &  mp_model,
SolverLogger logger 
)

Definition at line 349 of file sat/lp_utils.cc.

◆ NegatedRef()

int operations_research::sat::NegatedRef ( int  ref)
inline

Definition at line 41 of file cp_model_utils.h.

◆ NegationOf() [1/3]

LinearExpression NegationOf ( const LinearExpression expr)

Definition at line 442 of file linear_constraint.cc.

◆ NegationOf() [2/3]

std::vector< IntegerVariable > NegationOf ( const std::vector< IntegerVariable > &  vars)

Definition at line 46 of file integer.cc.

◆ NegationOf() [3/3]

IntegerVariable operations_research::sat::NegationOf ( IntegerVariable  i)
inline

Definition at line 141 of file integer.h.

◆ NewBooleanVariable()

std::function<BooleanVariable(Model*)> operations_research::sat::NewBooleanVariable ( )
inline

Definition at line 1720 of file integer.h.

◆ NewFeasibleSolutionObserver()

std::function< void(Model *)> NewFeasibleSolutionObserver ( const std::function< void(const CpSolverResponse &response)> &  observer)

Creates a solution observer with the model with model.Add(NewFeasibleSolutionObserver([](response){...}));.

The given function will be called on each improving feasible solution found during the search. For a non-optimization problem, if the option to find all solution was set, then this will be called on each new solution.

WARNING: Except when enumerate_all_solution() is true, one shouldn't rely on this to get a set of "diverse" solutions since any future change to the solver might completely kill any diversity in the set of solutions observed.

Valid usage of this includes implementing features like:

  • Enumerating all solution via enumerate_all_solution(). If only n solutions are needed, this can also be used to abort when this number is reached.
  • Aborting early if a good enough solution is found.
  • Displaying log progress.
  • etc...

Definition at line 1019 of file cp_model_solver.cc.

◆ NewIntegerVariable() [1/2]

std::function<IntegerVariable(Model*)> operations_research::sat::NewIntegerVariable ( const Domain domain)
inline

Definition at line 1743 of file integer.h.

◆ NewIntegerVariable() [2/2]

std::function<IntegerVariable(Model*)> operations_research::sat::NewIntegerVariable ( int64_t  lb,
int64_t  ub 
)
inline

Definition at line 1734 of file integer.h.

◆ NewIntegerVariableFromLiteral()

std::function<IntegerVariable(Model*)> operations_research::sat::NewIntegerVariableFromLiteral ( Literal  lit)
inline

Definition at line 1752 of file integer.h.

◆ NewInterval() [1/2]

std::function<IntervalVariable(Model*)> operations_research::sat::NewInterval ( int64_t  min_start,
int64_t  max_end,
int64_t  size 
)
inline

Definition at line 827 of file intervals.h.

◆ NewInterval() [2/2]

std::function<IntervalVariable(Model*)> operations_research::sat::NewInterval ( IntegerVariable  start,
IntegerVariable  end,
IntegerVariable  size 
)
inline

Definition at line 838 of file intervals.h.

◆ NewIntervalWithVariableSize()

std::function<IntervalVariable(Model*)> operations_research::sat::NewIntervalWithVariableSize ( int64_t  min_start,
int64_t  max_end,
int64_t  min_size,
int64_t  max_size 
)
inline

Definition at line 846 of file intervals.h.

◆ NewOptionalInterval() [1/2]

std::function<IntervalVariable(Model*)> operations_research::sat::NewOptionalInterval ( int64_t  min_start,
int64_t  max_end,
int64_t  size,
Literal  is_present 
)
inline

Definition at line 857 of file intervals.h.

◆ NewOptionalInterval() [2/2]

std::function<IntervalVariable(Model*)> operations_research::sat::NewOptionalInterval ( IntegerVariable  start,
IntegerVariable  end,
IntegerVariable  size,
Literal  is_present 
)
inline

Definition at line 884 of file intervals.h.

◆ NewOptionalIntervalWithOptionalVariables()

std::function<IntervalVariable(Model*)> operations_research::sat::NewOptionalIntervalWithOptionalVariables ( int64_t  min_start,
int64_t  max_end,
int64_t  size,
Literal  is_present 
)
inline

Definition at line 868 of file intervals.h.

◆ NewOptionalIntervalWithVariableSize()

std::function<IntervalVariable(Model*)> operations_research::sat::NewOptionalIntervalWithVariableSize ( int64_t  min_start,
int64_t  max_end,
int64_t  min_size,
int64_t  max_size,
Literal  is_present 
)
inline

Definition at line 894 of file intervals.h.

◆ NewSatParameters() [1/3]

std::function<SatParameters(Model*)> operations_research::sat::NewSatParameters ( const sat::SatParameters &  parameters)

Definition at line 1039 of file cp_model_solver.cc.

◆ NewSatParameters() [2/3]

std::function<SatParameters(Model*)> operations_research::sat::NewSatParameters ( const SatParameters &  parameters)

◆ NewSatParameters() [3/3]

std::function< SatParameters(Model *)> NewSatParameters ( const std::string &  params)

Creates parameters for the solver, which you can add to the model with.

model->Add(NewSatParameters(parameters_as_string_or_proto))
GRBmodel * model
std::function< SatParameters(Model *)> NewSatParameters(const std::string &params)
Creates parameters for the solver, which you can add to the model with.

before calling SolveCpModel().

Definition at line 1028 of file cp_model_solver.cc.

◆ NewWeightedSum()

std::function<IntegerVariable(Model*)> operations_research::sat::NewWeightedSum ( const VectorInt &  coefficients,
const std::vector< IntegerVariable > &  vars 
)
inline

Definition at line 690 of file integer_expr.h.

◆ NoDuplicateVariable()

bool NoDuplicateVariable ( const LinearConstraint ct)

Definition at line 386 of file linear_constraint.cc.

◆ NonDeterministicLoop()

void NonDeterministicLoop ( const std::vector< std::unique_ptr< SubSolver >> &  subsolvers,
int  num_threads 
)

Definition at line 133 of file subsolver.cc.

◆ NonOverlappingRectangles()

std::function<void(Model*)> operations_research::sat::NonOverlappingRectangles ( const std::vector< IntervalVariable > &  x,
const std::vector< IntervalVariable > &  y,
bool  is_strict 
)
inline

Definition at line 98 of file diffn.h.

◆ Not()

BoolVar Not ( BoolVar  x)

A convenient wrapper so we can write Not(x) instead of x.Not() which is sometimes clearer.

Definition at line 86 of file cp_model.cc.

◆ operator*() [1/4]

DoubleLinearExpr operations_research::sat::operator* ( double  factor,
DoubleLinearExpr  expr 
)
inline

Definition at line 1295 of file cp_model.h.

◆ operator*() [2/4]

DoubleLinearExpr operations_research::sat::operator* ( DoubleLinearExpr  expr,
double  factor 
)
inline

Definition at line 1290 of file cp_model.h.

◆ operator*() [3/4]

LinearExpr operations_research::sat::operator* ( int64_t  factor,
LinearExpr  expr 
)
inline

Definition at line 1209 of file cp_model.h.

◆ operator*() [4/4]

LinearExpr operations_research::sat::operator* ( LinearExpr  expr,
int64_t  factor 
)
inline

Definition at line 1205 of file cp_model.h.

◆ operator+() [1/10]

DoubleLinearExpr operations_research::sat::operator+ ( const DoubleLinearExpr lhs,
const DoubleLinearExpr rhs 
)
inline

Definition at line 1221 of file cp_model.h.

◆ operator+() [2/10]

DoubleLinearExpr operations_research::sat::operator+ ( const DoubleLinearExpr lhs,
DoubleLinearExpr &&  rhs 
)
inline

Definition at line 1232 of file cp_model.h.

◆ operator+() [3/10]

LinearExpr operations_research::sat::operator+ ( const LinearExpr lhs,
const LinearExpr rhs 
)
inline

Definition at line 1163 of file cp_model.h.

◆ operator+() [4/10]

LinearExpr operations_research::sat::operator+ ( const LinearExpr lhs,
LinearExpr &&  rhs 
)
inline

Definition at line 1172 of file cp_model.h.

◆ operator+() [5/10]

DoubleLinearExpr operations_research::sat::operator+ ( double  lhs,
DoubleLinearExpr  expr 
)
inline

Definition at line 1252 of file cp_model.h.

◆ operator+() [6/10]

DoubleLinearExpr operations_research::sat::operator+ ( DoubleLinearExpr &&  lhs,
const DoubleLinearExpr rhs 
)
inline

Definition at line 1227 of file cp_model.h.

◆ operator+() [7/10]

DoubleLinearExpr operations_research::sat::operator+ ( DoubleLinearExpr &&  lhs,
DoubleLinearExpr &&  rhs 
)
inline

Definition at line 1237 of file cp_model.h.

◆ operator+() [8/10]

DoubleLinearExpr operations_research::sat::operator+ ( DoubleLinearExpr  expr,
double  rhs 
)
inline

Definition at line 1248 of file cp_model.h.

◆ operator+() [9/10]

LinearExpr operations_research::sat::operator+ ( LinearExpr &&  lhs,
const LinearExpr rhs 
)
inline

Definition at line 1168 of file cp_model.h.

◆ operator+() [10/10]

LinearExpr operations_research::sat::operator+ ( LinearExpr &&  lhs,
LinearExpr &&  rhs 
)
inline

Definition at line 1176 of file cp_model.h.

◆ operator-() [1/12]

DoubleLinearExpr operations_research::sat::operator- ( const DoubleLinearExpr lhs,
const DoubleLinearExpr rhs 
)
inline

Definition at line 1257 of file cp_model.h.

◆ operator-() [2/12]

DoubleLinearExpr operations_research::sat::operator- ( const DoubleLinearExpr lhs,
DoubleLinearExpr &&  rhs 
)
inline

Definition at line 1268 of file cp_model.h.

◆ operator-() [3/12]

LinearExpr operations_research::sat::operator- ( const LinearExpr lhs,
const LinearExpr rhs 
)
inline

Definition at line 1186 of file cp_model.h.

◆ operator-() [4/12]

LinearExpr operations_research::sat::operator- ( const LinearExpr lhs,
LinearExpr &&  rhs 
)
inline

Definition at line 1195 of file cp_model.h.

◆ operator-() [5/12]

DoubleLinearExpr operations_research::sat::operator- ( double  lhs,
DoubleLinearExpr  expr 
)
inline

Definition at line 1284 of file cp_model.h.

◆ operator-() [6/12]

DoubleLinearExpr operations_research::sat::operator- ( DoubleLinearExpr &&  lhs,
const DoubleLinearExpr rhs 
)
inline

Definition at line 1263 of file cp_model.h.

◆ operator-() [7/12]

DoubleLinearExpr operations_research::sat::operator- ( DoubleLinearExpr &&  lhs,
DoubleLinearExpr &&  rhs 
)
inline

Definition at line 1274 of file cp_model.h.

◆ operator-() [8/12]

DoubleLinearExpr operations_research::sat::operator- ( DoubleLinearExpr  epxr,
double  rhs 
)
inline

Definition at line 1280 of file cp_model.h.

◆ operator-() [9/12]

DoubleLinearExpr operations_research::sat::operator- ( DoubleLinearExpr  expr)
inline

Definition at line 1216 of file cp_model.h.

◆ operator-() [10/12]

LinearExpr operations_research::sat::operator- ( LinearExpr &&  lhs,
const LinearExpr rhs 
)
inline

Definition at line 1191 of file cp_model.h.

◆ operator-() [11/12]

LinearExpr operations_research::sat::operator- ( LinearExpr &&  lhs,
LinearExpr &&  rhs 
)
inline

Definition at line 1200 of file cp_model.h.

◆ operator-() [12/12]

LinearExpr operations_research::sat::operator- ( LinearExpr  expr)
inline

Definition at line 1161 of file cp_model.h.

◆ operator<<() [1/15]

std::ostream& operations_research::sat::operator<< ( std::ostream &  os,
absl::Span< const IntegerLiteral literals 
)
inline

Definition at line 226 of file integer.h.

◆ operator<<() [2/15]

std::ostream& operations_research::sat::operator<< ( std::ostream &  os,
absl::Span< const Literal literals 
)
inline

Definition at line 118 of file sat_base.h.

◆ operator<<() [3/15]

std::ostream & operator<< ( std::ostream &  os,
const BoolVar var 
)

Definition at line 88 of file cp_model.cc.

◆ operator<<() [4/15]

std::ostream & operator<< ( std::ostream &  os,
const DoubleLinearExpr e 
)

Definition at line 487 of file cp_model.cc.

◆ operator<<() [5/15]

std::ostream & operator<< ( std::ostream &  os,
const EnforcementStatus e 
)

Definition at line 131 of file linear_propagation.cc.

◆ operator<<() [6/15]

std::ostream & operator<< ( std::ostream &  os,
const IntervalVar var 
)

Definition at line 640 of file cp_model.cc.

◆ operator<<() [7/15]

std::ostream & operator<< ( std::ostream &  os,
const IntVar var 
)

Definition at line 170 of file cp_model.cc.

◆ operator<<() [8/15]

std::ostream& operations_research::sat::operator<< ( std::ostream &  os,
const LinearConstraint ct 
)
inline

Definition at line 89 of file sat/linear_constraint.h.

◆ operator<<() [9/15]

std::ostream & operator<< ( std::ostream &  os,
const LinearExpr e 
)

Definition at line 317 of file cp_model.cc.

◆ operator<<() [10/15]

std::ostream & operator<< ( std::ostream &  os,
const ValueLiteralPair p 
)

Definition at line 60 of file integer.cc.

◆ operator<<() [11/15]

std::ostream& operations_research::sat::operator<< ( std::ostream &  os,
IntegerLiteral  i_lit 
)
inline

Definition at line 221 of file integer.h.

◆ operator<<() [12/15]

std::ostream& operations_research::sat::operator<< ( std::ostream &  os,
Literal  literal 
)
inline

Definition at line 113 of file sat_base.h.

◆ operator<<() [13/15]

std::ostream& operations_research::sat::operator<< ( std::ostream &  os,
LiteralWithCoeff  term 
)
inline

Definition at line 70 of file pb_constraint.h.

◆ operator<<() [14/15]

std::ostream& operations_research::sat::operator<< ( std::ostream &  os,
SatSolver::Status  status 
)
inline

Definition at line 1071 of file sat_solver.h.

◆ operator<<() [15/15]

std::ostream & operator<< ( std::ostream &  out,
const IndexedInterval interval 
)

Definition at line 356 of file diffn_util.cc.

◆ PartialIsOneOfVar()

std::function<void(Model*)> operations_research::sat::PartialIsOneOfVar ( IntegerVariable  target_var,
const std::vector< IntegerVariable > &  vars,
const std::vector< Literal > &  selectors 
)
inline

Definition at line 161 of file cp_constraints.h.

◆ PositiveMod()

int64_t PositiveMod ( int64_t  x,
int64_t  m 
)

Definition at line 137 of file sat/util.cc.

◆ PositiveRef()

int operations_research::sat::PositiveRef ( int  ref)
inline

Definition at line 42 of file cp_model_utils.h.

◆ PositiveRemainder()

IntegerValue operations_research::sat::PositiveRemainder ( IntegerValue  dividend,
IntegerValue  positive_divisor 
)
inline

Definition at line 113 of file integer.h.

◆ PositiveVarExpr()

LinearExpression PositiveVarExpr ( const LinearExpression expr)

Definition at line 450 of file linear_constraint.cc.

◆ PositiveVariable()

IntegerVariable operations_research::sat::PositiveVariable ( IntegerVariable  i)
inline

Definition at line 149 of file integer.h.

◆ PossibleIntegerOverflow()

bool PossibleIntegerOverflow ( const CpModelProto &  model,
absl::Span< const int >  vars,
absl::Span< const int64_t >  coeffs,
int64_t  offset 
)

Definition at line 860 of file cp_model_checker.cc.

◆ PossibleOverflow()

bool PossibleOverflow ( const IntegerTrail integer_trail,
const LinearConstraint constraint 
)

Definition at line 1778 of file linear_programming_constraint.cc.

◆ PostsolveClause()

void operations_research::sat::PostsolveClause ( const ConstraintProto &  ct,
std::vector< Domain > *  domains 
)

Definition at line 35 of file cp_model_postsolve.cc.

◆ PostsolveElement()

void operations_research::sat::PostsolveElement ( const ConstraintProto &  ct,
std::vector< Domain > *  domains 
)

Definition at line 226 of file cp_model_postsolve.cc.

◆ PostsolveExactlyOne()

void operations_research::sat::PostsolveExactlyOne ( const ConstraintProto &  ct,
std::vector< Domain > *  domains 
)

Definition at line 58 of file cp_model_postsolve.cc.

◆ PostsolveLinear()

void operations_research::sat::PostsolveLinear ( const ConstraintProto &  ct,
std::vector< Domain > *  domains 
)

Definition at line 112 of file cp_model_postsolve.cc.

◆ PostsolveLinMax()

void operations_research::sat::PostsolveLinMax ( const ConstraintProto &  ct,
std::vector< Domain > *  domains 
)

Definition at line 213 of file cp_model_postsolve.cc.

◆ PostsolveResponse()

void PostsolveResponse ( const int64_t  num_variables_in_original_model,
const CpModelProto &  mapping_proto,
const std::vector< int > &  postsolve_mapping,
std::vector< int64_t > *  solution 
)

Definition at line 309 of file cp_model_postsolve.cc.

◆ PresolveBooleanLinearExpression()

void PresolveBooleanLinearExpression ( std::vector< Literal > *  literals,
std::vector< Coefficient > *  coefficients,
Coefficient *  offset 
)

Definition at line 1676 of file optimization.cc.

◆ PresolveCpModel()

CpSolverStatus PresolveCpModel ( PresolveContext context,
std::vector< int > *  postsolve_mapping 
)

Definition at line 10477 of file cp_model_presolve.cc.

◆ PreventOverflow()

void PreventOverflow ( const IntegerTrail integer_trail,
LinearConstraint constraint 
)

Definition at line 1861 of file linear_programming_constraint.cc.

◆ PrintClauses()

bool PrintClauses ( const std::string &  file_path,
SatFormat  format,
const std::vector< std::vector< Literal >> &  clauses,
int  num_variables 
)

Definition at line 606 of file drat_checker.cc.

◆ ProbeAndFindEquivalentLiteral()

void ProbeAndFindEquivalentLiteral ( SatSolver solver,
SatPostsolver postsolver,
DratProofHandler drat_proof_handler,
absl::StrongVector< LiteralIndex, LiteralIndex > *  mapping 
)

Definition at line 1139 of file simplification.cc.

◆ ProbeAndSimplifyProblem()

void ProbeAndSimplifyProblem ( SatPostsolver postsolver,
LinearBooleanProblem *  problem 
)

Definition at line 838 of file boolean_problem.cc.

◆ ProcessCore()

bool ProcessCore ( const std::vector< Literal > &  core,
Coefficient  min_weight,
std::deque< EncodingNode > *  repository,
std::vector< EncodingNode * > *  nodes,
SatSolver solver 
)

Definition at line 551 of file encoding.cc.

◆ ProcessCoreWithAlternativeEncoding()

bool ProcessCoreWithAlternativeEncoding ( const std::vector< Literal > &  core,
Coefficient  min_weight,
std::deque< EncodingNode > *  repository,
std::vector< EncodingNode * > *  nodes,
SatSolver solver 
)

Definition at line 599 of file encoding.cc.

◆ ProductConstraint()

std::function<void(Model*)> operations_research::sat::ProductConstraint ( AffineExpression  a,
AffineExpression  b,
AffineExpression  p 
)
inline

Definition at line 818 of file integer_expr.h.

◆ ProductWithModularInverse()

int64_t ProductWithModularInverse ( int64_t  coeff,
int64_t  mod,
int64_t  rhs 
)

Definition at line 142 of file sat/util.cc.

◆ PropagateAutomaton()

void PropagateAutomaton ( const AutomatonConstraintProto &  proto,
const PresolveContext context,
std::vector< absl::flat_hash_set< int64_t >> *  states,
std::vector< absl::flat_hash_set< int64_t >> *  labels 
)

Definition at line 47 of file cp_model_expand.cc.

◆ PropagateEncodingFromEquivalenceRelations()

void PropagateEncodingFromEquivalenceRelations ( const CpModelProto &  model_proto,
Model m 
)

Definition at line 699 of file cp_model_loader.cc.

◆ PseudoCost()

std::function< BooleanOrIntegerLiteral()> PseudoCost ( Model model)

Definition at line 374 of file integer_search.cc.

◆ RandomizeDecisionHeuristic()

void RandomizeDecisionHeuristic ( absl::BitGenRef  random,
SatParameters *  parameters 
)

Definition at line 61 of file sat/util.cc.

◆ RandomizeOnRestartHeuristic()

std::function<BooleanOrIntegerLiteral()> operations_research::sat::RandomizeOnRestartHeuristic ( Model model)

Definition at line 509 of file integer_search.cc.

◆ ReadDomainFromProto()

Domain operations_research::sat::ReadDomainFromProto ( const ProtoWithDomain &  proto)

Definition at line 111 of file cp_model_utils.h.

◆ RecordLPRelaxationValues()

void RecordLPRelaxationValues ( Model model)

Definition at line 33 of file rins.cc.

◆ ReduceModuloBasis()

void ReduceModuloBasis ( const std::vector< std::vector< absl::int128 >> &  basis,
const int  elements_to_consider,
std::vector< absl::int128 > &  v 
)

Definition at line 43 of file diophantine.cc.

◆ ReduceNodesAndExtractAssumptions()

std::vector< Literal > ReduceNodesAndExtractAssumptions ( Coefficient  upper_bound,
Coefficient  stratified_lower_bound,
Coefficient *  lower_bound,
std::vector< EncodingNode * > *  nodes,
SatSolver solver 
)

Definition at line 471 of file encoding.cc.

◆ RefIsPositive()

bool operations_research::sat::RefIsPositive ( int  ref)
inline

Definition at line 43 of file cp_model_utils.h.

◆ RegisterAndTransferOwnership()

void operations_research::sat::RegisterAndTransferOwnership ( Model model,
T *  ct 
)

Definition at line 813 of file integer_expr.h.

◆ ReifiedBoolAnd()

std::function<void(Model*)> operations_research::sat::ReifiedBoolAnd ( const std::vector< Literal > &  literals,
Literal  r 
)
inline

Definition at line 1004 of file sat_solver.h.

◆ ReifiedBoolLe()

std::function<void(Model*)> operations_research::sat::ReifiedBoolLe ( Literal  a,
Literal  b,
Literal  r 
)
inline

Definition at line 1020 of file sat_solver.h.

◆ ReifiedBoolOr()

std::function<void(Model*)> operations_research::sat::ReifiedBoolOr ( const std::vector< Literal > &  literals,
Literal  r 
)
inline

Definition at line 970 of file sat_solver.h.

◆ ReindexArcs()

int operations_research::sat::ReindexArcs ( IntContainer *  tails,
IntContainer *  heads,
absl::flat_hash_map< int, int > *  mapping_output = nullptr 
)

Definition at line 209 of file circuit.h.

◆ RemoveNearZeroTerms()

void RemoveNearZeroTerms ( const SatParameters &  params,
MPModelProto *  mp_model,
SolverLogger logger 
)

Definition at line 239 of file sat/lp_utils.cc.

◆ RemoveZeroTerms()

void RemoveZeroTerms ( LinearConstraint constraint)

Definition at line 269 of file linear_constraint.cc.

◆ ReportEnergyConflict()

bool ReportEnergyConflict ( Rectangle  bounding_box,
absl::Span< const int >  boxes,
SchedulingConstraintHelper x,
SchedulingConstraintHelper y 
)

Definition at line 67 of file diffn_util.cc.

◆ ResetAndSolveIntegerProblem()

SatSolver::Status ResetAndSolveIntegerProblem ( const std::vector< Literal > &  assumptions,
Model model 
)

Definition at line 1114 of file integer_search.cc.

◆ Resolve()

bool Resolve ( absl::Span< const Literal clause,
absl::Span< const Literal other_clause,
Literal  complementary_literal,
VariablesAssignment assignment,
std::vector< Literal > *  resolvent 
)

Definition at line 478 of file drat_checker.cc.

◆ RestartEveryKFailures()

std::function< bool()> RestartEveryKFailures ( int  k,
SatSolver solver 
)

Definition at line 675 of file integer_search.cc.

◆ RestrictObjectiveDomainWithBinarySearch()

void RestrictObjectiveDomainWithBinarySearch ( IntegerVariable  objective_var,
const std::function< void()> &  feasible_solution_observer,
Model model 
)

Definition at line 1109 of file optimization.cc.

◆ SafeDoubleToInt64()

int64_t SafeDoubleToInt64 ( double  value)
inline

Definition at line 387 of file sat/util.h.

◆ SatSolverHeuristic()

std::function< BooleanOrIntegerLiteral()> SatSolverHeuristic ( Model model)

Definition at line 336 of file integer_search.cc.

◆ SatSolverRestartPolicy()

std::function< bool()> SatSolverRestartPolicy ( Model model)

Definition at line 689 of file integer_search.cc.

◆ SatStatusString()

std::string SatStatusString ( SatSolver::Status  status)

Definition at line 2649 of file sat_solver.cc.

◆ ScalarProduct()

double ScalarProduct ( const LinearConstraint constraint1,
const LinearConstraint constraint2 
)

Definition at line 216 of file linear_constraint.cc.

◆ ScaleAndSetObjective()

bool ScaleAndSetObjective ( const SatParameters &  params,
const std::vector< std::pair< int, double >> &  objective,
double  objective_offset,
bool  maximize,
CpModelProto *  cp_model,
SolverLogger logger 
)

Definition at line 1266 of file sat/lp_utils.cc.

◆ ScaleContinuousVariables()

std::vector< double > ScaleContinuousVariables ( double  scaling,
double  max_bound,
MPModelProto *  mp_model 
)

Definition at line 107 of file sat/lp_utils.cc.

◆ ScaleInnerObjectiveValue()

int64_t operations_research::sat::ScaleInnerObjectiveValue ( const CpObjectiveProto &  proto,
int64_t  value 
)
inline

Definition at line 150 of file cp_model_utils.h.

◆ ScaleObjectiveValue()

double operations_research::sat::ScaleObjectiveValue ( const CpObjectiveProto &  proto,
int64_t  value 
)
inline

Definition at line 137 of file cp_model_utils.h.

◆ SchedulingSearchHeuristic()

std::function< BooleanOrIntegerLiteral()> SchedulingSearchHeuristic ( Model model)

Definition at line 396 of file integer_search.cc.

◆ SeparateFlowInequalities()

void operations_research::sat::SeparateFlowInequalities ( int  num_nodes,
const std::vector< int > &  tails,
const std::vector< int > &  heads,
const std::vector< AffineExpression > &  arc_capacities,
std::function< void(const std::vector< bool > &in_subset, IntegerValue *min_incoming_flow, IntegerValue *min_outgoing_flow)>  get_flows,
const absl::StrongVector< IntegerVariable, double > &  lp_values,
LinearConstraintManager manager,
Model model 
)

Definition at line 462 of file routing_cuts.cc.

◆ SeparateSubtourInequalities()

void operations_research::sat::SeparateSubtourInequalities ( int  num_nodes,
const std::vector< int > &  tails,
const std::vector< int > &  heads,
const std::vector< Literal > &  literals,
const absl::StrongVector< IntegerVariable, double > &  lp_values,
absl::Span< const int64_t >  demands,
int64_t  capacity,
LinearConstraintManager manager,
Model model 
)

Definition at line 235 of file routing_cuts.cc.

◆ SequentialLoop()

void SequentialLoop ( const std::vector< std::unique_ptr< SubSolver >> &  subsolvers)

Definition at line 64 of file subsolver.cc.

◆ SequentialSearch()

std::function< BooleanOrIntegerLiteral()> SequentialSearch ( std::vector< std::function< BooleanOrIntegerLiteral()>>  heuristics)

Definition at line 203 of file integer_search.cc.

◆ SequentialValueSelection()

std::function< BooleanOrIntegerLiteral()> SequentialValueSelection ( std::vector< std::function< IntegerLiteral(IntegerVariable)>>  value_selection_heuristics,
std::function< BooleanOrIntegerLiteral()>  var_selection_heuristic,
Model model 
)

Definition at line 214 of file integer_search.cc.

◆ SetEnforcementLiteralToFalse()

void operations_research::sat::SetEnforcementLiteralToFalse ( const ConstraintProto &  ct,
std::vector< Domain > *  domains 
)

Definition at line 89 of file cp_model_postsolve.cc.

◆ SetToNegatedLinearExpression()

void SetToNegatedLinearExpression ( const LinearExpressionProto &  input_expr,
LinearExpressionProto *  output_negated_expr 
)

Definition at line 40 of file cp_model_utils.cc.

◆ SetupTextFormatPrinter()

void SetupTextFormatPrinter ( google::protobuf::TextFormat::Printer *  printer)

Definition at line 814 of file cp_model_utils.cc.

◆ ShaveObjectiveLb()

std::function<BooleanOrIntegerLiteral()> operations_research::sat::ShaveObjectiveLb ( Model model)

Definition at line 351 of file integer_search.cc.

◆ SimplifyCanonicalBooleanLinearConstraint()

void SimplifyCanonicalBooleanLinearConstraint ( std::vector< LiteralWithCoeff > *  cst,
Coefficient *  rhs 
)

Definition at line 160 of file pb_constraint.cc.

◆ SimplifyClause()

bool SimplifyClause ( const std::vector< Literal > &  a,
std::vector< Literal > *  b,
LiteralIndex *  opposite_literal,
int64_t *  num_inspected_literals 
)

Definition at line 941 of file simplification.cc.

◆ SizeVar()

std::function<IntegerVariable(const Model&)> operations_research::sat::SizeVar ( IntervalVariable  v)
inline

Definition at line 795 of file intervals.h.

◆ SolutionBooleanValue()

bool SolutionBooleanValue ( const CpSolverResponse &  r,
BoolVar  x 
)

Evaluates the value of a Boolean literal in a solver response.

Definition at line 1358 of file cp_model.cc.

◆ SolutionIntegerValue()

int64_t SolutionIntegerValue ( const CpSolverResponse &  r,
const LinearExpr expr 
)

Evaluates the value of an linear expression in a solver response.

Definition at line 1347 of file cp_model.cc.

◆ SolutionIsFeasible()

bool SolutionIsFeasible ( const CpModelProto &  model,
absl::Span< const int64_t >  variable_values,
const CpModelProto *  mapping_proto,
const std::vector< int > *  postsolve_mapping 
)

Definition at line 1558 of file cp_model_checker.cc.

◆ Solve()

CpSolverResponse Solve ( const CpModelProto &  model_proto)

Solves the given CpModelProto and returns an instance of CpSolverResponse.

Definition at line 4106 of file cp_model_solver.cc.

◆ SolveCpModel()

CpSolverResponse SolveCpModel ( const CpModelProto &  model_proto,
Model model 
)

Solves the given CpModelProto.

This advanced API accept a Model* which allows to access more adavanced features by configuring some classes in the Model before solve.

For instance:

  • model->Add(NewSatParameters(parameters_as_string_or_proto));
  • model->GetOrCreate<TimeLimit>()->RegisterExternalBooleanAsLimit(&stop);
  • model->Add(NewFeasibleSolutionObserver(observer));

Definition at line 3503 of file cp_model_solver.cc.

◆ SolveDiophantine()

DiophantineSolution SolveDiophantine ( absl::Span< const int64_t >  coeffs,
int64_t  rhs,
absl::Span< const int64_t >  var_lbs,
absl::Span< const int64_t >  var_ubs 
)

Definition at line 117 of file diophantine.cc.

◆ SolveDiophantineEquationOfSizeTwo()

bool SolveDiophantineEquationOfSizeTwo ( int64_t &  a,
int64_t &  b,
int64_t &  cte,
int64_t &  x0,
int64_t &  y0 
)

Definition at line 164 of file sat/util.cc.

◆ SolveFzWithCpModelProto()

void SolveFzWithCpModelProto ( const fz::Model fz_model,
const fz::FlatzincSatParameters p,
const std::string &  sat_params,
SolverLogger logger,
SolverLogger solution_logger 
)

Definition at line 1147 of file cp_model_fz_solver.cc.

◆ SolveIntegerProblemWithLazyEncoding()

SatSolver::Status SolveIntegerProblemWithLazyEncoding ( Model model)

Definition at line 1135 of file integer_search.cc.

◆ SolveWithCardinalityEncoding()

SatSolver::Status SolveWithCardinalityEncoding ( LogBehavior  log,
const LinearBooleanProblem &  problem,
SatSolver solver,
std::vector< bool > *  solution 
)

Definition at line 901 of file optimization.cc.

◆ SolveWithCardinalityEncodingAndCore()

SatSolver::Status SolveWithCardinalityEncodingAndCore ( LogBehavior  log,
const LinearBooleanProblem &  problem,
SatSolver solver,
std::vector< bool > *  solution 
)

Definition at line 969 of file optimization.cc.

◆ SolveWithFuMalik()

SatSolver::Status SolveWithFuMalik ( LogBehavior  log,
const LinearBooleanProblem &  problem,
SatSolver solver,
std::vector< bool > *  solution 
)

Definition at line 283 of file optimization.cc.

◆ SolveWithLinearScan()

SatSolver::Status SolveWithLinearScan ( LogBehavior  log,
const LinearBooleanProblem &  problem,
SatSolver solver,
std::vector< bool > *  solution 
)

Definition at line 855 of file optimization.cc.

◆ SolveWithParameters() [1/2]

CpSolverResponse SolveWithParameters ( const CpModelProto &  model_proto,
const SatParameters &  params 
)

Solves the given CpModelProto with the given parameters.

Definition at line 4111 of file cp_model_solver.cc.

◆ SolveWithParameters() [2/2]

CpSolverResponse SolveWithParameters ( const CpModelProto &  model_proto,
const std::string &  params 
)

Solves the given CpModelProto with the given sat parameters as string in JSon format, and returns an instance of CpSolverResponse.

Definition at line 4119 of file cp_model_solver.cc.

◆ SolveWithPresolve()

SatSolver::Status SolveWithPresolve ( std::unique_ptr< SatSolver > *  solver,
TimeLimit time_limit,
std::vector< bool > *  solution,
DratProofHandler drat_proof_handler,
SolverLogger logger 
)

Definition at line 1257 of file simplification.cc.

◆ SolveWithRandomParameters()

SatSolver::Status SolveWithRandomParameters ( LogBehavior  log,
const LinearBooleanProblem &  problem,
int  num_times,
absl::BitGenRef  random,
SatSolver solver,
std::vector< bool > *  solution 
)

Definition at line 777 of file optimization.cc.

◆ SolveWithWPM1()

SatSolver::Status SolveWithWPM1 ( LogBehavior  log,
const LinearBooleanProblem &  problem,
SatSolver solver,
std::vector< bool > *  solution 
)

Definition at line 480 of file optimization.cc.

◆ SpanOfIntervals()

std::function< void(Model *)> SpanOfIntervals ( IntervalVariable  span,
const std::vector< IntervalVariable > &  intervals 
)

Definition at line 318 of file scheduling_constraints.cc.

◆ SplitAndLoadIntermediateConstraints()

void SplitAndLoadIntermediateConstraints ( bool  lb_required,
bool  ub_required,
std::vector< IntegerVariable > *  vars,
std::vector< int64_t > *  coeffs,
Model m 
)

Definition at line 1021 of file cp_model_loader.cc.

◆ SplitAroundGivenValue()

IntegerLiteral SplitAroundGivenValue ( IntegerVariable  var,
IntegerValue  value,
Model model 
)

Definition at line 84 of file integer_search.cc.

◆ SplitAroundLpValue()

IntegerLiteral SplitAroundLpValue ( IntegerVariable  var,
Model model 
)

Definition at line 112 of file integer_search.cc.

◆ SplitDomainUsingBestSolutionValue()

IntegerLiteral operations_research::sat::SplitDomainUsingBestSolutionValue ( IntegerVariable  var,
Model model 
)

◆ SplitUsingBestSolutionValueInRepository()

IntegerLiteral operations_research::sat::SplitUsingBestSolutionValueInRepository ( IntegerVariable  var,
const SharedSolutionRepository< int64_t > &  solution_repo,
Model model 
)

Definition at line 143 of file integer_search.cc.

◆ StartVar()

std::function<IntegerVariable(const Model&)> operations_research::sat::StartVar ( IntervalVariable  v)
inline

Definition at line 782 of file intervals.h.

◆ StoreAssignment()

void StoreAssignment ( const VariablesAssignment assignment,
BooleanAssignment *  output 
)

Definition at line 487 of file boolean_problem.cc.

◆ SubcircuitConstraint()

std::function< void(Model *)> SubcircuitConstraint ( int  num_nodes,
const std::vector< int > &  tails,
const std::vector< int > &  heads,
const std::vector< Literal > &  literals,
bool  multiple_subcircuit_through_zero 
)

Definition at line 631 of file circuit.cc.

◆ SubstituteVariable()

bool SubstituteVariable ( int  var,
int64_t  var_coeff_in_definition,
const ConstraintProto &  definition,
ConstraintProto *  ct 
)

Definition at line 202 of file presolve_util.cc.

◆ Sum2LowerOrEqual()

std::function<void(Model*)> operations_research::sat::Sum2LowerOrEqual ( IntegerVariable  a,
IntegerVariable  b,
int64_t  ub 
)
inline

Definition at line 394 of file precedences.h.

◆ Sum3LowerOrEqual()

std::function<void(Model*)> operations_research::sat::Sum3LowerOrEqual ( IntegerVariable  a,
IntegerVariable  b,
IntegerVariable  c,
int64_t  ub 
)
inline

Definition at line 412 of file precedences.h.

◆ SUniv()

int operations_research::sat::SUniv ( int  i)
inline

Definition at line 87 of file restart.h.

◆ ToDouble()

double operations_research::sat::ToDouble ( IntegerValue  value)
inline

Definition at line 77 of file integer.h.

◆ ToIntegerValueVector()

std::vector<IntegerValue> operations_research::sat::ToIntegerValueVector ( const std::vector< int64_t > &  input)
inline

Definition at line 103 of file cp_constraints.h.

◆ TransformToGeneratorOfStabilizer()

void operations_research::sat::TransformToGeneratorOfStabilizer ( int  to_stabilize,
std::vector< std::unique_ptr< SparsePermutation >> *  generators 
)
inline

Definition at line 78 of file symmetry_util.h.

◆ TryToDecomposeProduct()

std::vector< LiteralValueValue > TryToDecomposeProduct ( const AffineExpression left,
const AffineExpression right,
Model model 
)

Definition at line 357 of file implied_bounds.cc.

◆ TryToLinearizeConstraint()

void TryToLinearizeConstraint ( const CpModelProto &  model_proto,
const ConstraintProto &  ct,
int  linearization_level,
Model model,
LinearRelaxation relaxation,
ActivityBoundHelper activity_helper 
)

Definition at line 1218 of file linear_relaxation.cc.

◆ TryToReconcileEncodings()

std::vector<LiteralValueValue> operations_research::sat::TryToReconcileEncodings ( const AffineExpression size2_affine,
const AffineExpression affine,
const std::vector< ValueLiteralPair > &  affine_var_encoding,
bool  put_affine_left_in_result,
Model model 
)

Definition at line 266 of file implied_bounds.cc.

◆ TryToReconcileSize2Encodings()

std::vector<LiteralValueValue> operations_research::sat::TryToReconcileSize2Encodings ( const AffineExpression left,
const AffineExpression right,
Model model 
)

Definition at line 311 of file implied_bounds.cc.

◆ UnassignedVarWithLowestMinAtItsMinHeuristic()

std::function< BooleanOrIntegerLiteral()> UnassignedVarWithLowestMinAtItsMinHeuristic ( const std::vector< IntegerVariable > &  vars,
Model model 
)

Definition at line 183 of file integer_search.cc.

◆ UnscaleObjectiveValue()

double operations_research::sat::UnscaleObjectiveValue ( const CpObjectiveProto &  proto,
double  value 
)
inline

Definition at line 161 of file cp_model_utils.h.

◆ UpperBound()

std::function<int64_t(const Model&)> operations_research::sat::UpperBound ( IntegerVariable  v)
inline

Definition at line 1781 of file integer.h.

◆ UsedIntervals()

std::vector< int > UsedIntervals ( const ConstraintProto &  ct)

Definition at line 459 of file cp_model_utils.cc.

◆ UsedVariables()

std::vector< int > UsedVariables ( const ConstraintProto &  ct)

Definition at line 444 of file cp_model_utils.cc.

◆ UseObjectiveForSatAssignmentPreference()

void UseObjectiveForSatAssignmentPreference ( const LinearBooleanProblem &  problem,
SatSolver solver 
)

Definition at line 319 of file boolean_problem.cc.

◆ ValidateBooleanProblem()

absl::Status ValidateBooleanProblem ( const LinearBooleanProblem &  problem)

Definition at line 143 of file boolean_problem.cc.

◆ ValidateCpModel()

std::string ValidateCpModel ( const CpModelProto &  model,
bool  after_presolve 
)

Definition at line 896 of file cp_model_checker.cc.

◆ ValidateInputCpModel()

std::string ValidateInputCpModel ( const SatParameters &  params,
const CpModelProto &  model 
)

Definition at line 1083 of file cp_model_checker.cc.

◆ ValidateLinearConstraintForOverflow()

bool ValidateLinearConstraintForOverflow ( const LinearConstraint constraint,
const IntegerTrail integer_trail 
)

Definition at line 416 of file linear_constraint.cc.

◆ ValidateParameters()

std::string ValidateParameters ( const SatParameters &  params)

Definition at line 52 of file sat/parameters_validation.cc.

◆ Value() [1/3]

std::function<int64_t(const Model&)> operations_research::sat::Value ( BooleanVariable  b)
inline

Definition at line 1039 of file sat_solver.h.

◆ Value() [2/3]

std::function<int64_t(const Model&)> operations_research::sat::Value ( IntegerVariable  v)
inline

Definition at line 1795 of file integer.h.

◆ Value() [3/3]

std::function<int64_t(const Model&)> operations_research::sat::Value ( Literal  l)
inline

Definition at line 1030 of file sat_solver.h.

◆ VarDebugString()

std::string VarDebugString ( const CpModelProto &  proto,
int  index 
)

Definition at line 142 of file cp_model.cc.

◆ VariableIsPositive()

bool operations_research::sat::VariableIsPositive ( IntegerVariable  i)
inline

Definition at line 145 of file integer.h.

◆ WeightedSumGreaterOrEqual()

std::function<void(Model*)> operations_research::sat::WeightedSumGreaterOrEqual ( const std::vector< IntegerVariable > &  vars,
const VectorInt &  coefficients,
int64_t  lower_bound 
)
inline

Definition at line 427 of file integer_expr.h.

◆ WeightedSumGreaterOrEqualReif()

std::function<void(Model*)> operations_research::sat::WeightedSumGreaterOrEqualReif ( Literal  is_ge,
const std::vector< IntegerVariable > &  vars,
const VectorInt &  coefficients,
int64_t  lower_bound 
)
inline

Definition at line 573 of file integer_expr.h.

◆ WeightedSumLowerOrEqual()

std::function<void(Model*)> operations_research::sat::WeightedSumLowerOrEqual ( const std::vector< IntegerVariable > &  vars,
const VectorInt &  coefficients,
int64_t  upper_bound 
)
inline

Definition at line 369 of file integer_expr.h.

◆ WeightedSumLowerOrEqualReif()

std::function<void(Model*)> operations_research::sat::WeightedSumLowerOrEqualReif ( Literal  is_le,
const std::vector< IntegerVariable > &  vars,
const VectorInt &  coefficients,
int64_t  upper_bound 
)
inline

Definition at line 560 of file integer_expr.h.

◆ WeightedSumNotEqual()

std::function<void(Model*)> operations_research::sat::WeightedSumNotEqual ( const std::vector< IntegerVariable > &  vars,
const VectorInt &  coefficients,
int64_t  value 
)
inline

Definition at line 668 of file integer_expr.h.

◆ WriteModelProtoToFile()

bool operations_research::sat::WriteModelProtoToFile ( const M &  proto,
absl::string_view  filename 
)

Definition at line 247 of file cp_model_utils.h.

Variable Documentation

◆ kAffineRelationConstraint

constexpr int kAffineRelationConstraint = -2
constexpr

Definition at line 47 of file presolve_context.h.

◆ kAssumptionsConstraint

constexpr int kAssumptionsConstraint = -3
constexpr

Definition at line 48 of file presolve_context.h.

◆ kDefaultFingerprintSeed

constexpr uint64_t kDefaultFingerprintSeed = 0xa5b85c5e198ed849
constexpr

Definition at line 201 of file cp_model_utils.h.

◆ kObjectiveConstraint

constexpr int kObjectiveConstraint = -1
constexpr

Definition at line 46 of file presolve_context.h.

◆ kTableAnyValue

constexpr int64_t kTableAnyValue = std::numeric_limits<int64_t>::min()
constexpr

Definition at line 358 of file sat/util.h.

◆ kUnsatTrailIndex

const int kUnsatTrailIndex = -1

Definition at line 57 of file sat_solver.h.