OR-Tools  8.2
operations_research::sat Namespace Reference

Classes

class  AllDifferentConstraint
 
class  AllDifferentBoundsPropagator
 
class  CircuitPropagator
 
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  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  SimpleNeighborhoodGenerator
 
class  SimpleConstraintNeighborhoodGenerator
 
class  VariableGraphNeighborhoodGenerator
 
class  ConstraintGraphNeighborhoodGenerator
 
class  SchedulingNeighborhoodGenerator
 
class  SchedulingTimeWindowNeighborhoodGenerator
 
class  RelaxationInducedNeighborhoodGenerator
 
class  ConsecutiveConstraintsRelaxationNeighborhoodGenerator
 
class  WeightedRandomRelaxationNeighborhoodGenerator
 
class  FullEncodingFixedPointComputer
 
struct  ObjectiveDefinition
 
class  CpModelMapping
 
class  CpModelPresolver
 
struct  Strategy
 
struct  VarValue
 
struct  SolutionObservers
 
struct  IndexReferences
 
class  CumulativeEnergyConstraint
 
struct  CutGenerator
 
class  ImpliedBoundsProcessor
 
struct  RoundingOptions
 
class  IntegerRoundingCutHelper
 
class  CoverCutHelper
 
struct  KnapsackItem
 
class  NonOverlappingRectanglesEnergyPropagator
 
class  NonOverlappingRectanglesDisjunctivePropagator
 
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
 
struct  IntegerLiteral
 
struct  AffineExpression
 
struct  IntegerDomains
 
struct  DebugSolution
 
class  IntegerEncoder
 
class  IntegerTrail
 
class  PropagatorInterface
 
class  RevIntRepository
 
class  RevIntegerValueRepository
 
class  GenericLiteralWatcher
 
class  IntegerSumLE
 
class  LevelZeroEquality
 
class  MinPropagator
 
class  LinMinPropagator
 
class  PositiveProductPropagator
 
class  DivisionPropagator
 
class  FixedDivisionPropagator
 
class  SquarePropagator
 
struct  BooleanOrIntegerLiteral
 
struct  SearchHeuristics
 
struct  LevelZeroCallbackHelper
 
struct  BooleanOrIntegerVariable
 
class  IntervalsRepository
 
struct  TaskTime
 
class  SchedulingConstraintHelper
 
struct  LinearConstraint
 
class  LinearConstraintBuilder
 
struct  LinearExpression
 
class  LinearConstraintManager
 
class  TopN
 
class  TopNCuts
 
struct  LinearProgrammingConstraintLpSolution
 
struct  LPSolveInfo
 
class  ScatteredIntegerVector
 
class  LinearProgrammingConstraint
 
class  LinearProgrammingDispatcher
 
class  LinearProgrammingConstraintCollection
 
struct  LinearRelaxation
 
class  Model
 Class that owns everything related to a particular optimization model. More...
 
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  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
 
class  SatDecisionPolicy
 
struct  PostsolveClauses
 
struct  SatPresolveOptions
 
class  Inprocessing
 
class  StampingSimplifier
 
class  BlockedClauseSimplifier
 
class  BoundedVariableElimination
 
class  SatSolver
 
class  SelectedMinPropagator
 
class  PropagationGraph
 
class  SatPostsolver
 
class  SatPresolver
 
class  SubSolver
 
class  SynchronizationPoint
 
class  SymmetryPropagator
 
class  SharedSolutionRepository
 
class  SharedRelaxationSolutionRepository
 
class  SharedLPSolutionRepository
 
class  SharedIncompleteSolutionManager
 
class  SharedResponseManager
 
class  SharedBoundsManager
 
class  ThetaLambdaTree
 
class  ReservoirTimeTabling
 
class  TimeTablingPerTask
 
class  TimeTableEdgeFinding
 
class  ModelRandomGenerator
 
class  IncrementalAverage
 
class  ExponentialMovingAverage
 
class  Percentile
 
class  VarDomination
 
class  DualBoundStrengthening
 
class  ZeroHalfCutHelper
 

Typedefs

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

Enumerations

enum  SatFormat { DIMACS , DRAT }
 
enum  LogBehavior { DEFAULT_LOG , STDOUT_LOG }
 

Functions

void SolveFzWithCpModelProto (const fz::Model &fz_model, const fz::FlatzincSatParameters &p, const std::string &sat_params)
 
std::function< void(Model *)> AllDifferentBinary (const std::vector< IntegerVariable > &vars)
 
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)
 
std::vector< IntegerValue > ToIntegerValueVector (const std::vector< int64 > &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::ostream & operator<< (std::ostream &os, const IntVar &var)
 
std::ostream & operator<< (std::ostream &os, const IntervalVar &var)
 
int64 SolutionIntegerValue (const CpSolverResponse &r, const LinearExpr &expr)
 Evaluates the value of an linear expression in a solver response. More...
 
int64 SolutionIntegerMin (const CpSolverResponse &r, IntVar x)
 Returns the min of an integer variable in a solution. More...
 
int64 SolutionIntegerMax (const CpSolverResponse &r, IntVar x)
 Returns the max of an integer variable in a solution. More...
 
bool SolutionBooleanValue (const CpSolverResponse &r, BoolVar x)
 Evaluates the value of a Boolean literal in a solver response. More...
 
std::string ValidateCpModel (const CpModelProto &model)
 
bool SolutionIsFeasible (const CpModelProto &model, const std::vector< int64 > &variable_values, const CpModelProto *mapping_proto, const std::vector< int > *postsolve_mapping)
 
void ExpandCpModel (PresolveContext *context)
 
Neighborhood GenerateSchedulingNeighborhoodForRelaxation (const absl::Span< const int > intervals_to_relax, const CpSolverResponse &initial_solution, const NeighborhoodGeneratorHelper &helper)
 
void MaybeFullyEncodeMoreVariables (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 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 LoadIntMinConstraint (const ConstraintProto &ct, Model *m)
 
LinearExpression GetExprFromProto (const LinearExpressionProto &expr_proto, const CpModelMapping &mapping)
 
void LoadLinMaxConstraint (const ConstraintProto &ct, Model *m)
 
void LoadIntMaxConstraint (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)
 
bool DetectEquivalencesInElementConstraint (const ConstraintProto &ct, Model *m)
 
void LoadElementConstraintBounds (const ConstraintProto &ct, Model *m)
 
void LoadElementConstraintAC (const ConstraintProto &ct, Model *m)
 
void LoadElementConstraint (const ConstraintProto &ct, Model *m)
 
void LoadTableConstraint (const ConstraintProto &ct, Model *m)
 
void LoadAutomatonConstraint (const ConstraintProto &ct, Model *m)
 
std::vector< std::vector< Literal > > GetSquareMatrixFromIntegerVariables (const std::vector< IntegerVariable > &vars, Model *m)
 
void LoadCircuitConstraint (const ConstraintProto &ct, Model *m)
 
void LoadRoutesConstraint (const ConstraintProto &ct, Model *m)
 
bool LoadConstraint (const ConstraintProto &ct, Model *m)
 
void LoadCircuitCoveringConstraint (const ConstraintProto &ct, Model *m)
 
void LoadInverseConstraint (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 PostsolveLinear (const ConstraintProto &ct, const std::vector< bool > &prefer_lower_value, std::vector< Domain > *domains)
 
void PostsolveIntMax (const ConstraintProto &ct, std::vector< Domain > *domains)
 
void PostsolveElement (const ConstraintProto &ct, std::vector< Domain > *domains)
 
void PostsolveResponse (const int64 num_variables_in_original_model, const CpModelProto &mapping_proto, const std::vector< int > &postsolve_mapping, CpSolverResponse *response)
 
void LogInfoFromContext (const PresolveContext *context)
 
bool PresolveCpModel (PresolveContext *context, std::vector< int > *postsolve_mapping)
 
void ApplyVariableMapping (const std::vector< int > &mapping, const PresolveContext &context)
 
std::vector< int > FindDuplicateConstraints (const CpModelProto &model_proto)
 
const std::function< BooleanOrIntegerLiteral()> ConstructSearchStrategyInternal (const absl::flat_hash_map< int, std::pair< int64, int64 >> &var_to_coeff_offset_pair, const std::vector< Strategy > &strategies, Model *model)
 
std::function< BooleanOrIntegerLiteral()> ConstructSearchStrategy (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, const int num_workers)
 
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...
 
void SetSynchronizationFunction (std::function< CpSolverResponse()> f, Model *model)
 If set, the underlying solver will call this function regularly in a deterministic way. 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)
 
void DetectAndAddSymmetryToProto (const SatParameters &params, CpModelProto *proto)
 
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 ComputeInnerObjective (const CpObjectiveProto &objective, const CpSolverResponse &response)
 
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 value)
 
template<typename ProtoWithDomain >
void FillDomainInProto (const Domain &domain, ProtoWithDomain *proto)
 
template<typename ProtoWithDomain >
Domain ReadDomainFromProto (const ProtoWithDomain &proto)
 
template<typename ProtoWithDomain >
std::vector< int64AllValuesInDomain (const ProtoWithDomain &proto)
 
double ScaleObjectiveValue (const CpObjectiveProto &proto, int64 value)
 
double UnscaleObjectiveValue (const CpObjectiveProto &proto, double value)
 
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 AddCumulativeEnergyConstraint (std::vector< AffineExpression > energies, AffineExpression capacity, SchedulingConstraintHelper *helper, Model *model)
 
void AddCumulativeOverloadChecker (const std::vector< AffineExpression > &demands, AffineExpression capacity, SchedulingConstraintHelper *helper, Model *model)
 
bool LiftKnapsackCut (const LinearConstraint &constraint, const absl::StrongVector< IntegerVariable, double > &lp_values, const std::vector< IntegerValue > &cut_vars_original_coefficients, const IntegerTrail &integer_trail, TimeLimit *time_limit, LinearConstraint *cut)
 
LinearConstraint GetPreprocessedLinearConstraint (const LinearConstraint &constraint, const absl::StrongVector< IntegerVariable, double > &lp_values, const IntegerTrail &integer_trail)
 
bool ConstraintIsTriviallyTrue (const LinearConstraint &constraint, const IntegerTrail &integer_trail)
 
bool CanBeFilteredUsingCutLowerBound (const LinearConstraint &preprocessed_constraint, const absl::StrongVector< IntegerVariable, double > &lp_values, const IntegerTrail &integer_trail)
 
double GetKnapsackUpperBound (std::vector< KnapsackItem > items, const double capacity)
 
bool CanBeFilteredUsingKnapsackUpperBound (const LinearConstraint &constraint, const absl::StrongVector< IntegerVariable, double > &lp_values, const IntegerTrail &integer_trail)
 
bool CanFormValidKnapsackCover (const LinearConstraint &preprocessed_constraint, const absl::StrongVector< IntegerVariable, double > &lp_values, const IntegerTrail &integer_trail)
 
void ConvertToKnapsackForm (const LinearConstraint &constraint, std::vector< LinearConstraint > *knapsack_constraints, IntegerTrail *integer_trail)
 
CutGenerator CreateKnapsackCoverCutGenerator (const std::vector< LinearConstraint > &base_constraints, const std::vector< IntegerVariable > &vars, Model *model)
 
IntegerValue GetFactorT (IntegerValue rhs_remainder, IntegerValue divisor, IntegerValue max_t)
 
std::function< IntegerValue(IntegerValue)> GetSuperAdditiveRoundingFunction (IntegerValue rhs_remainder, IntegerValue divisor, IntegerValue t, IntegerValue max_scaling)
 
CutGenerator CreatePositiveMultiplicationCutGenerator (IntegerVariable z, IntegerVariable x, IntegerVariable y, Model *model)
 
CutGenerator CreateSquareCutGenerator (IntegerVariable y, IntegerVariable x, Model *model)
 
CutGenerator CreateAllDifferentCutGenerator (const std::vector< IntegerVariable > &vars, Model *model)
 
CutGenerator CreateLinMaxCutGenerator (const IntegerVariable target, const std::vector< LinearExpression > &exprs, const std::vector< IntegerVariable > &z_vars, Model *model)
 
void AddIntegerVariableFromIntervals (SchedulingConstraintHelper *helper, Model *model, std::vector< IntegerVariable > *vars)
 
std::function< void(const absl::StrongVector< IntegerVariable, double > &, LinearConstraintManager *)> GenerateCumulativeCut (const std::string &cut_name, SchedulingConstraintHelper *helper, const std::vector< IntegerVariable > &demands, AffineExpression capacity, Model *model)
 
CutGenerator CreateCumulativeCutGenerator (const std::vector< IntervalVariable > &intervals, const IntegerVariable capacity, const std::vector< IntegerVariable > &demands, Model *model)
 
CutGenerator CreateOverlappingCumulativeCutGenerator (const std::vector< IntervalVariable > &intervals, const IntegerVariable capacity, const std::vector< IntegerVariable > &demands, Model *model)
 
CutGenerator CreateNoOverlapCutGenerator (const std::vector< IntervalVariable > &intervals, Model *model)
 
CutGenerator CreateNoOverlapPrecedenceCutGenerator (const std::vector< IntervalVariable > &intervals, Model *model)
 
CutGenerator CreateCliqueCutGenerator (const std::vector< IntegerVariable > &base_variables, Model *model)
 
void AddCumulativeRelaxation (const std::vector< IntervalVariable > &x_intervals, 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::function< void(Model *)> Disjunctive (const std::vector< IntervalVariable > &vars)
 
std::function< void(Model *)> DisjunctiveWithBooleanPrecedencesOnly (const std::vector< IntervalVariable > &vars)
 
std::function< void(Model *)> DisjunctiveWithBooleanPrecedences (const std::vector< IntervalVariable > &vars)
 
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_INT_TYPE (ClauseIndex, int)
 
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)
 
EncodingNodeLazyMergeAllNodeWithPQ (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)
 
void ProcessCore (const std::vector< Literal > &core, Coefficient min_weight, std::deque< EncodingNode > *repository, std::vector< EncodingNode * > *nodes, SatSolver *solver)
 
std::vector< IntegerVariable > NegationOf (const std::vector< IntegerVariable > &vars)
 
std::function< void(Model *)> ExcludeCurrentSolutionWithoutIgnoredVariableAndBacktrack ()
 
 DEFINE_INT_TYPE (IntegerValue, int64)
 
constexpr IntegerValue kMaxIntegerValue (std::numeric_limits< IntegerValue::ValueType >::max() - 1)
 
constexpr IntegerValue kMinIntegerValue (-kMaxIntegerValue)
 
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_INT_TYPE (IntegerVariable, int32)
 
const IntegerVariable kNoIntegerVariable (-1)
 
IntegerVariable NegationOf (IntegerVariable i)
 
bool VariableIsPositive (IntegerVariable i)
 
IntegerVariable PositiveVariable (IntegerVariable i)
 
 DEFINE_INT_TYPE (PositiveOnlyIndex, int32)
 
PositiveOnlyIndex GetPositiveOnlyIndex (IntegerVariable var)
 
std::ostream & operator<< (std::ostream &os, IntegerLiteral i_lit)
 
std::function< BooleanVariable(Model *)> NewBooleanVariable ()
 
std::function< IntegerVariable(Model *)> ConstantIntegerVariable (int64 value)
 
std::function< IntegerVariable(Model *)> NewIntegerVariable (int64 lb, int64 ub)
 
std::function< IntegerVariable(Model *)> NewIntegerVariable (const Domain &domain)
 
std::function< IntegerVariable(Model *)> NewIntegerVariableFromLiteral (Literal lit)
 
std::function< int64(const Model &)> LowerBound (IntegerVariable v)
 
std::function< int64(const Model &)> UpperBound (IntegerVariable v)
 
std::function< bool(const Model &)> IsFixed (IntegerVariable v)
 
std::function< int64(const Model &)> Value (IntegerVariable v)
 
std::function< void(Model *)> GreaterOrEqual (IntegerVariable v, int64 lb)
 
std::function< void(Model *)> LowerOrEqual (IntegerVariable v, int64 ub)
 
std::function< void(Model *)> Equality (IntegerVariable v, int64 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 lb, int64 ub)
 
std::function< std::vector< IntegerEncoder::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 upper_bound)
 
template<typename VectorInt >
std::function< void(Model *)> WeightedSumGreaterOrEqual (const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 lower_bound)
 
template<typename VectorInt >
std::function< void(Model *)> FixedWeightedSum (const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 value)
 
template<typename VectorInt >
std::function< void(Model *)> ConditionalWeightedSumLowerOrEqual (const std::vector< Literal > &enforcement_literals, const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 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 lower_bound)
 
template<typename VectorInt >
std::function< void(Model *)> WeightedSumLowerOrEqualReif (Literal is_le, const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 upper_bound)
 
template<typename VectorInt >
std::function< void(Model *)> WeightedSumGreaterOrEqualReif (Literal is_ge, const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 lower_bound)
 
void LoadLinearConstraint (const LinearConstraint &cst, Model *model)
 
void LoadConditionalLinearConstraint (const absl::Span< const Literal > enforcement_literals, const LinearConstraint &cst, Model *model)
 
template<typename VectorInt >
std::function< void(Model *)> FixedWeightedSumReif (Literal is_eq, const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 value)
 
template<typename VectorInt >
std::function< void(Model *)> WeightedSumNotEqual (const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 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 (IntegerVariable a, IntegerVariable b, IntegerVariable p)
 
std::function< void(Model *)> DivisionConstraint (IntegerVariable a, IntegerVariable b, IntegerVariable c)
 
std::function< void(Model *)> FixedDivisionConstraint (IntegerVariable a, IntegerValue b, IntegerVariable 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 > &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()> PseudoCost (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 SolveIntegerProblem (Model *model)
 
SatSolver::Status ResetAndSolveIntegerProblem (const std::vector< Literal > &assumptions, Model *model)
 
SatSolver::Status SolveIntegerProblemWithLazyEncoding (Model *model)
 
SatSolver::Status ContinuousProbing (const std::vector< BooleanVariable > &bool_vars, const std::vector< IntegerVariable > &int_vars, const std::function< void()> &feasible_solution_observer, Model *model)
 
IntegerLiteral SplitDomainUsingBestSolutionValue (IntegerVariable var, Model *model)
 
 DEFINE_INT_TYPE (IntervalVariable, int32)
 
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(const Model &)> MinSize (IntervalVariable v)
 
std::function< int64(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 min_start, int64 max_end, int64 size)
 
std::function< IntervalVariable(Model *)> NewInterval (IntegerVariable start, IntegerVariable end, IntegerVariable size)
 
std::function< IntervalVariable(Model *)> NewIntervalWithVariableSize (int64 min_start, int64 max_end, int64 min_size, int64 max_size)
 
std::function< IntervalVariable(Model *)> NewOptionalInterval (int64 min_start, int64 max_end, int64 size, Literal is_present)
 
std::function< IntervalVariable(Model *)> NewOptionalIntervalWithOptionalVariables (int64 min_start, int64 max_end, int64 size, Literal is_present)
 
std::function< IntervalVariable(Model *)> NewOptionalInterval (IntegerVariable start, IntegerVariable end, IntegerVariable size, Literal is_present)
 
std::function< IntervalVariable(Model *)> NewOptionalIntervalWithVariableSize (int64 min_start, int64 max_end, int64 min_size, int64 max_size, Literal is_present)
 
std::function< void(Model *)> IntervalWithAlternatives (IntervalVariable parent, const std::vector< IntervalVariable > &members)
 
void CleanTermsAndFillConstraint (std::vector< std::pair< IntegerVariable, IntegerValue >> *terms, LinearConstraint *constraint)
 
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)
 
IntegerValue LinExprLowerBound (const LinearExpression &expr, const IntegerTrail &integer_trail)
 
IntegerValue LinExprUpperBound (const LinearExpression &expr, 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)
 
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 > demands, int64 capacity, LinearConstraintManager *manager, Model *model)
 
CutGenerator CreateStronglyConnectedGraphCutGenerator (int num_nodes, const std::vector< int > &tails, const std::vector< int > &heads, const std::vector< Literal > &literals, Model *model)
 
CutGenerator CreateCVRPCutGenerator (int num_nodes, const std::vector< int > &tails, const std::vector< int > &heads, const std::vector< Literal > &literals, const std::vector< int64 > &demands, int64 capacity, Model *model)
 
bool AppendFullEncodingRelaxation (IntegerVariable var, const Model &model, LinearRelaxation *relaxation)
 
void AppendPartialEncodingRelaxation (IntegerVariable var, const Model &model, LinearRelaxation *relaxation)
 
void AppendPartialGreaterThanEncodingRelaxation (IntegerVariable var, const Model &model, LinearRelaxation *relaxation)
 
void TryToLinearizeConstraint (const CpModelProto &model_proto, const ConstraintProto &ct, Model *model, int linearization_level, LinearRelaxation *relaxation)
 
void AddCumulativeCut (const std::vector< IntervalVariable > &intervals, const std::vector< IntegerVariable > &demands, IntegerValue capacity_upper_bound, Model *model, LinearRelaxation *relaxation)
 
void AppendCumulativeRelaxation (const CpModelProto &model_proto, const ConstraintProto &ct, int linearization_level, Model *model, LinearRelaxation *relaxation)
 
void AppendNoOverlapRelaxation (const CpModelProto &model_proto, const ConstraintProto &ct, int linearization_level, Model *model, LinearRelaxation *relaxation)
 
void AppendMaxRelaxation (IntegerVariable target, const std::vector< IntegerVariable > &vars, int linearization_level, Model *model, LinearRelaxation *relaxation)
 
std::vector< IntegerVariable > AppendLinMaxRelaxation (IntegerVariable target, const std::vector< LinearExpression > &exprs, Model *model, LinearRelaxation *relaxation)
 
void AppendLinearConstraintRelaxation (const ConstraintProto &constraint_proto, const int linearization_level, const Model &model, LinearRelaxation *relaxation)
 
std::vector< double > ScaleContinuousVariables (double scaling, double max_bound, MPModelProto *mp_model)
 
int FindRationalFactor (double x, int limit, double tolerance)
 
void RemoveNearZeroTerms (const SatParameters &params, MPModelProto *mp_model)
 
std::vector< double > DetectImpliedIntegers (bool log_info, MPModelProto *mp_model)
 
bool ConvertMPModelProtoToCpModelProto (const SatParameters &params, const MPModelProto &mp_model, CpModelProto *cp_model)
 
bool ConvertBinaryMPModelProtoToBooleanProblem (const MPModelProto &mp_model, LinearBooleanProblem *problem)
 
void ConvertBooleanProblemToLinearProgram (const LinearBooleanProblem &problem, glop::LinearProgram *lp)
 
int FixVariablesFromSat (const SatSolver &solver, glop::LinearProgram *lp)
 
bool SolveLpAndUseSolutionForSatAssignmentPreference (const glop::LinearProgram &lp, SatSolver *sat_solver, double max_time_in_seconds)
 
bool SolveLpAndUseIntegerVariableToStartLNS (const glop::LinearProgram &lp, LinearBooleanProblem *problem)
 
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, 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)
 
SatSolver::Status MinimizeWithHittingSetAndLazyEncoding (const ObjectiveDefinition &objective_definition, const std::function< void()> &feasible_solution_observer, Model *model)
 
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_INT_TYPE (Coefficient, int64)
 
const Coefficient kCoefficientMax (std::numeric_limits< Coefficient::ValueType >::max())
 
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 offset)
 
std::function< void(Model *)> Sum2LowerOrEqual (IntegerVariable a, IntegerVariable b, int64 ub)
 
std::function< void(Model *)> ConditionalSum2LowerOrEqual (IntegerVariable a, IntegerVariable b, int64 ub, const std::vector< Literal > &enforcement_literals)
 
std::function< void(Model *)> Sum3LowerOrEqual (IntegerVariable a, IntegerVariable b, IntegerVariable c, int64 ub)
 
std::function< void(Model *)> ConditionalSum3LowerOrEqual (IntegerVariable a, IntegerVariable b, IntegerVariable c, int64 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 offset)
 
std::function< void(Model *)> ConditionalLowerOrEqualWithOffset (IntegerVariable a, IntegerVariable b, int64 offset, Literal is_le)
 
std::function< void(Model *)> ConditionalLowerOrEqual (IntegerVariable a, IntegerVariable b, Literal is_le)
 
std::function< void(Model *)> ConditionalLowerOrEqual (IntegerVariable a, IntegerVariable b, absl::Span< const Literal > literals)
 
std::function< void(Model *)> ReifiedLowerOrEqualWithOffset (IntegerVariable a, IntegerVariable b, int64 offset, Literal is_le)
 
std::function< void(Model *)> ReifiedEquality (IntegerVariable a, IntegerVariable b, Literal is_eq)
 
std::function< void(Model *)> ReifiedEqualityWithOffset (IntegerVariable a, IntegerVariable b, int64 offset, Literal is_eq)
 
std::function< void(Model *)> NotEqual (IntegerVariable a, IntegerVariable b)
 
void SubstituteVariable (int var, int64 var_coeff_in_definition, const ConstraintProto &definition, ConstraintProto *ct)
 
bool LookForTrivialSatSolution (double deterministic_time_limit, Model *model, bool log_info)
 
bool FailedLiteralProbingRound (ProbingOptions options, Model *model)
 
std::vector< PseudoCosts::VariableBoundChangeGetBoundChanges (LiteralIndex decision, 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)
 
 DEFINE_INT_TYPE (BooleanVariable, int)
 
const BooleanVariable kNoBooleanVariable (-1)
 
 DEFINE_INT_TYPE (LiteralIndex, int)
 
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 lower_bound, int64 upper_bound, std::vector< LiteralWithCoeff > *cst)
 
std::function< void(Model *)> CardinalityConstraint (int64 lower_bound, int64 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(const Model &)> Value (Literal l)
 
std::function< int64(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)
 
bool SimplifyClause (const std::vector< Literal > &a, std::vector< Literal > *b, LiteralIndex *opposite_literal, int64 *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)
 
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)
 
std::string ExtractWorkerName (const std::string &improvement_info)
 
void AddTableConstraint (absl::Span< const IntegerVariable > vars, std::vector< std::vector< int64 >> tuples, Model *model)
 
void AddNegatedTableConstraint (absl::Span< const IntegerVariable > vars, std::vector< std::vector< int64 >> tuples, Model *model)
 
std::function< void(Model *)> LiteralTableConstraint (const std::vector< std::vector< Literal >> &literal_tuples, const std::vector< Literal > &line_literals)
 
std::function< void(Model *)> TransitionConstraint (const std::vector< IntegerVariable > &vars, const std::vector< std::vector< int64 >> &automaton, int64 initial_state, const std::vector< int64 > &final_states)
 
template<typename IntegerType >
constexpr IntegerType IntegerTypeMinimumValue ()
 
template<>
constexpr IntegerValue IntegerTypeMinimumValue ()
 
void AddReservoirConstraint (std::vector< AffineExpression > times, std::vector< IntegerValue > deltas, std::vector< Literal > presences, int64 min_level, int64 max_level, Model *model)
 
int MoveOneUnprocessedLiteralLast (const std::set< LiteralIndex > &processed, int relevant_prefix_size, std::vector< Literal > *literals)
 
void CompressTuples (absl::Span< const int64 > domain_sizes, int64 any_value, std::vector< std::vector< int64 >> *tuples)
 
template<typename URBG >
void RandomizeDecisionHeuristic (URBG *random, SatParameters *parameters)
 
void DetectDominanceRelations (const PresolveContext &context, VarDomination *var_domination, DualBoundStrengthening *dual_bound_strengthening)
 
bool ExploitDominanceRelations (const VarDomination &var_domination, PresolveContext *context)
 

Variables

constexpr int kObjectiveConstraint = -1
 
constexpr int kAffineRelationConstraint = -2
 
constexpr int kAssumptionsConstraint = -3
 
const int kUnsatTrailIndex = -1
 

Typedef Documentation

◆ InlinedIntegerLiteralVector

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

Definition at line 198 of file integer.h.

Enumeration Type Documentation

◆ LogBehavior

Enumerator
DEFAULT_LOG 
STDOUT_LOG 

Definition at line 47 of file optimization.h.

◆ SatFormat

enum SatFormat
Enumerator
DIMACS 
DRAT 

Definition at line 326 of file drat_checker.h.

Function Documentation

◆ AddCumulativeCut()

void operations_research::sat::AddCumulativeCut ( const std::vector< IntervalVariable > &  intervals,
const std::vector< IntegerVariable > &  demands,
IntegerValue  capacity_upper_bound,
Model model,
LinearRelaxation relaxation 
)

Definition at line 513 of file linear_relaxation.cc.

◆ AddCumulativeEnergyConstraint()

void AddCumulativeEnergyConstraint ( std::vector< AffineExpression energies,
AffineExpression  capacity,
SchedulingConstraintHelper helper,
Model model 
)

Definition at line 27 of file cumulative_energy.cc.

◆ AddCumulativeOverloadChecker()

void AddCumulativeOverloadChecker ( const std::vector< AffineExpression > &  demands,
AffineExpression  capacity,
SchedulingConstraintHelper helper,
Model model 
)

Definition at line 40 of file cumulative_energy.cc.

◆ AddCumulativeRelaxation()

void AddCumulativeRelaxation ( const std::vector< IntervalVariable > &  x_intervals,
SchedulingConstraintHelper x,
SchedulingConstraintHelper y,
Model model 
)

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

◆ AddInferedAndDeletedClauses()

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

Definition at line 550 of file drat_checker.cc.

◆ AddIntegerVariableFromIntervals()

void operations_research::sat::AddIntegerVariableFromIntervals ( SchedulingConstraintHelper helper,
Model model,
std::vector< IntegerVariable > *  vars 
)

Definition at line 1984 of file cuts.cc.

◆ AddNegatedTableConstraint()

void AddNegatedTableConstraint ( absl::Span< const IntegerVariable >  vars,
std::vector< std::vector< int64 >>  tuples,
Model model 
)

Definition at line 457 of file sat/table.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 337 of file boolean_problem.cc.

◆ AddObjectiveUpperBound()

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

Definition at line 329 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 501 of file drat_checker.cc.

◆ AddProductTo()

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

Definition at line 110 of file integer.h.

◆ AddReservoirConstraint()

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

Definition at line 27 of file timetable.cc.

◆ AddTableConstraint()

void AddTableConstraint ( absl::Span< const IntegerVariable >  vars,
std::vector< std::vector< int64 >>  tuples,
Model model 
)

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

◆ AllDifferentAC()

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

Definition at line 76 of file all_different.cc.

◆ AllDifferentBinary()

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

Definition at line 31 of file all_different.cc.

◆ AllDifferentOnBounds()

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

Definition at line 65 of file all_different.cc.

◆ AllValuesInDomain()

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

Definition at line 116 of file cp_model_utils.h.

◆ AppendCumulativeRelaxation()

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

Definition at line 605 of file linear_relaxation.cc.

◆ AppendFullEncodingRelaxation()

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

Definition at line 33 of file linear_relaxation.cc.

◆ AppendLinearConstraintRelaxation()

void AppendLinearConstraintRelaxation ( const ConstraintProto &  constraint_proto,
const int  linearization_level,
const Model model,
LinearRelaxation relaxation 
)

Definition at line 810 of file linear_relaxation.cc.

◆ AppendLinMaxRelaxation()

std::vector< IntegerVariable > AppendLinMaxRelaxation ( IntegerVariable  target,
const std::vector< LinearExpression > &  exprs,
Model model,
LinearRelaxation relaxation 
)

Definition at line 713 of file linear_relaxation.cc.

◆ AppendMaxRelaxation()

void AppendMaxRelaxation ( IntegerVariable  target,
const std::vector< IntegerVariable > &  vars,
int  linearization_level,
Model model,
LinearRelaxation relaxation 
)

Definition at line 639 of file linear_relaxation.cc.

◆ AppendNoOverlapRelaxation()

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

Definition at line 624 of file linear_relaxation.cc.

◆ AppendPartialEncodingRelaxation()

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

Definition at line 110 of file linear_relaxation.cc.

◆ AppendPartialGreaterThanEncodingRelaxation()

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

Definition at line 185 of file linear_relaxation.cc.

◆ ApplyLiteralMapping()

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

Definition at line 103 of file pb_constraint.cc.

◆ ApplyLiteralMappingToBooleanProblem()

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

Definition at line 743 of file boolean_problem.cc.

◆ ApplyToAllIntervalIndices()

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

Definition at line 336 of file cp_model_utils.cc.

◆ ApplyToAllLiteralIndices()

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

Definition at line 166 of file cp_model_utils.cc.

◆ ApplyToAllVariableIndices()

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

Definition at line 233 of file cp_model_utils.cc.

◆ ApplyVariableMapping()

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

Definition at line 5491 of file cp_model_presolve.cc.

◆ AtMinValue()

IntegerLiteral AtMinValue ( IntegerVariable  var,
IntegerTrail integer_trail 
)

Definition at line 39 of file integer_search.cc.

◆ AtMostOneConstraint()

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

Definition at line 890 of file sat_solver.h.

◆ BasicOrbitopeExtraction()

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

Definition at line 21 of file symmetry_util.cc.

◆ BooleanLinearConstraint()

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

Definition at line 852 of file sat_solver.h.

◆ BooleanLinearExpressionIsCanonical()

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

Definition at line 136 of file pb_constraint.cc.

◆ BooleanProblemToCpModelproto()

CpModelProto BooleanProblemToCpModelproto ( const LinearBooleanProblem &  problem)

Definition at line 152 of file boolean_problem.cc.

◆ CanBeFilteredUsingCutLowerBound()

bool CanBeFilteredUsingCutLowerBound ( const LinearConstraint preprocessed_constraint,
const absl::StrongVector< IntegerVariable, double > &  lp_values,
const IntegerTrail integer_trail 
)

Definition at line 290 of file cuts.cc.

◆ CanBeFilteredUsingKnapsackUpperBound()

bool CanBeFilteredUsingKnapsackUpperBound ( const LinearConstraint constraint,
const absl::StrongVector< IntegerVariable, double > &  lp_values,
const IntegerTrail integer_trail 
)

Definition at line 336 of file cuts.cc.

◆ CanFormValidKnapsackCover()

bool CanFormValidKnapsackCover ( const LinearConstraint preprocessed_constraint,
const absl::StrongVector< IntegerVariable, double > &  lp_values,
const IntegerTrail integer_trail 
)

Definition at line 370 of file cuts.cc.

◆ CanonicalizeConstraint()

void CanonicalizeConstraint ( LinearConstraint ct)

Definition at line 244 of file linear_constraint.cc.

◆ CanonicalizeExpr()

LinearExpression CanonicalizeExpr ( const LinearExpression expr)

Definition at line 278 of file linear_constraint.cc.

◆ CardinalityConstraint()

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

Definition at line 861 of file sat_solver.h.

◆ CeilRatio()

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

Definition at line 81 of file integer.h.

◆ ChangeOptimizationDirection()

void ChangeOptimizationDirection ( LinearBooleanProblem *  problem)

Definition at line 209 of file boolean_problem.cc.

◆ ChooseBestObjectiveValue()

IntegerLiteral ChooseBestObjectiveValue ( IntegerVariable  var,
Model model 
)

Definition at line 47 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 513 of file circuit.cc.

◆ ClauseConstraint()

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

Definition at line 904 of file sat_solver.h.

◆ CleanTermsAndFillConstraint()

void CleanTermsAndFillConstraint ( std::vector< std::pair< IntegerVariable, IntegerValue >> *  terms,
LinearConstraint constraint 
)

Definition at line 83 of file linear_constraint.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 639 of file integer_search.cc.

◆ CompressTuples()

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

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

◆ ComputeActivity()

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

Definition at line 122 of file linear_constraint.cc.

◆ ComputeBooleanLinearExpressionCanonicalForm()

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

Definition at line 41 of file pb_constraint.cc.

◆ ComputeCanonicalRhs()

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

Definition at line 160 of file pb_constraint.cc.

◆ ComputeCoreMinWeight()

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

Definition at line 418 of file encoding.cc.

◆ ComputeInfinityNorm()

IntegerValue ComputeInfinityNorm ( const LinearConstraint constraint)

Definition at line 142 of file linear_constraint.cc.

◆ ComputeInnerObjective()

int64 ComputeInnerObjective ( const CpObjectiveProto &  objective,
const CpSolverResponse &  response 
)

Definition at line 538 of file cp_model_utils.cc.

◆ ComputeL2Norm()

double ComputeL2Norm ( const LinearConstraint constraint)

Definition at line 134 of file linear_constraint.cc.

◆ ComputeNegatedCanonicalRhs()

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

Definition at line 178 of file pb_constraint.cc.

◆ ComputeObjectiveValue()

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

Definition at line 347 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 1013 of file simplification.cc.

◆ ComputeResolvantSize()

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

Definition at line 1048 of file simplification.cc.

◆ ConditionalLowerOrEqual() [1/2]

std::function<void(Model*)> operations_research::sat::ConditionalLowerOrEqual ( IntegerVariable  a,
IntegerVariable  b,
absl::Span< const Literal literals 
)
inline

Definition at line 435 of file precedences.h.

◆ ConditionalLowerOrEqual() [2/2]

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

Definition at line 428 of file precedences.h.

◆ ConditionalLowerOrEqualWithOffset()

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

Definition at line 419 of file precedences.h.

◆ ConditionalSum2LowerOrEqual()

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

Definition at line 359 of file precedences.h.

◆ ConditionalSum3LowerOrEqual()

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

Definition at line 381 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  lower_bound 
)
inline

Definition at line 514 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  upper_bound 
)
inline

Definition at line 426 of file integer_expr.h.

◆ ConfigureSearchHeuristics()

void ConfigureSearchHeuristics ( Model model)

Definition at line 527 of file integer_search.cc.

◆ ConstantIntegerVariable()

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

Definition at line 1418 of file integer.h.

◆ ConstraintCaseName()

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

Definition at line 401 of file cp_model_utils.cc.

◆ ConstraintIsTriviallyTrue()

bool ConstraintIsTriviallyTrue ( const LinearConstraint constraint,
const IntegerTrail integer_trail 
)

Definition at line 274 of file cuts.cc.

◆ ConstructSearchStrategy()

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

Definition at line 173 of file cp_model_search.cc.

◆ ConstructSearchStrategyInternal()

const std::function<BooleanOrIntegerLiteral()> operations_research::sat::ConstructSearchStrategyInternal ( const absl::flat_hash_map< int, std::pair< int64, int64 >> &  var_to_coeff_offset_pair,
const std::vector< Strategy > &  strategies,
Model model 
)

Definition at line 42 of file cp_model_search.cc.

◆ ContainsLiteral()

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

Definition at line 460 of file drat_checker.cc.

◆ ContinuousProbing()

SatSolver::Status ContinuousProbing ( const std::vector< BooleanVariable > &  bool_vars,
const std::vector< IntegerVariable > &  int_vars,
const std::function< void()> &  feasible_solution_observer,
Model model 
)

Definition at line 926 of file integer_search.cc.

◆ ConvertBinaryMPModelProtoToBooleanProblem()

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

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

◆ ConvertBooleanProblemToLinearProgram()

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

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

◆ ConvertMPModelProtoToCpModelProto()

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

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

◆ ConvertToKnapsackForm()

void ConvertToKnapsackForm ( const LinearConstraint constraint,
std::vector< LinearConstraint > *  knapsack_constraints,
IntegerTrail integer_trail 
)

Definition at line 388 of file cuts.cc.

◆ CpModelStats()

std::string CpModelStats ( const CpModelProto &  model_proto)

Returns a string with some statistics on the given CpModelProto.

Definition at line 151 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 286 of file cp_model_solver.cc.

◆ CreateAllDifferentCutGenerator()

CutGenerator CreateAllDifferentCutGenerator ( const std::vector< IntegerVariable > &  vars,
Model model 
)

Definition at line 1818 of file cuts.cc.

◆ CreateCliqueCutGenerator()

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

Definition at line 2411 of file cuts.cc.

◆ CreateCumulativeCutGenerator()

CutGenerator CreateCumulativeCutGenerator ( const std::vector< IntervalVariable > &  intervals,
const IntegerVariable  capacity,
const std::vector< IntegerVariable > &  demands,
Model model 
)

Definition at line 2198 of file cuts.cc.

◆ CreateCVRPCutGenerator()

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

Definition at line 2557 of file linear_programming_constraint.cc.

◆ CreateInitialEncodingNodes() [1/2]

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

Definition at line 327 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 302 of file encoding.cc.

◆ CreateKnapsackCoverCutGenerator()

CutGenerator CreateKnapsackCoverCutGenerator ( const std::vector< LinearConstraint > &  base_constraints,
const std::vector< IntegerVariable > &  vars,
Model model 
)

Definition at line 437 of file cuts.cc.

◆ CreateLinMaxCutGenerator()

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

Definition at line 1915 of file cuts.cc.

◆ CreateNoOverlapCutGenerator()

CutGenerator CreateNoOverlapCutGenerator ( const std::vector< IntervalVariable > &  intervals,
Model model 
)

Definition at line 2331 of file cuts.cc.

◆ CreateNoOverlapPrecedenceCutGenerator()

CutGenerator CreateNoOverlapPrecedenceCutGenerator ( const std::vector< IntervalVariable > &  intervals,
Model model 
)

Definition at line 2348 of file cuts.cc.

◆ CreateOverlappingCumulativeCutGenerator()

CutGenerator CreateOverlappingCumulativeCutGenerator ( const std::vector< IntervalVariable > &  intervals,
const IntegerVariable  capacity,
const std::vector< IntegerVariable > &  demands,
Model model 
)

Definition at line 2217 of file cuts.cc.

◆ CreatePositiveMultiplicationCutGenerator()

CutGenerator CreatePositiveMultiplicationCutGenerator ( IntegerVariable  z,
IntegerVariable  x,
IntegerVariable  y,
Model model 
)

Definition at line 1328 of file cuts.cc.

◆ CreateSquareCutGenerator()

CutGenerator CreateSquareCutGenerator ( IntegerVariable  y,
IntegerVariable  x,
Model model 
)

Definition at line 1424 of file cuts.cc.

◆ CreateStronglyConnectedGraphCutGenerator()

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

Definition at line 2541 of file linear_programming_constraint.cc.

◆ Cumulative()

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

Definition at line 35 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 153 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 234 of file cumulative.cc.

◆ DEFINE_INT_TYPE() [1/8]

operations_research::sat::DEFINE_INT_TYPE ( BooleanVariable  ,
int   
)

◆ DEFINE_INT_TYPE() [2/8]

operations_research::sat::DEFINE_INT_TYPE ( ClauseIndex  ,
int   
)

◆ DEFINE_INT_TYPE() [3/8]

operations_research::sat::DEFINE_INT_TYPE ( Coefficient  ,
int64   
)

◆ DEFINE_INT_TYPE() [4/8]

operations_research::sat::DEFINE_INT_TYPE ( IntegerValue  ,
int64   
)

◆ DEFINE_INT_TYPE() [5/8]

operations_research::sat::DEFINE_INT_TYPE ( IntegerVariable  ,
int32   
)

◆ DEFINE_INT_TYPE() [6/8]

operations_research::sat::DEFINE_INT_TYPE ( IntervalVariable  ,
int32   
)

◆ DEFINE_INT_TYPE() [7/8]

operations_research::sat::DEFINE_INT_TYPE ( LiteralIndex  ,
int   
)

◆ DEFINE_INT_TYPE() [8/8]

operations_research::sat::DEFINE_INT_TYPE ( PositiveOnlyIndex  ,
int32   
)

◆ DetectAndAddSymmetryToProto()

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

Definition at line 458 of file cp_model_symmetries.cc.

◆ DetectAndExploitSymmetriesInPresolve()

bool DetectAndExploitSymmetriesInPresolve ( PresolveContext context)

Definition at line 497 of file cp_model_symmetries.cc.

◆ DetectDominanceRelations()

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

Definition at line 751 of file var_domination.cc.

◆ DetectEquivalencesInElementConstraint()

bool operations_research::sat::DetectEquivalencesInElementConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1434 of file cp_model_loader.cc.

◆ DetectImpliedIntegers()

std::vector< double > DetectImpliedIntegers ( bool  log_info,
MPModelProto *  mp_model 
)

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

◆ DeterministicLoop()

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

Definition at line 84 of file subsolver.cc.

◆ DifferAtGivenLiteral()

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

Definition at line 979 of file simplification.cc.

◆ Disjunctive()

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

Definition at line 30 of file disjunctive.cc.

◆ DisjunctiveWithBooleanPrecedences()

std::function< void(Model *)> DisjunctiveWithBooleanPrecedences ( const std::vector< IntervalVariable > &  vars)

Definition at line 155 of file disjunctive.cc.

◆ DisjunctiveWithBooleanPrecedencesOnly()

std::function< void(Model *)> DisjunctiveWithBooleanPrecedencesOnly ( const std::vector< IntervalVariable > &  vars)

Definition at line 132 of file disjunctive.cc.

◆ DivideByGCD()

void DivideByGCD ( LinearConstraint constraint)

Definition at line 189 of file linear_constraint.cc.

◆ DivisionConstraint()

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

Definition at line 810 of file integer_expr.h.

◆ DomainInProtoContains()

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

Definition at line 82 of file cp_model_utils.h.

◆ EncodeObjectiveAsSingleVariable()

void EncodeObjectiveAsSingleVariable ( CpModelProto *  cp_model)

Definition at line 21 of file cp_model_objective.cc.

◆ EndVar()

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

Definition at line 594 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 950 of file sat_solver.h.

◆ EnforcementLiteral()

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

Definition at line 40 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 400 of file precedences.h.

◆ Equality() [2/3]

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

Definition at line 1524 of file integer.h.

◆ Equality() [3/3]

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

Definition at line 926 of file sat_solver.h.

◆ EqualityWithOffset()

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

Definition at line 409 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 290 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 266 of file scheduling_constraints.cc.

◆ ExactlyOneConstraint()

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

Definition at line 876 of file sat_solver.h.

◆ ExactlyOnePerRowAndPerColumn()

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

Definition at line 452 of file circuit.cc.

◆ ExcludeCurrentSolutionAndBacktrack()

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

Definition at line 1015 of file sat_solver.h.

◆ ExcludeCurrentSolutionWithoutIgnoredVariableAndBacktrack()

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

Definition at line 1989 of file integer.cc.

◆ ExpandCpModel()

void ExpandCpModel ( PresolveContext context)

Definition at line 1400 of file cp_model_expand.cc.

◆ ExploitDominanceRelations()

bool ExploitDominanceRelations ( const VarDomination var_domination,
PresolveContext context 
)

Definition at line 946 of file var_domination.cc.

◆ ExtractAssignment()

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

Definition at line 51 of file boolean_problem.cc.

◆ ExtractSubproblem()

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

Definition at line 487 of file boolean_problem.cc.

◆ ExtractWorkerName()

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

Definition at line 567 of file synchronization.cc.

◆ FailedLiteralProbingRound()

bool FailedLiteralProbingRound ( ProbingOptions  options,
Model model 
)

Definition at line 350 of file probing.cc.

◆ FillDomainInProto()

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

Definition at line 91 of file cp_model_utils.h.

◆ FindCpModelSymmetries()

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

Definition at line 373 of file cp_model_symmetries.cc.

◆ FindDuplicateConstraints()

std::vector< int > FindDuplicateConstraints ( const CpModelProto &  model_proto)

Definition at line 5592 of file cp_model_presolve.cc.

◆ FindLinearBooleanProblemSymmetries()

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

Definition at line 671 of file boolean_problem.cc.

◆ FindRationalFactor()

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

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

◆ FirstUnassignedVarAtItsMinHeuristic()

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

Definition at line 153 of file integer_search.cc.

◆ FixedDivisionConstraint()

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

Definition at line 823 of file integer_expr.h.

◆ FixedWeightedSum()

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

Definition at line 415 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  value 
)
inline

Definition at line 602 of file integer_expr.h.

◆ FixVariablesFromSat()

int FixVariablesFromSat ( const SatSolver solver,
glop::LinearProgram lp 
)

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

◆ FloorRatio()

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

Definition at line 90 of file integer.h.

◆ FollowHint()

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

Definition at line 469 of file integer_search.cc.

◆ FullMerge()

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

Definition at line 212 of file encoding.cc.

◆ FullyEncodeVariable()

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

Definition at line 1587 of file integer.h.

◆ GenerateCumulativeCut()

std::function<void(const absl::StrongVector<IntegerVariable, double>&, LinearConstraintManager*)> operations_research::sat::GenerateCumulativeCut ( const std::string &  cut_name,
SchedulingConstraintHelper helper,
const std::vector< IntegerVariable > &  demands,
AffineExpression  capacity,
Model model 
)

Definition at line 2019 of file cuts.cc.

◆ GenerateGraphForSymmetryDetection()

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

Definition at line 533 of file boolean_problem.cc.

◆ GenerateSchedulingNeighborhoodForRelaxation()

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

Definition at line 560 of file cp_model_lns.cc.

◆ GetBoundChanges()

std::vector< PseudoCosts::VariableBoundChange > GetBoundChanges ( LiteralIndex  decision,
Model model 
)

Definition at line 99 of file pseudo_costs.cc.

◆ GetCoefficient()

IntegerValue GetCoefficient ( const IntegerVariable  var,
const LinearExpression expr 
)

Definition at line 336 of file linear_constraint.cc.

◆ GetCoefficientOfPositiveVar()

IntegerValue GetCoefficientOfPositiveVar ( const IntegerVariable  var,
const LinearExpression expr 
)

Definition at line 348 of file linear_constraint.cc.

◆ GetDiverseSetOfParameters()

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

Definition at line 292 of file cp_model_search.cc.

◆ GetExprFromProto()

LinearExpression GetExprFromProto ( const LinearExpressionProto &  expr_proto,
const CpModelMapping mapping 
)

Definition at line 1348 of file cp_model_loader.cc.

◆ GetFactorT()

IntegerValue GetFactorT ( IntegerValue  rhs_remainder,
IntegerValue  divisor,
IntegerValue  max_t 
)

Definition at line 616 of file cuts.cc.

◆ GetKnapsackUpperBound()

double GetKnapsackUpperBound ( std::vector< KnapsackItem items,
const double  capacity 
)

Definition at line 318 of file cuts.cc.

◆ GetOrbitopeOrbits()

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

Definition at line 176 of file symmetry_util.cc.

◆ GetOrbits()

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

Definition at line 144 of file symmetry_util.cc.

◆ GetPositiveOnlyIndex()

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

Definition at line 140 of file integer.h.

◆ GetPreprocessedLinearConstraint()

LinearConstraint GetPreprocessedLinearConstraint ( const LinearConstraint constraint,
const absl::StrongVector< IntegerVariable, double > &  lp_values,
const IntegerTrail integer_trail 
)

Definition at line 250 of file cuts.cc.

◆ GetReferencesUsedByConstraint()

IndexReferences GetReferencesUsedByConstraint ( const ConstraintProto &  ct)

Definition at line 40 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 99 of file rins.cc.

◆ GetSquareMatrixFromIntegerVariables()

std::vector<std::vector<Literal> > operations_research::sat::GetSquareMatrixFromIntegerVariables ( const std::vector< IntegerVariable > &  vars,
Model m 
)

Definition at line 1786 of file cp_model_loader.cc.

◆ GetSuperAdditiveRoundingFunction()

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

Definition at line 624 of file cuts.cc.

◆ GreaterOrEqual() [1/2]

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

Definition at line 392 of file precedences.h.

◆ GreaterOrEqual() [2/2]

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

Definition at line 1495 of file integer.h.

◆ GreaterOrEqualToMiddleValue()

IntegerLiteral GreaterOrEqualToMiddleValue ( IntegerVariable  var,
IntegerTrail integer_trail 
)

Definition at line 59 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 123 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 136 of file cp_constraints.h.

◆ HasEnforcementLiteral()

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

Definition at line 37 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 1537 of file integer.h.

◆ Implication() [2/2]

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

Definition at line 919 of file sat_solver.h.

◆ ImpliesInInterval()

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

Definition at line 1564 of file integer.h.

◆ IncreaseNodeSize()

void IncreaseNodeSize ( EncodingNode node,
SatSolver solver 
)

Definition at line 116 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 231 of file cp_model_search.cc.

◆ IntegerTypeMinimumValue() [1/2]

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

Definition at line 94 of file theta_tree.h.

◆ IntegerTypeMinimumValue() [2/2]

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

Definition at line 98 of file theta_tree.h.

◆ IntegerValueSelectionHeuristic()

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

Definition at line 259 of file integer_search.cc.

◆ IntervalWithAlternatives()

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

Definition at line 712 of file intervals.h.

◆ IntTypeAbs()

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

Definition at line 77 of file integer.h.

◆ IsAssignmentValid()

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

Definition at line 361 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 741 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 689 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 672 of file integer_expr.h.

◆ IsFixed()

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

Definition at line 1479 of file integer.h.

◆ IsOneOf()

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

Definition at line 875 of file integer_expr.cc.

◆ IsOptional()

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

Definition at line 619 of file intervals.h.

◆ IsPresentLiteral()

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

Definition at line 625 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)
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 106 of file encoding.cc.

◆ LazyMergeAllNodeWithPQ()

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

Definition at line 285 of file encoding.cc.

◆ LiftKnapsackCut()

bool LiftKnapsackCut ( const LinearConstraint constraint,
const absl::StrongVector< IntegerVariable, double > &  lp_values,
const std::vector< IntegerValue > &  cut_vars_original_coefficients,
const IntegerTrail integer_trail,
TimeLimit time_limit,
LinearConstraint cut 
)

Definition at line 172 of file cuts.cc.

◆ LinearBooleanProblemToCnfString()

std::string LinearBooleanProblemToCnfString ( const LinearBooleanProblem &  problem)

Definition at line 391 of file boolean_problem.cc.

◆ LinearizedPartIsLarge()

bool LinearizedPartIsLarge ( Model model)

Definition at line 246 of file integer_search.cc.

◆ LinExprLowerBound()

IntegerValue LinExprLowerBound ( const LinearExpression expr,
const IntegerTrail integer_trail 
)

Definition at line 293 of file linear_constraint.cc.

◆ LinExprUpperBound()

IntegerValue LinExprUpperBound ( const LinearExpression expr,
const IntegerTrail integer_trail 
)

Definition at line 303 of file linear_constraint.cc.

◆ LiteralTableConstraint()

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

Definition at line 544 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 111 of file cp_constraints.h.

◆ LoadAllDiffConstraint()

void LoadAllDiffConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1287 of file cp_model_loader.cc.

◆ LoadAndConsumeBooleanProblem()

bool LoadAndConsumeBooleanProblem ( LinearBooleanProblem *  problem,
SatSolver solver 
)

Definition at line 260 of file boolean_problem.cc.

◆ LoadAtMostOneConstraint()

void LoadAtMostOneConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1044 of file cp_model_loader.cc.

◆ LoadAutomatonConstraint()

void LoadAutomatonConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1764 of file cp_model_loader.cc.

◆ LoadBoolAndConstraint()

void LoadBoolAndConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1030 of file cp_model_loader.cc.

◆ LoadBooleanProblem()

bool LoadBooleanProblem ( const LinearBooleanProblem &  problem,
SatSolver solver 
)

Definition at line 220 of file boolean_problem.cc.

◆ LoadBoolOrConstraint()

void LoadBoolOrConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1021 of file cp_model_loader.cc.

◆ LoadBoolXorConstraint()

void LoadBoolXorConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1056 of file cp_model_loader.cc.

◆ LoadCircuitConstraint()

void LoadCircuitConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1816 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 572 of file integer_expr.h.

◆ LoadConstraint()

bool LoadConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1841 of file cp_model_loader.cc.

◆ LoadCumulativeConstraint()

void LoadCumulativeConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1398 of file cp_model_loader.cc.

◆ LoadElementConstraint()

void LoadElementConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1666 of file cp_model_loader.cc.

◆ LoadElementConstraintAC()

void LoadElementConstraintAC ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1544 of file cp_model_loader.cc.

◆ LoadElementConstraintBounds()

void LoadElementConstraintBounds ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1492 of file cp_model_loader.cc.

◆ LoadExactlyOneConstraint()

void LoadExactlyOneConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1050 of file cp_model_loader.cc.

◆ LoadIntDivConstraint()

void LoadIntDivConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1323 of file cp_model_loader.cc.

◆ LoadIntMaxConstraint()

void LoadIntMaxConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1373 of file cp_model_loader.cc.

◆ LoadIntMinConstraint()

void LoadIntMinConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1340 of file cp_model_loader.cc.

◆ LoadIntProdConstraint()

void LoadIntProdConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1314 of file cp_model_loader.cc.

◆ LoadInverseConstraint()

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

◆ LoadLinearConstraint() [1/2]

void LoadLinearConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1136 of file cp_model_loader.cc.

◆ LoadLinearConstraint() [2/2]

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

Definition at line 552 of file integer_expr.h.

◆ LoadLinMaxConstraint()

void LoadLinMaxConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1359 of file cp_model_loader.cc.

◆ LoadNoOverlap2dConstraint()

void LoadNoOverlap2dConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1386 of file cp_model_loader.cc.

◆ LoadNoOverlapConstraint()

void LoadNoOverlapConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1381 of file cp_model_loader.cc.

◆ LoadReservoirConstraint()

void LoadReservoirConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1411 of file cp_model_loader.cc.

◆ LoadRoutesConstraint()

void LoadRoutesConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1828 of file cp_model_loader.cc.

◆ LoadTableConstraint()

void LoadTableConstraint ( const ConstraintProto &  ct,
Model m 
)

Definition at line 1743 of file cp_model_loader.cc.

◆ LogInfoFromContext()

void operations_research::sat::LogInfoFromContext ( const PresolveContext context)

Definition at line 5120 of file cp_model_presolve.cc.

◆ LookForTrivialSatSolution()

bool LookForTrivialSatSolution ( double  deterministic_time_limit,
Model model,
bool  log_info 
)

Definition at line 270 of file probing.cc.

◆ LowerBound()

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

Definition at line 1467 of file integer.h.

◆ LowerOrEqual() [1/2]

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

Definition at line 334 of file precedences.h.

◆ LowerOrEqual() [2/2]

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

Definition at line 1509 of file integer.h.

◆ LowerOrEqualWithOffset()

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

Definition at line 342 of file precedences.h.

◆ MakeAllCoefficientsPositive()

void MakeAllCoefficientsPositive ( LinearConstraint constraint)

Definition at line 216 of file linear_constraint.cc.

◆ MakeAllLiteralsPositive()

void MakeAllLiteralsPositive ( LinearBooleanProblem *  problem)

Definition at line 636 of file boolean_problem.cc.

◆ MakeAllVariablesPositive()

void MakeAllVariablesPositive ( LinearConstraint constraint)

Definition at line 227 of file linear_constraint.cc.

◆ MaxNodeWeightSmallerThan()

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

Definition at line 433 of file encoding.cc.

◆ MaxSize()

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

Definition at line 613 of file intervals.h.

◆ MaybeFullyEncodeMoreVariables()

void MaybeFullyEncodeMoreVariables ( const CpModelProto &  model_proto,
Model m 
)

Definition at line 1012 of file cp_model_loader.cc.

◆ MergeAllNodesWithDeque()

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

Definition at line 263 of file encoding.cc.

◆ MinimizeCore()

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

Definition at line 2547 of file sat_solver.cc.

◆ MinimizeCoreWithPropagation()

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

Definition at line 218 of file optimization.cc.

◆ MinimizeIntegerVariableWithLinearScanAndLazyEncoding()

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

Definition at line 1058 of file optimization.cc.

◆ MinimizeWithHittingSetAndLazyEncoding()

SatSolver::Status MinimizeWithHittingSetAndLazyEncoding ( const ObjectiveDefinition objective_definition,
const std::function< void()> &  feasible_solution_observer,
Model model 
)

Definition at line 1757 of file optimization.cc.

◆ MinSize()

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

Definition at line 607 of file intervals.h.

◆ MoveOneUnprocessedLiteralLast()

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

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

◆ NegatedRef()

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

Definition at line 32 of file cp_model_utils.h.

◆ NegationOf() [1/3]

LinearExpression NegationOf ( const LinearExpression expr)

Definition at line 313 of file linear_constraint.cc.

◆ NegationOf() [2/3]

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

Definition at line 27 of file integer.cc.

◆ NegationOf() [3/3]

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

Definition at line 126 of file integer.h.

◆ NewBooleanVariable()

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

Definition at line 1412 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.

Definition at line 913 of file cp_model_solver.cc.

◆ NewIntegerVariable() [1/2]

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

Definition at line 1435 of file integer.h.

◆ NewIntegerVariable() [2/2]

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

Definition at line 1426 of file integer.h.

◆ NewIntegerVariableFromLiteral()

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

Definition at line 1444 of file integer.h.

◆ NewInterval() [1/2]

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

Definition at line 632 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 643 of file intervals.h.

◆ NewIntervalWithVariableSize()

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

Definition at line 651 of file intervals.h.

◆ NewOptionalInterval() [1/2]

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

Definition at line 662 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 689 of file intervals.h.

◆ NewOptionalIntervalWithOptionalVariables()

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

Definition at line 673 of file intervals.h.

◆ NewOptionalIntervalWithVariableSize()

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

Definition at line 699 of file intervals.h.

◆ NewSatParameters() [1/3]

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

Definition at line 933 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 922 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 641 of file integer_expr.h.

◆ NoDuplicateVariable()

bool NoDuplicateVariable ( const LinearConstraint ct)

Definition at line 265 of file linear_constraint.cc.

◆ NonDeterministicLoop()

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

Definition at line 116 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 155 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 63 of file cp_model.cc.

◆ NotEqual()

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

Definition at line 496 of file precedences.h.

◆ operator<<() [1/8]

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

Definition at line 112 of file sat_base.h.

◆ operator<<() [2/8]

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

Definition at line 65 of file cp_model.cc.

◆ operator<<() [3/8]

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

Definition at line 330 of file cp_model.cc.

◆ operator<<() [4/8]

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

Definition at line 130 of file cp_model.cc.

◆ operator<<() [5/8]

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

Definition at line 193 of file integer.h.

◆ operator<<() [6/8]

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

Definition at line 107 of file sat_base.h.

◆ operator<<() [7/8]

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

Definition at line 60 of file pb_constraint.h.

◆ operator<<() [8/8]

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

Definition at line 1035 of file sat_solver.h.

◆ 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 159 of file cp_constraints.h.

◆ PositiveRef()

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

Definition at line 33 of file cp_model_utils.h.

◆ PositiveRemainder()

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

Definition at line 102 of file integer.h.

◆ PositiveVarExpr()

LinearExpression PositiveVarExpr ( const LinearExpression expr)

Definition at line 321 of file linear_constraint.cc.

◆ PositiveVariable()

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

Definition at line 134 of file integer.h.

◆ PostsolveClause()

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

Definition at line 27 of file cp_model_postsolve.cc.

◆ PostsolveElement()

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

Definition at line 183 of file cp_model_postsolve.cc.

◆ PostsolveExactlyOne()

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

Definition at line 50 of file cp_model_postsolve.cc.

◆ PostsolveIntMax()

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

Definition at line 157 of file cp_model_postsolve.cc.

◆ PostsolveLinear()

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

Definition at line 81 of file cp_model_postsolve.cc.

◆ PostsolveResponse()

void PostsolveResponse ( const int64  num_variables_in_original_model,
const CpModelProto &  mapping_proto,
const std::vector< int > &  postsolve_mapping,
CpSolverResponse *  response 
)

Definition at line 246 of file cp_model_postsolve.cc.

◆ PresolveCpModel()

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

Definition at line 5141 of file cp_model_presolve.cc.

◆ PrintClauses()

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

Definition at line 592 of file drat_checker.cc.

◆ ProbeAndFindEquivalentLiteral()

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

Definition at line 1129 of file simplification.cc.

◆ ProbeAndSimplifyProblem()

void ProbeAndSimplifyProblem ( SatPostsolver postsolver,
LinearBooleanProblem *  problem 
)

Definition at line 825 of file boolean_problem.cc.

◆ ProcessCore()

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

Definition at line 445 of file encoding.cc.

◆ ProductConstraint()

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

Definition at line 769 of file integer_expr.h.

◆ PseudoCost()

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

Definition at line 329 of file integer_search.cc.

◆ RandomizeDecisionHeuristic()

void RandomizeDecisionHeuristic ( URBG *  random,
SatParameters *  parameters 
)
inline

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

◆ RandomizeOnRestartHeuristic()

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

Definition at line 350 of file integer_search.cc.

◆ ReadDomainFromProto()

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

Definition at line 102 of file cp_model_utils.h.

◆ RecordLPRelaxationValues()

void RecordLPRelaxationValues ( Model model)

Definition at line 25 of file rins.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 366 of file encoding.cc.

◆ RefIsPositive()

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

Definition at line 34 of file cp_model_utils.h.

◆ RegisterAndTransferOwnership()

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

Definition at line 764 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 968 of file sat_solver.h.

◆ ReifiedBoolLe()

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

Definition at line 984 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 934 of file sat_solver.h.

◆ ReifiedEquality()

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

Definition at line 459 of file precedences.h.

◆ ReifiedEqualityWithOffset()

std::function<void(Model*)> operations_research::sat::ReifiedEqualityWithOffset ( IntegerVariable  a,
IntegerVariable  b,
int64  offset,
Literal  is_eq 
)
inline

Definition at line 477 of file precedences.h.

◆ ReifiedLowerOrEqualWithOffset()

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

Definition at line 445 of file precedences.h.

◆ ReindexArcs()

int operations_research::sat::ReindexArcs ( IntContainer *  tails,
IntContainer *  heads 
)

Definition at line 168 of file circuit.h.

◆ RemoveNearZeroTerms()

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

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

◆ RemoveZeroTerms()

void RemoveZeroTerms ( LinearConstraint constraint)

Definition at line 203 of file linear_constraint.cc.

◆ ResetAndSolveIntegerProblem()

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

Definition at line 891 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 464 of file drat_checker.cc.

◆ RestartEveryKFailures()

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

Definition at line 499 of file integer_search.cc.

◆ RestrictObjectiveDomainWithBinarySearch()

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

Definition at line 1091 of file optimization.cc.

◆ SatSolverHeuristic()

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

Definition at line 316 of file integer_search.cc.

◆ SatSolverRestartPolicy()

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

Definition at line 513 of file integer_search.cc.

◆ SatStatusString()

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

Definition at line 2530 of file sat_solver.cc.

◆ ScalarProduct()

double ScalarProduct ( const LinearConstraint constraint1,
const LinearConstraint constraint2 
)

Definition at line 150 of file linear_constraint.cc.

◆ ScaleContinuousVariables()

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

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

◆ ScaleObjectiveValue()

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

Definition at line 128 of file cp_model_utils.h.

◆ 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 demands,
int64  capacity,
LinearConstraintManager manager,
Model model 
)

Definition at line 2300 of file linear_programming_constraint.cc.

◆ SequentialLoop()

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

Definition at line 54 of file subsolver.cc.

◆ SequentialSearch()

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

Definition at line 188 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 199 of file integer_search.cc.

◆ SetSynchronizationFunction()

void operations_research::sat::SetSynchronizationFunction ( std::function< CpSolverResponse()>  f,
Model model 
)

If set, the underlying solver will call this function regularly in a deterministic way.

It will then wait until this function returns with the current best information about the current problem.

This is meant to be used in a multi-threaded environment with many parallel solving process. If the returned current "best" response only uses information derived at a lower deterministic time (possibly with offset) than the deterministic time of the current thread, the whole process can be made deterministic.

◆ SetToNegatedLinearExpression()

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

Definition at line 30 of file cp_model_utils.cc.

◆ SimplifyCanonicalBooleanLinearConstraint()

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

Definition at line 148 of file pb_constraint.cc.

◆ SimplifyClause()

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

Definition at line 931 of file simplification.cc.

◆ SizeVar()

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

Definition at line 600 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 887 of file cp_model.cc.

◆ SolutionIntegerMax()

int64 SolutionIntegerMax ( const CpSolverResponse &  r,
IntVar  x 
)

Returns the max of an integer variable in a solution.

Definition at line 879 of file cp_model.cc.

◆ SolutionIntegerMin()

int64 SolutionIntegerMin ( const CpSolverResponse &  r,
IntVar  x 
)

Returns the min of an integer variable in a solution.

Definition at line 871 of file cp_model.cc.

◆ SolutionIntegerValue()

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

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

Definition at line 863 of file cp_model.cc.

◆ SolutionIsFeasible()

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

Definition at line 1057 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 3259 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 2893 of file cp_model_solver.cc.

◆ SolveFzWithCpModelProto()

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

Definition at line 992 of file cp_model_fz_solver.cc.

◆ SolveIntegerProblem()

SatSolver::Status SolveIntegerProblem ( Model model)

Definition at line 652 of file integer_search.cc.

◆ SolveIntegerProblemWithLazyEncoding()

SatSolver::Status SolveIntegerProblemWithLazyEncoding ( Model model)

Definition at line 909 of file integer_search.cc.

◆ SolveLpAndUseIntegerVariableToStartLNS()

bool SolveLpAndUseIntegerVariableToStartLNS ( const glop::LinearProgram lp,
LinearBooleanProblem *  problem 
)

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

◆ SolveLpAndUseSolutionForSatAssignmentPreference()

bool SolveLpAndUseSolutionForSatAssignmentPreference ( const glop::LinearProgram lp,
SatSolver sat_solver,
double  max_time_in_seconds 
)

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

◆ SolveWithCardinalityEncoding()

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

Definition at line 888 of file optimization.cc.

◆ SolveWithCardinalityEncodingAndCore()

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

Definition at line 956 of file optimization.cc.

◆ SolveWithFuMalik()

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

Definition at line 268 of file optimization.cc.

◆ SolveWithLinearScan()

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

Definition at line 842 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 3264 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 3272 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 
)

Definition at line 1247 of file simplification.cc.

◆ SolveWithRandomParameters()

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

Definition at line 762 of file optimization.cc.

◆ SolveWithWPM1()

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

Definition at line 465 of file optimization.cc.

◆ SpanOfIntervals()

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

Definition at line 305 of file scheduling_constraints.cc.

◆ SplitAroundGivenValue()

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

Definition at line 70 of file integer_search.cc.

◆ SplitAroundLpValue()

IntegerLiteral SplitAroundLpValue ( IntegerVariable  var,
Model model 
)

Definition at line 98 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 > &  solution_repo,
Model model 
)

Definition at line 128 of file integer_search.cc.

◆ StartVar()

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

Definition at line 587 of file intervals.h.

◆ StoreAssignment()

void StoreAssignment ( const VariablesAssignment assignment,
BooleanAssignment *  output 
)

Definition at line 476 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 471 of file circuit.cc.

◆ SubstituteVariable()

void SubstituteVariable ( int  var,
int64  var_coeff_in_definition,
const ConstraintProto &  definition,
ConstraintProto *  ct 
)

Definition at line 182 of file presolve_util.cc.

◆ Sum2LowerOrEqual()

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

Definition at line 352 of file precedences.h.

◆ Sum3LowerOrEqual()

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

Definition at line 370 of file precedences.h.

◆ SUniv()

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

Definition at line 85 of file restart.h.

◆ ToDouble()

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

Definition at line 69 of file integer.h.

◆ ToIntegerValueVector()

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

Definition at line 101 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 75 of file symmetry_util.h.

◆ TransitionConstraint()

std::function< void(Model *)> TransitionConstraint ( const std::vector< IntegerVariable > &  vars,
const std::vector< std::vector< int64 >> &  automaton,
int64  initial_state,
const std::vector< int64 > &  final_states 
)

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

◆ TryToLinearizeConstraint()

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

Definition at line 323 of file linear_relaxation.cc.

◆ UnassignedVarWithLowestMinAtItsMinHeuristic()

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

Definition at line 168 of file integer_search.cc.

◆ UnscaleObjectiveValue()

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

Definition at line 138 of file cp_model_utils.h.

◆ UpperBound()

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

Definition at line 1473 of file integer.h.

◆ UsedIntervals()

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

Definition at line 474 of file cp_model_utils.cc.

◆ UsedVariables()

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

Definition at line 459 of file cp_model_utils.cc.

◆ UseObjectiveForSatAssignmentPreference()

void UseObjectiveForSatAssignmentPreference ( const LinearBooleanProblem &  problem,
SatSolver solver 
)

Definition at line 308 of file boolean_problem.cc.

◆ ValidateBooleanProblem()

absl::Status ValidateBooleanProblem ( const LinearBooleanProblem &  problem)

Definition at line 132 of file boolean_problem.cc.

◆ ValidateCpModel()

std::string ValidateCpModel ( const CpModelProto &  model)

Definition at line 453 of file cp_model_checker.cc.

◆ Value() [1/3]

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

Definition at line 1003 of file sat_solver.h.

◆ Value() [2/3]

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

Definition at line 1487 of file integer.h.

◆ Value() [3/3]

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

Definition at line 994 of file sat_solver.h.

◆ VariableIsPositive()

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

Definition at line 130 of file integer.h.

◆ WeightedSumGreaterOrEqual()

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

Definition at line 404 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  lower_bound 
)
inline

Definition at line 540 of file integer_expr.h.

◆ WeightedSumLowerOrEqual()

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

Definition at line 299 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  upper_bound 
)
inline

Definition at line 527 of file integer_expr.h.

◆ WeightedSumNotEqual()

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

Definition at line 619 of file integer_expr.h.

Variable Documentation

◆ kAffineRelationConstraint

constexpr int kAffineRelationConstraint = -2
constexpr

Definition at line 36 of file presolve_context.h.

◆ kAssumptionsConstraint

constexpr int kAssumptionsConstraint = -3
constexpr

Definition at line 37 of file presolve_context.h.

◆ kObjectiveConstraint

constexpr int kObjectiveConstraint = -1
constexpr

Definition at line 35 of file presolve_context.h.

◆ kUnsatTrailIndex

const int kUnsatTrailIndex = -1

Definition at line 52 of file sat_solver.h.