Namespaces
	AllDifferentConstraintProto

	AutomatonConstraintProto

	BoolArgumentProto

	BooleanAssignment

	CircuitConstraintProto

	ConstraintProto

	CpModelProto

	CpObjectiveProto

	CpSolverResponse

	CumulativeConstraintProto

	DecisionStrategyProto

	DecisionStrategyProto_AffineTransformation

	ElementConstraintProto

	IntegerArgumentProto

	IntegerVariableProto

	IntervalConstraintProto

	InverseConstraintProto

	LinearArgumentProto

	LinearBooleanConstraint

	LinearBooleanProblem

	LinearConstraintProto

	LinearExpressionProto

	LinearObjective

	NoOverlap2DConstraintProto

	NoOverlapConstraintProto

	PartialVariableAssignment

	ReservoirConstraintProto

	RoutesConstraintProto

	SatParameters

	TableConstraintProto

Classes
struct	AffineExpression

class	AllDifferentBoundsPropagator

class	AllDifferentConstraint

class	AllDifferentConstraintProtoDefaultTypeInternal

class	AllIntervalsHelper

struct	AssignmentInfo

struct	AssignmentType

class	AutomatonConstraint
	Specialized automaton constraint. More...

class	AutomatonConstraintProtoDefaultTypeInternal

struct	BinaryClause

class	BinaryClauseManager

class	BinaryImplicationGraph

class	BlockedClauseSimplifier

class	BoolArgumentProtoDefaultTypeInternal

class	BooleanAssignmentDefaultTypeInternal

struct	BooleanOrIntegerLiteral

struct	BooleanOrIntegerVariable

class	BooleanXorPropagator

class	BoolVar
	A Boolean variable. More...

class	BoundedVariableElimination

class	CanonicalBooleanLinearProblem

class	CircuitConstraint
	Specialized circuit constraint. More...

class	CircuitConstraintProtoDefaultTypeInternal

class	CircuitCoveringPropagator

class	CircuitPropagator

struct	ClauseInfo

class	CombinedDisjunctive

class	ConsecutiveConstraintsRelaxationNeighborhoodGenerator

class	Constraint
	A constraint. More...

class	ConstraintGraphNeighborhoodGenerator

class	ConstraintProtoDefaultTypeInternal

class	CoreBasedOptimizer

class	CoverCutHelper

class	CpModelBuilder
	Wrapper class around the cp_model proto. More...

class	CpModelMapping

class	CpModelPresolver

class	CpModelProtoDefaultTypeInternal

class	CpObjectiveProtoDefaultTypeInternal

class	CpSolverResponseDefaultTypeInternal

class	CumulativeConstraint
	Specialized cumulative constraint. More...

class	CumulativeConstraintProtoDefaultTypeInternal

class	CumulativeEnergyConstraint

struct	CutGenerator

struct	DebugSolution

class	DecisionStrategyProto_AffineTransformationDefaultTypeInternal

class	DecisionStrategyProtoDefaultTypeInternal

class	DisjunctiveDetectablePrecedences

class	DisjunctiveEdgeFinding

class	DisjunctiveNotLast

class	DisjunctiveOverloadChecker

class	DisjunctivePrecedences

class	DisjunctiveWithTwoItems

class	DivisionPropagator

class	DomainDeductions

class	DratChecker

class	DratProofHandler

class	DratWriter

class	DualBoundStrengthening

class	ElementConstraintProtoDefaultTypeInternal

class	EncodingNode

class	ExponentialMovingAverage

class	FeasibilityPump

class	FixedDivisionPropagator

class	FullEncodingFixedPointComputer

class	GenericLiteralWatcher

class	GreaterThanAtLeastOneOfPropagator

struct	ImpliedBoundEntry

class	ImpliedBounds

class	ImpliedBoundsProcessor

class	IncrementalAverage

struct	IndexReferences

class	Inprocessing

class	IntegerArgumentProtoDefaultTypeInternal

struct	IntegerDomains

class	IntegerEncoder

struct	IntegerLiteral

class	IntegerRoundingCutHelper

class	IntegerSumLE

class	IntegerTrail

class	IntegerVariableProtoDefaultTypeInternal

class	IntervalConstraintProtoDefaultTypeInternal

class	IntervalsRepository

class	IntervalVar
	Represents a Interval variable. More...

class	IntVar
	An integer variable. More...

class	InverseConstraintProtoDefaultTypeInternal

struct	KnapsackItem

struct	LevelZeroCallbackHelper

class	LevelZeroEquality

class	LinearArgumentProtoDefaultTypeInternal

class	LinearBooleanConstraintDefaultTypeInternal

class	LinearBooleanProblemDefaultTypeInternal

struct	LinearConstraint

class	LinearConstraintBuilder

class	LinearConstraintManager

class	LinearConstraintProtoDefaultTypeInternal

class	LinearExpr
	A dedicated container for linear expressions. More...

struct	LinearExpression

class	LinearExpressionProtoDefaultTypeInternal

class	LinearObjectiveDefaultTypeInternal

class	LinearProgrammingConstraint

class	LinearProgrammingConstraintCollection

struct	LinearProgrammingConstraintLpSolution

class	LinearProgrammingDispatcher

struct	LinearRelaxation

class	LinMinPropagator

class	Literal

class	LiteralWatchers

struct	LiteralWithCoeff

struct	LPSolveInfo

struct	LPVariable

struct	LPVariables

class	MinPropagator

class	Model
	Class that owns everything related to a particular optimization model. More...

struct	ModelRandomGenerator

class	MultipleCircuitConstraint
	Specialized circuit constraint. More...

class	MutableUpperBoundedLinearConstraint

struct	Neighborhood

class	NeighborhoodGenerator

class	NeighborhoodGeneratorHelper

class	NonOverlappingRectanglesDisjunctivePropagator

class	NonOverlappingRectanglesEnergyPropagator

class	NoOverlap2DConstraint
	Specialized no_overlap2D constraint. More...

class	NoOverlap2DConstraintProtoDefaultTypeInternal

class	NoOverlapConstraintProtoDefaultTypeInternal

struct	ObjectiveDefinition

class	PartialVariableAssignmentDefaultTypeInternal

class	PbConstraints

struct	PbConstraintsEnqueueHelper

class	Percentile

class	PositiveProductPropagator

struct	PostsolveClauses

class	PrecedencesPropagator

class	PresolveContext

struct	PresolveOptions

class	Prober

struct	ProbingOptions

class	PropagationGraph

class	PropagatorInterface

class	PROTOBUF_FINAL

class	PseudoCosts

class	RelaxationInducedNeighborhoodGenerator

class	ReservoirConstraint
	Specialized reservoir constraint. More...

class	ReservoirConstraintProtoDefaultTypeInternal

class	RestartPolicy

class	RevIntegerValueRepository

class	RevIntRepository

struct	RINSNeighborhood

struct	RoundingOptions

class	RoutesConstraintProtoDefaultTypeInternal

class	SatClause

class	SatDecisionPolicy

class	SatParametersDefaultTypeInternal

class	SatPostsolver

struct	SatPresolveOptions

class	SatPresolver

class	SatPropagator

class	SatSolver

class	SavedLiteral

class	SavedVariable

class	ScatteredIntegerVector

class	SccGraph

class	SchedulingConstraintHelper

class	SchedulingNeighborhoodGenerator

class	SchedulingTimeWindowNeighborhoodGenerator

struct	SearchHeuristics

class	SelectedMinPropagator

class	SharedBoundsManager

class	SharedIncompleteSolutionManager

class	SharedLPSolutionRepository

class	SharedRelaxationSolutionRepository

class	SharedResponseManager

class	SharedSolutionRepository

class	SimpleNeighborhoodGenerator

struct	SolutionObservers

class	SquarePropagator

class	StampingSimplifier

struct	Strategy

class	SubSolver

class	SymmetryPropagator

class	SynchronizationPoint

class	TableConstraint
	Specialized assignment constraint. More...

class	TableConstraintProtoDefaultTypeInternal

class	TaskSet

struct	TaskTime

class	ThetaLambdaTree

class	TimeTableEdgeFinding

class	TimeTablingPerTask

class	TopN

class	TopNCuts

class	Trail

class	UpperBoundedLinearConstraint

class	VarDomination

class	VariableGraphNeighborhoodGenerator

class	VariablesAssignment

class	VariableWithSameReasonIdentifier

struct	VarValue

class	WeightedRandomRelaxationNeighborhoodGenerator

class	ZeroHalfCutHelper

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

Enumerations
enum	DecisionStrategyProto_VariableSelectionStrategy : int { DecisionStrategyProto_VariableSelectionStrategy_CHOOSE_FIRST = 0, DecisionStrategyProto_VariableSelectionStrategy_CHOOSE_LOWEST_MIN = 1, DecisionStrategyProto_VariableSelectionStrategy_CHOOSE_HIGHEST_MAX = 2, DecisionStrategyProto_VariableSelectionStrategy_CHOOSE_MIN_DOMAIN_SIZE = 3, DecisionStrategyProto_VariableSelectionStrategy_CHOOSE_MAX_DOMAIN_SIZE = 4, DecisionStrategyProto_VariableSelectionStrategy_DecisionStrategyProto_VariableSelectionStrategy_INT_MIN_SENTINEL_DO_NOT_USE_ = std::numeric_limits<::PROTOBUF_NAMESPACE_ID::int32>::min(), DecisionStrategyProto_VariableSelectionStrategy_DecisionStrategyProto_VariableSelectionStrategy_INT_MAX_SENTINEL_DO_NOT_USE_ = std::numeric_limits<::PROTOBUF_NAMESPACE_ID::int32>::max() }

enum	DecisionStrategyProto_DomainReductionStrategy : int { DecisionStrategyProto_DomainReductionStrategy_SELECT_MIN_VALUE = 0, DecisionStrategyProto_DomainReductionStrategy_SELECT_MAX_VALUE = 1, DecisionStrategyProto_DomainReductionStrategy_SELECT_LOWER_HALF = 2, DecisionStrategyProto_DomainReductionStrategy_SELECT_UPPER_HALF = 3, DecisionStrategyProto_DomainReductionStrategy_SELECT_MEDIAN_VALUE = 4, DecisionStrategyProto_DomainReductionStrategy_DecisionStrategyProto_DomainReductionStrategy_INT_MIN_SENTINEL_DO_NOT_USE_ = std::numeric_limits<::PROTOBUF_NAMESPACE_ID::int32>::min(), DecisionStrategyProto_DomainReductionStrategy_DecisionStrategyProto_DomainReductionStrategy_INT_MAX_SENTINEL_DO_NOT_USE_ = std::numeric_limits<::PROTOBUF_NAMESPACE_ID::int32>::max() }

enum	CpSolverStatus : int { UNKNOWN = 0, MODEL_INVALID = 1, FEASIBLE = 2, INFEASIBLE = 3, OPTIMAL = 4, CpSolverStatus_INT_MIN_SENTINEL_DO_NOT_USE_ = std::numeric_limits<::PROTOBUF_NAMESPACE_ID::int32>::min(), CpSolverStatus_INT_MAX_SENTINEL_DO_NOT_USE_ = std::numeric_limits<::PROTOBUF_NAMESPACE_ID::int32>::max() }

enum	SatParameters_VariableOrder : int { SatParameters_VariableOrder_IN_ORDER = 0, SatParameters_VariableOrder_IN_REVERSE_ORDER = 1, SatParameters_VariableOrder_IN_RANDOM_ORDER = 2 }

enum	SatParameters_Polarity : int { SatParameters_Polarity_POLARITY_TRUE = 0, SatParameters_Polarity_POLARITY_FALSE = 1, SatParameters_Polarity_POLARITY_RANDOM = 2, SatParameters_Polarity_POLARITY_WEIGHTED_SIGN = 3, SatParameters_Polarity_POLARITY_REVERSE_WEIGHTED_SIGN = 4 }

enum	SatParameters_ConflictMinimizationAlgorithm : int { SatParameters_ConflictMinimizationAlgorithm_NONE = 0, SatParameters_ConflictMinimizationAlgorithm_SIMPLE = 1, SatParameters_ConflictMinimizationAlgorithm_RECURSIVE = 2, SatParameters_ConflictMinimizationAlgorithm_EXPERIMENTAL = 3 }

enum	SatParameters_BinaryMinizationAlgorithm : int { SatParameters_BinaryMinizationAlgorithm_NO_BINARY_MINIMIZATION = 0, SatParameters_BinaryMinizationAlgorithm_BINARY_MINIMIZATION_FIRST = 1, SatParameters_BinaryMinizationAlgorithm_BINARY_MINIMIZATION_FIRST_WITH_TRANSITIVE_REDUCTION = 4, SatParameters_BinaryMinizationAlgorithm_BINARY_MINIMIZATION_WITH_REACHABILITY = 2, SatParameters_BinaryMinizationAlgorithm_EXPERIMENTAL_BINARY_MINIMIZATION = 3 }

enum	SatParameters_ClauseProtection : int { SatParameters_ClauseProtection_PROTECTION_NONE = 0, SatParameters_ClauseProtection_PROTECTION_ALWAYS = 1, SatParameters_ClauseProtection_PROTECTION_LBD = 2 }

enum	SatParameters_ClauseOrdering : int { SatParameters_ClauseOrdering_CLAUSE_ACTIVITY = 0, SatParameters_ClauseOrdering_CLAUSE_LBD = 1 }

enum	SatParameters_RestartAlgorithm : int { SatParameters_RestartAlgorithm_NO_RESTART = 0, SatParameters_RestartAlgorithm_LUBY_RESTART = 1, SatParameters_RestartAlgorithm_DL_MOVING_AVERAGE_RESTART = 2, SatParameters_RestartAlgorithm_LBD_MOVING_AVERAGE_RESTART = 3, SatParameters_RestartAlgorithm_FIXED_RESTART = 4 }

enum	SatParameters_MaxSatAssumptionOrder : int { SatParameters_MaxSatAssumptionOrder_DEFAULT_ASSUMPTION_ORDER = 0, SatParameters_MaxSatAssumptionOrder_ORDER_ASSUMPTION_BY_DEPTH = 1, SatParameters_MaxSatAssumptionOrder_ORDER_ASSUMPTION_BY_WEIGHT = 2 }

enum	SatParameters_MaxSatStratificationAlgorithm : int { SatParameters_MaxSatStratificationAlgorithm_STRATIFICATION_NONE = 0, SatParameters_MaxSatStratificationAlgorithm_STRATIFICATION_DESCENT = 1, SatParameters_MaxSatStratificationAlgorithm_STRATIFICATION_ASCENT = 2 }

enum	SatParameters_SearchBranching : int { SatParameters_SearchBranching_AUTOMATIC_SEARCH = 0, SatParameters_SearchBranching_FIXED_SEARCH = 1, SatParameters_SearchBranching_PORTFOLIO_SEARCH = 2, SatParameters_SearchBranching_LP_SEARCH = 3, SatParameters_SearchBranching_PSEUDO_COST_SEARCH = 4, SatParameters_SearchBranching_PORTFOLIO_WITH_QUICK_RESTART_SEARCH = 5, SatParameters_SearchBranching_HINT_SEARCH = 6 }

enum	SatParameters_FPRoundingMethod : int { SatParameters_FPRoundingMethod_NEAREST_INTEGER = 0, SatParameters_FPRoundingMethod_LOCK_BASED = 1, SatParameters_FPRoundingMethod_ACTIVE_LOCK_BASED = 3, SatParameters_FPRoundingMethod_PROPAGATION_ASSISTED = 2 }

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)

const ::PROTOBUF_NAMESPACE_ID::EnumDescriptor *	DecisionStrategyProto_VariableSelectionStrategy_descriptor ()

bool	DecisionStrategyProto_VariableSelectionStrategy_IsValid (int value)

const ::PROTOBUF_NAMESPACE_ID::EnumDescriptor *	DecisionStrategyProto_DomainReductionStrategy_descriptor ()

bool	DecisionStrategyProto_DomainReductionStrategy_IsValid (int value)

const ::PROTOBUF_NAMESPACE_ID::EnumDescriptor *	CpSolverStatus_descriptor ()

bool	CpSolverStatus_IsValid (int value)

template<typename T >
const std::string &	DecisionStrategyProto_VariableSelectionStrategy_Name (T enum_t_value)

bool	DecisionStrategyProto_VariableSelectionStrategy_Parse (::PROTOBUF_NAMESPACE_ID::ConstStringParam name, DecisionStrategyProto_VariableSelectionStrategy *value)

template<typename T >
const std::string &	DecisionStrategyProto_DomainReductionStrategy_Name (T enum_t_value)

bool	DecisionStrategyProto_DomainReductionStrategy_Parse (::PROTOBUF_NAMESPACE_ID::ConstStringParam name, DecisionStrategyProto_DomainReductionStrategy *value)

template<typename T >
const std::string &	CpSolverStatus_Name (T enum_t_value)

bool	CpSolverStatus_Parse (::PROTOBUF_NAMESPACE_ID::ConstStringParam name, CpSolverStatus *value)

const ::PROTOBUF_NAMESPACE_ID::EnumDescriptor *	SatParameters_VariableOrder_descriptor ()

bool	SatParameters_VariableOrder_IsValid (int value)

const ::PROTOBUF_NAMESPACE_ID::EnumDescriptor *	SatParameters_Polarity_descriptor ()

bool	SatParameters_Polarity_IsValid (int value)

const ::PROTOBUF_NAMESPACE_ID::EnumDescriptor *	SatParameters_ConflictMinimizationAlgorithm_descriptor ()

bool	SatParameters_ConflictMinimizationAlgorithm_IsValid (int value)

const ::PROTOBUF_NAMESPACE_ID::EnumDescriptor *	SatParameters_BinaryMinizationAlgorithm_descriptor ()

bool	SatParameters_BinaryMinizationAlgorithm_IsValid (int value)

const ::PROTOBUF_NAMESPACE_ID::EnumDescriptor *	SatParameters_ClauseProtection_descriptor ()

bool	SatParameters_ClauseProtection_IsValid (int value)

const ::PROTOBUF_NAMESPACE_ID::EnumDescriptor *	SatParameters_ClauseOrdering_descriptor ()

bool	SatParameters_ClauseOrdering_IsValid (int value)

const ::PROTOBUF_NAMESPACE_ID::EnumDescriptor *	SatParameters_RestartAlgorithm_descriptor ()

bool	SatParameters_RestartAlgorithm_IsValid (int value)

const ::PROTOBUF_NAMESPACE_ID::EnumDescriptor *	SatParameters_MaxSatAssumptionOrder_descriptor ()

bool	SatParameters_MaxSatAssumptionOrder_IsValid (int value)

const ::PROTOBUF_NAMESPACE_ID::EnumDescriptor *	SatParameters_MaxSatStratificationAlgorithm_descriptor ()

bool	SatParameters_MaxSatStratificationAlgorithm_IsValid (int value)

const ::PROTOBUF_NAMESPACE_ID::EnumDescriptor *	SatParameters_SearchBranching_descriptor ()

bool	SatParameters_SearchBranching_IsValid (int value)

const ::PROTOBUF_NAMESPACE_ID::EnumDescriptor *	SatParameters_FPRoundingMethod_descriptor ()

bool	SatParameters_FPRoundingMethod_IsValid (int value)

template<typename T >
const std::string &	SatParameters_VariableOrder_Name (T enum_t_value)

bool	SatParameters_VariableOrder_Parse (::PROTOBUF_NAMESPACE_ID::ConstStringParam name, SatParameters_VariableOrder *value)

template<typename T >
const std::string &	SatParameters_Polarity_Name (T enum_t_value)

bool	SatParameters_Polarity_Parse (::PROTOBUF_NAMESPACE_ID::ConstStringParam name, SatParameters_Polarity *value)

template<typename T >
const std::string &	SatParameters_ConflictMinimizationAlgorithm_Name (T enum_t_value)

bool	SatParameters_ConflictMinimizationAlgorithm_Parse (::PROTOBUF_NAMESPACE_ID::ConstStringParam name, SatParameters_ConflictMinimizationAlgorithm *value)

template<typename T >
const std::string &	SatParameters_BinaryMinizationAlgorithm_Name (T enum_t_value)

bool	SatParameters_BinaryMinizationAlgorithm_Parse (::PROTOBUF_NAMESPACE_ID::ConstStringParam name, SatParameters_BinaryMinizationAlgorithm *value)

template<typename T >
const std::string &	SatParameters_ClauseProtection_Name (T enum_t_value)

bool	SatParameters_ClauseProtection_Parse (::PROTOBUF_NAMESPACE_ID::ConstStringParam name, SatParameters_ClauseProtection *value)

template<typename T >
const std::string &	SatParameters_ClauseOrdering_Name (T enum_t_value)

bool	SatParameters_ClauseOrdering_Parse (::PROTOBUF_NAMESPACE_ID::ConstStringParam name, SatParameters_ClauseOrdering *value)

template<typename T >
const std::string &	SatParameters_RestartAlgorithm_Name (T enum_t_value)

bool	SatParameters_RestartAlgorithm_Parse (::PROTOBUF_NAMESPACE_ID::ConstStringParam name, SatParameters_RestartAlgorithm *value)

template<typename T >
const std::string &	SatParameters_MaxSatAssumptionOrder_Name (T enum_t_value)

bool	SatParameters_MaxSatAssumptionOrder_Parse (::PROTOBUF_NAMESPACE_ID::ConstStringParam name, SatParameters_MaxSatAssumptionOrder *value)

template<typename T >
const std::string &	SatParameters_MaxSatStratificationAlgorithm_Name (T enum_t_value)

bool	SatParameters_MaxSatStratificationAlgorithm_Parse (::PROTOBUF_NAMESPACE_ID::ConstStringParam name, SatParameters_MaxSatStratificationAlgorithm *value)

template<typename T >
const std::string &	SatParameters_SearchBranching_Name (T enum_t_value)

bool	SatParameters_SearchBranching_Parse (::PROTOBUF_NAMESPACE_ID::ConstStringParam name, SatParameters_SearchBranching *value)

template<typename T >
const std::string &	SatParameters_FPRoundingMethod_Name (T enum_t_value)

bool	SatParameters_FPRoundingMethod_Parse (::PROTOBUF_NAMESPACE_ID::ConstStringParam name, SatParameters_FPRoundingMethod *value)

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 (PresolveOptions options, 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	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)

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	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 (const PresolveOptions &options, 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 CpModelProto &problem, std::vector< std::unique_ptr< SparsePermutation >> *generators, double time_limit_seconds)

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< int64 >	AllValuesInDomain (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)

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)

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

EncodingNode *	LazyMergeAllNodeWithPQ (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< Literal >	ReduceNodesAndExtractAssumptions (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 master, 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_lower_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 (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::VariableBoundChange >	GetBoundChanges (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, random_engine_t *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)

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 ()

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
class operations_research::sat::LinearBooleanConstraintDefaultTypeInternal	_LinearBooleanConstraint_default_instance_

class operations_research::sat::LinearObjectiveDefaultTypeInternal	_LinearObjective_default_instance_

class operations_research::sat::BooleanAssignmentDefaultTypeInternal	_BooleanAssignment_default_instance_

class operations_research::sat::LinearBooleanProblemDefaultTypeInternal	_LinearBooleanProblem_default_instance_

class operations_research::sat::IntegerVariableProtoDefaultTypeInternal	_IntegerVariableProto_default_instance_

class operations_research::sat::BoolArgumentProtoDefaultTypeInternal	_BoolArgumentProto_default_instance_

class operations_research::sat::IntegerArgumentProtoDefaultTypeInternal	_IntegerArgumentProto_default_instance_

class operations_research::sat::LinearExpressionProtoDefaultTypeInternal	_LinearExpressionProto_default_instance_

class operations_research::sat::LinearArgumentProtoDefaultTypeInternal	_LinearArgumentProto_default_instance_

class operations_research::sat::AllDifferentConstraintProtoDefaultTypeInternal	_AllDifferentConstraintProto_default_instance_

class operations_research::sat::LinearConstraintProtoDefaultTypeInternal	_LinearConstraintProto_default_instance_

class operations_research::sat::ElementConstraintProtoDefaultTypeInternal	_ElementConstraintProto_default_instance_

class operations_research::sat::IntervalConstraintProtoDefaultTypeInternal	_IntervalConstraintProto_default_instance_

class operations_research::sat::NoOverlapConstraintProtoDefaultTypeInternal	_NoOverlapConstraintProto_default_instance_

class operations_research::sat::NoOverlap2DConstraintProtoDefaultTypeInternal	_NoOverlap2DConstraintProto_default_instance_

class operations_research::sat::CumulativeConstraintProtoDefaultTypeInternal	_CumulativeConstraintProto_default_instance_

class operations_research::sat::ReservoirConstraintProtoDefaultTypeInternal	_ReservoirConstraintProto_default_instance_

class operations_research::sat::CircuitConstraintProtoDefaultTypeInternal	_CircuitConstraintProto_default_instance_

class operations_research::sat::RoutesConstraintProtoDefaultTypeInternal	_RoutesConstraintProto_default_instance_

class operations_research::sat::TableConstraintProtoDefaultTypeInternal	_TableConstraintProto_default_instance_

class operations_research::sat::InverseConstraintProtoDefaultTypeInternal	_InverseConstraintProto_default_instance_

class operations_research::sat::AutomatonConstraintProtoDefaultTypeInternal	_AutomatonConstraintProto_default_instance_

class operations_research::sat::ConstraintProtoDefaultTypeInternal	_ConstraintProto_default_instance_

class operations_research::sat::CpObjectiveProtoDefaultTypeInternal	_CpObjectiveProto_default_instance_

class operations_research::sat::DecisionStrategyProto_AffineTransformationDefaultTypeInternal	_DecisionStrategyProto_AffineTransformation_default_instance_

class operations_research::sat::DecisionStrategyProtoDefaultTypeInternal	_DecisionStrategyProto_default_instance_

class operations_research::sat::PartialVariableAssignmentDefaultTypeInternal	_PartialVariableAssignment_default_instance_

class operations_research::sat::CpModelProtoDefaultTypeInternal	_CpModelProto_default_instance_

class operations_research::sat::CpSolverResponseDefaultTypeInternal	_CpSolverResponse_default_instance_

constexpr DecisionStrategyProto_VariableSelectionStrategy	DecisionStrategyProto_VariableSelectionStrategy_VariableSelectionStrategy_MIN = DecisionStrategyProto_VariableSelectionStrategy_CHOOSE_FIRST

constexpr DecisionStrategyProto_VariableSelectionStrategy	DecisionStrategyProto_VariableSelectionStrategy_VariableSelectionStrategy_MAX = DecisionStrategyProto_VariableSelectionStrategy_CHOOSE_MAX_DOMAIN_SIZE

constexpr int	DecisionStrategyProto_VariableSelectionStrategy_VariableSelectionStrategy_ARRAYSIZE = DecisionStrategyProto_VariableSelectionStrategy_VariableSelectionStrategy_MAX + 1

constexpr DecisionStrategyProto_DomainReductionStrategy	DecisionStrategyProto_DomainReductionStrategy_DomainReductionStrategy_MIN = DecisionStrategyProto_DomainReductionStrategy_SELECT_MIN_VALUE

constexpr DecisionStrategyProto_DomainReductionStrategy	DecisionStrategyProto_DomainReductionStrategy_DomainReductionStrategy_MAX = DecisionStrategyProto_DomainReductionStrategy_SELECT_MEDIAN_VALUE

constexpr int	DecisionStrategyProto_DomainReductionStrategy_DomainReductionStrategy_ARRAYSIZE = DecisionStrategyProto_DomainReductionStrategy_DomainReductionStrategy_MAX + 1

constexpr CpSolverStatus	CpSolverStatus_MIN = UNKNOWN

constexpr CpSolverStatus	CpSolverStatus_MAX = OPTIMAL

constexpr int	CpSolverStatus_ARRAYSIZE = CpSolverStatus_MAX + 1

class operations_research::sat::SatParametersDefaultTypeInternal	_SatParameters_default_instance_

constexpr SatParameters_VariableOrder	SatParameters_VariableOrder_VariableOrder_MIN = SatParameters_VariableOrder_IN_ORDER

constexpr SatParameters_VariableOrder	SatParameters_VariableOrder_VariableOrder_MAX = SatParameters_VariableOrder_IN_RANDOM_ORDER

constexpr int	SatParameters_VariableOrder_VariableOrder_ARRAYSIZE = SatParameters_VariableOrder_VariableOrder_MAX + 1

constexpr SatParameters_Polarity	SatParameters_Polarity_Polarity_MIN = SatParameters_Polarity_POLARITY_TRUE

constexpr SatParameters_Polarity	SatParameters_Polarity_Polarity_MAX = SatParameters_Polarity_POLARITY_REVERSE_WEIGHTED_SIGN

constexpr int	SatParameters_Polarity_Polarity_ARRAYSIZE = SatParameters_Polarity_Polarity_MAX + 1

constexpr SatParameters_ConflictMinimizationAlgorithm	SatParameters_ConflictMinimizationAlgorithm_ConflictMinimizationAlgorithm_MIN = SatParameters_ConflictMinimizationAlgorithm_NONE

constexpr SatParameters_ConflictMinimizationAlgorithm	SatParameters_ConflictMinimizationAlgorithm_ConflictMinimizationAlgorithm_MAX = SatParameters_ConflictMinimizationAlgorithm_EXPERIMENTAL

constexpr int	SatParameters_ConflictMinimizationAlgorithm_ConflictMinimizationAlgorithm_ARRAYSIZE = SatParameters_ConflictMinimizationAlgorithm_ConflictMinimizationAlgorithm_MAX + 1

constexpr SatParameters_BinaryMinizationAlgorithm	SatParameters_BinaryMinizationAlgorithm_BinaryMinizationAlgorithm_MIN = SatParameters_BinaryMinizationAlgorithm_NO_BINARY_MINIMIZATION

constexpr SatParameters_BinaryMinizationAlgorithm	SatParameters_BinaryMinizationAlgorithm_BinaryMinizationAlgorithm_MAX = SatParameters_BinaryMinizationAlgorithm_BINARY_MINIMIZATION_FIRST_WITH_TRANSITIVE_REDUCTION

constexpr int	SatParameters_BinaryMinizationAlgorithm_BinaryMinizationAlgorithm_ARRAYSIZE = SatParameters_BinaryMinizationAlgorithm_BinaryMinizationAlgorithm_MAX + 1

constexpr SatParameters_ClauseProtection	SatParameters_ClauseProtection_ClauseProtection_MIN = SatParameters_ClauseProtection_PROTECTION_NONE

constexpr SatParameters_ClauseProtection	SatParameters_ClauseProtection_ClauseProtection_MAX = SatParameters_ClauseProtection_PROTECTION_LBD

constexpr int	SatParameters_ClauseProtection_ClauseProtection_ARRAYSIZE = SatParameters_ClauseProtection_ClauseProtection_MAX + 1

constexpr SatParameters_ClauseOrdering	SatParameters_ClauseOrdering_ClauseOrdering_MIN = SatParameters_ClauseOrdering_CLAUSE_ACTIVITY

constexpr SatParameters_ClauseOrdering	SatParameters_ClauseOrdering_ClauseOrdering_MAX = SatParameters_ClauseOrdering_CLAUSE_LBD

constexpr int	SatParameters_ClauseOrdering_ClauseOrdering_ARRAYSIZE = SatParameters_ClauseOrdering_ClauseOrdering_MAX + 1

constexpr SatParameters_RestartAlgorithm	SatParameters_RestartAlgorithm_RestartAlgorithm_MIN = SatParameters_RestartAlgorithm_NO_RESTART

constexpr SatParameters_RestartAlgorithm	SatParameters_RestartAlgorithm_RestartAlgorithm_MAX = SatParameters_RestartAlgorithm_FIXED_RESTART

constexpr int	SatParameters_RestartAlgorithm_RestartAlgorithm_ARRAYSIZE = SatParameters_RestartAlgorithm_RestartAlgorithm_MAX + 1

constexpr SatParameters_MaxSatAssumptionOrder	SatParameters_MaxSatAssumptionOrder_MaxSatAssumptionOrder_MIN = SatParameters_MaxSatAssumptionOrder_DEFAULT_ASSUMPTION_ORDER

constexpr SatParameters_MaxSatAssumptionOrder	SatParameters_MaxSatAssumptionOrder_MaxSatAssumptionOrder_MAX = SatParameters_MaxSatAssumptionOrder_ORDER_ASSUMPTION_BY_WEIGHT

constexpr int	SatParameters_MaxSatAssumptionOrder_MaxSatAssumptionOrder_ARRAYSIZE = SatParameters_MaxSatAssumptionOrder_MaxSatAssumptionOrder_MAX + 1

constexpr SatParameters_MaxSatStratificationAlgorithm	SatParameters_MaxSatStratificationAlgorithm_MaxSatStratificationAlgorithm_MIN = SatParameters_MaxSatStratificationAlgorithm_STRATIFICATION_NONE

constexpr SatParameters_MaxSatStratificationAlgorithm	SatParameters_MaxSatStratificationAlgorithm_MaxSatStratificationAlgorithm_MAX = SatParameters_MaxSatStratificationAlgorithm_STRATIFICATION_ASCENT

constexpr int	SatParameters_MaxSatStratificationAlgorithm_MaxSatStratificationAlgorithm_ARRAYSIZE = SatParameters_MaxSatStratificationAlgorithm_MaxSatStratificationAlgorithm_MAX + 1

constexpr SatParameters_SearchBranching	SatParameters_SearchBranching_SearchBranching_MIN = SatParameters_SearchBranching_AUTOMATIC_SEARCH

constexpr SatParameters_SearchBranching	SatParameters_SearchBranching_SearchBranching_MAX = SatParameters_SearchBranching_HINT_SEARCH

constexpr int	SatParameters_SearchBranching_SearchBranching_ARRAYSIZE = SatParameters_SearchBranching_SearchBranching_MAX + 1

constexpr SatParameters_FPRoundingMethod	SatParameters_FPRoundingMethod_FPRoundingMethod_MIN = SatParameters_FPRoundingMethod_NEAREST_INTEGER

constexpr SatParameters_FPRoundingMethod	SatParameters_FPRoundingMethod_FPRoundingMethod_MAX = SatParameters_FPRoundingMethod_ACTIVE_LOCK_BASED

constexpr int	SatParameters_FPRoundingMethod_FPRoundingMethod_ARRAYSIZE = SatParameters_FPRoundingMethod_FPRoundingMethod_MAX + 1

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

◆ CpSolverStatus

enum CpSolverStatus : int

Enumerator
UNKNOWN
MODEL_INVALID
FEASIBLE
INFEASIBLE
OPTIMAL
CpSolverStatus_INT_MIN_SENTINEL_DO_NOT_USE_
CpSolverStatus_INT_MAX_SENTINEL_DO_NOT_USE_

Definition at line 222 of file cp_model.pb.h.

◆ DecisionStrategyProto_DomainReductionStrategy

enum DecisionStrategyProto_DomainReductionStrategy : int

Enumerator
DecisionStrategyProto_DomainReductionStrategy_SELECT_MIN_VALUE
DecisionStrategyProto_DomainReductionStrategy_SELECT_MAX_VALUE
DecisionStrategyProto_DomainReductionStrategy_SELECT_LOWER_HALF
DecisionStrategyProto_DomainReductionStrategy_SELECT_UPPER_HALF
DecisionStrategyProto_DomainReductionStrategy_SELECT_MEDIAN_VALUE
DecisionStrategyProto_DomainReductionStrategy_DecisionStrategyProto_DomainReductionStrategy_INT_MIN_SENTINEL_DO_NOT_USE_
DecisionStrategyProto_DomainReductionStrategy_DecisionStrategyProto_DomainReductionStrategy_INT_MAX_SENTINEL_DO_NOT_USE_

Definition at line 194 of file cp_model.pb.h.

◆ DecisionStrategyProto_VariableSelectionStrategy

enum DecisionStrategyProto_VariableSelectionStrategy : int

Enumerator
DecisionStrategyProto_VariableSelectionStrategy_CHOOSE_FIRST
DecisionStrategyProto_VariableSelectionStrategy_CHOOSE_LOWEST_MIN
DecisionStrategyProto_VariableSelectionStrategy_CHOOSE_HIGHEST_MAX
DecisionStrategyProto_VariableSelectionStrategy_CHOOSE_MIN_DOMAIN_SIZE
DecisionStrategyProto_VariableSelectionStrategy_CHOOSE_MAX_DOMAIN_SIZE
DecisionStrategyProto_VariableSelectionStrategy_DecisionStrategyProto_VariableSelectionStrategy_INT_MIN_SENTINEL_DO_NOT_USE_
DecisionStrategyProto_VariableSelectionStrategy_DecisionStrategyProto_VariableSelectionStrategy_INT_MAX_SENTINEL_DO_NOT_USE_

Definition at line 166 of file cp_model.pb.h.

◆ LogBehavior

enum LogBehavior

Enumerator
DEFAULT_LOG
STDOUT_LOG

Definition at line 44 of file optimization.h.

◆ SatFormat

enum SatFormat

Enumerator
DIMACS
DRAT

Definition at line 326 of file drat_checker.h.

◆ SatParameters_BinaryMinizationAlgorithm

enum SatParameters_BinaryMinizationAlgorithm : int

Enumerator
SatParameters_BinaryMinizationAlgorithm_NO_BINARY_MINIMIZATION
SatParameters_BinaryMinizationAlgorithm_BINARY_MINIMIZATION_FIRST
SatParameters_BinaryMinizationAlgorithm_BINARY_MINIMIZATION_FIRST_WITH_TRANSITIVE_REDUCTION
SatParameters_BinaryMinizationAlgorithm_BINARY_MINIMIZATION_WITH_REACHABILITY
SatParameters_BinaryMinizationAlgorithm_EXPERIMENTAL_BINARY_MINIMIZATION

Definition at line 145 of file sat_parameters.pb.h.

◆ SatParameters_ClauseOrdering

enum SatParameters_ClauseOrdering : int

Enumerator
SatParameters_ClauseOrdering_CLAUSE_ACTIVITY
SatParameters_ClauseOrdering_CLAUSE_LBD

Definition at line 195 of file sat_parameters.pb.h.

◆ SatParameters_ClauseProtection

enum SatParameters_ClauseProtection : int

Enumerator
SatParameters_ClauseProtection_PROTECTION_NONE
SatParameters_ClauseProtection_PROTECTION_ALWAYS
SatParameters_ClauseProtection_PROTECTION_LBD

Definition at line 171 of file sat_parameters.pb.h.

◆ SatParameters_ConflictMinimizationAlgorithm

enum SatParameters_ConflictMinimizationAlgorithm : int

Enumerator
SatParameters_ConflictMinimizationAlgorithm_NONE
SatParameters_ConflictMinimizationAlgorithm_SIMPLE
SatParameters_ConflictMinimizationAlgorithm_RECURSIVE
SatParameters_ConflictMinimizationAlgorithm_EXPERIMENTAL

Definition at line 120 of file sat_parameters.pb.h.

◆ SatParameters_FPRoundingMethod

enum SatParameters_FPRoundingMethod : int

Enumerator
SatParameters_FPRoundingMethod_NEAREST_INTEGER
SatParameters_FPRoundingMethod_LOCK_BASED
SatParameters_FPRoundingMethod_ACTIVE_LOCK_BASED
SatParameters_FPRoundingMethod_PROPAGATION_ASSISTED

Definition at line 320 of file sat_parameters.pb.h.

◆ SatParameters_MaxSatAssumptionOrder

enum SatParameters_MaxSatAssumptionOrder : int

Enumerator
SatParameters_MaxSatAssumptionOrder_DEFAULT_ASSUMPTION_ORDER
SatParameters_MaxSatAssumptionOrder_ORDER_ASSUMPTION_BY_DEPTH
SatParameters_MaxSatAssumptionOrder_ORDER_ASSUMPTION_BY_WEIGHT

Definition at line 244 of file sat_parameters.pb.h.

◆ SatParameters_MaxSatStratificationAlgorithm

enum SatParameters_MaxSatStratificationAlgorithm : int

Enumerator
SatParameters_MaxSatStratificationAlgorithm_STRATIFICATION_NONE
SatParameters_MaxSatStratificationAlgorithm_STRATIFICATION_DESCENT
SatParameters_MaxSatStratificationAlgorithm_STRATIFICATION_ASCENT

Definition at line 268 of file sat_parameters.pb.h.

◆ SatParameters_Polarity

enum SatParameters_Polarity : int

Enumerator
SatParameters_Polarity_POLARITY_TRUE
SatParameters_Polarity_POLARITY_FALSE
SatParameters_Polarity_POLARITY_RANDOM
SatParameters_Polarity_POLARITY_WEIGHTED_SIGN
SatParameters_Polarity_POLARITY_REVERSE_WEIGHTED_SIGN

Definition at line 94 of file sat_parameters.pb.h.

◆ SatParameters_RestartAlgorithm

enum SatParameters_RestartAlgorithm : int

Enumerator
SatParameters_RestartAlgorithm_NO_RESTART
SatParameters_RestartAlgorithm_LUBY_RESTART
SatParameters_RestartAlgorithm_DL_MOVING_AVERAGE_RESTART
SatParameters_RestartAlgorithm_LBD_MOVING_AVERAGE_RESTART
SatParameters_RestartAlgorithm_FIXED_RESTART

Definition at line 218 of file sat_parameters.pb.h.

◆ SatParameters_SearchBranching

enum SatParameters_SearchBranching : int

Enumerator
SatParameters_SearchBranching_AUTOMATIC_SEARCH
SatParameters_SearchBranching_FIXED_SEARCH
SatParameters_SearchBranching_PORTFOLIO_SEARCH
SatParameters_SearchBranching_LP_SEARCH
SatParameters_SearchBranching_PSEUDO_COST_SEARCH
SatParameters_SearchBranching_PORTFOLIO_WITH_QUICK_RESTART_SEARCH
SatParameters_SearchBranching_HINT_SEARCH

Definition at line 292 of file sat_parameters.pb.h.

◆ SatParameters_VariableOrder

enum SatParameters_VariableOrder : int

Enumerator
SatParameters_VariableOrder_IN_ORDER
SatParameters_VariableOrder_IN_REVERSE_ORDER
SatParameters_VariableOrder_IN_RANDOM_ORDER

Definition at line 70 of file sat_parameters.pb.h.

Function Documentation

◆ AddCumulativeCut()

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

Definition at line 488 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 1983 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 336 of file boolean_problem.cc.

◆ AddObjectiveUpperBound()

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

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

◆ 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 580 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 785 of file linear_relaxation.cc.

◆ AppendLinMaxRelaxation()

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

Definition at line 688 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 614 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 599 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 102 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 310 of file cp_model_utils.cc.

◆ ApplyToAllLiteralIndices()

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

Definition at line 157 of file cp_model_utils.cc.

◆ ApplyToAllVariableIndices()

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

Definition at line 221 of file cp_model_utils.cc.

◆ ApplyVariableMapping()

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

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

◆ BooleanLinearConstraint()

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

inline

Definition at line 853 of file sat_solver.h.

◆ BooleanLinearExpressionIsCanonical()

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

Definition at line 135 of file pb_constraint.cc.

◆ BooleanProblemToCpModelproto()

CpModelProto BooleanProblemToCpModelproto ( const LinearBooleanProblem & problem )

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

◆ CanBeFilteredUsingKnapsackUpperBound()

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

Definition at line 335 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 369 of file cuts.cc.

◆ CanonicalizeConstraint()

void CanonicalizeConstraint ( LinearConstraint * ct )

Definition at line 243 of file linear_constraint.cc.

◆ CanonicalizeExpr()

LinearExpression CanonicalizeExpr ( const LinearExpression & expr )

Definition at line 277 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 862 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 208 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 905 of file sat_solver.h.

◆ CleanTermsAndFillConstraint()

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

Definition at line 82 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 121 of file linear_constraint.cc.

◆ ComputeBooleanLinearExpressionCanonicalForm()

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

Definition at line 40 of file pb_constraint.cc.

◆ ComputeCanonicalRhs()

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

Definition at line 159 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 141 of file linear_constraint.cc.

◆ ComputeInnerObjective()

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

Definition at line 506 of file cp_model_utils.cc.

◆ ComputeL2Norm()

double ComputeL2Norm ( const LinearConstraint & constraint )

Definition at line 133 of file linear_constraint.cc.

◆ ComputeNegatedCanonicalRhs()

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

Definition at line 177 of file pb_constraint.cc.

◆ ComputeObjectiveValue()

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

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

◆ ComputeResolvantSize()

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

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

◆ ConstraintCaseName()

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

Definition at line 373 of file cp_model_utils.cc.

◆ ConstraintIsTriviallyTrue()

bool ConstraintIsTriviallyTrue	(	const LinearConstraint &	constraint,
		const IntegerTrail &	integer_trail
	)

Definition at line 273 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 915 of file sat/lp_utils.cc.

◆ ConvertBooleanProblemToLinearProgram()

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

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

◆ ConvertMPModelProtoToCpModelProto()

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

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

◆ ConvertToKnapsackForm()

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

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

◆ CpSolverStatus_descriptor()

const ::PROTOBUF_NAMESPACE_ID::EnumDescriptor * CpSolverStatus_descriptor ( )

Definition at line 1031 of file cp_model.pb.cc.

◆ CpSolverStatus_IsValid()

bool CpSolverStatus_IsValid ( int value )

Definition at line 1035 of file cp_model.pb.cc.

◆ CpSolverStatus_Name()

const std::string& operations_research::sat::CpSolverStatus_Name ( T enum_t_value )

inline

Definition at line 238 of file cp_model.pb.h.

◆ CpSolverStatus_Parse()

bool operations_research::sat::CpSolverStatus_Parse	(	::PROTOBUF_NAMESPACE_ID::ConstStringParam	name,
		CpSolverStatus *	value
	)

inline

Definition at line 245 of file cp_model.pb.h.

◆ CreateAllDifferentCutGenerator()

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

Definition at line 1817 of file cuts.cc.

◆ CreateCliqueCutGenerator()

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

Definition at line 2410 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 2197 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 2528 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 436 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 1914 of file cuts.cc.

◆ CreateNoOverlapCutGenerator()

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

Definition at line 2330 of file cuts.cc.

◆ CreateNoOverlapPrecedenceCutGenerator()

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

Definition at line 2347 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 2216 of file cuts.cc.

◆ CreatePositiveMultiplicationCutGenerator()

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

Definition at line 1327 of file cuts.cc.

◆ CreateSquareCutGenerator()

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

Definition at line 1423 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 2512 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 154 of file cumulative.cc.

◆ DecisionStrategyProto_DomainReductionStrategy_descriptor()

const ::PROTOBUF_NAMESPACE_ID::EnumDescriptor * DecisionStrategyProto_DomainReductionStrategy_descriptor ( )

Definition at line 1004 of file cp_model.pb.cc.

◆ DecisionStrategyProto_DomainReductionStrategy_IsValid()

bool DecisionStrategyProto_DomainReductionStrategy_IsValid ( int value )

Definition at line 1008 of file cp_model.pb.cc.

◆ DecisionStrategyProto_DomainReductionStrategy_Name()

const std::string& operations_research::sat::DecisionStrategyProto_DomainReductionStrategy_Name ( T enum_t_value )

inline

Definition at line 210 of file cp_model.pb.h.

◆ DecisionStrategyProto_DomainReductionStrategy_Parse()

bool operations_research::sat::DecisionStrategyProto_DomainReductionStrategy_Parse	(	::PROTOBUF_NAMESPACE_ID::ConstStringParam	name,
		DecisionStrategyProto_DomainReductionStrategy *	value
	)

inline

Definition at line 217 of file cp_model.pb.h.

◆ DecisionStrategyProto_VariableSelectionStrategy_descriptor()

const ::PROTOBUF_NAMESPACE_ID::EnumDescriptor * DecisionStrategyProto_VariableSelectionStrategy_descriptor ( )

Definition at line 977 of file cp_model.pb.cc.

◆ DecisionStrategyProto_VariableSelectionStrategy_IsValid()

bool DecisionStrategyProto_VariableSelectionStrategy_IsValid ( int value )

Definition at line 981 of file cp_model.pb.cc.

◆ DecisionStrategyProto_VariableSelectionStrategy_Name()

const std::string& operations_research::sat::DecisionStrategyProto_VariableSelectionStrategy_Name ( T enum_t_value )

inline

Definition at line 182 of file cp_model.pb.h.

◆ DecisionStrategyProto_VariableSelectionStrategy_Parse()

bool operations_research::sat::DecisionStrategyProto_VariableSelectionStrategy_Parse	(	::PROTOBUF_NAMESPACE_ID::ConstStringParam	name,
		DecisionStrategyProto_VariableSelectionStrategy *	value
	)

inline

Definition at line 189 of file cp_model.pb.h.

◆ 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
	)

◆ DetectDominanceRelations()

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

Definition at line 677 of file var_domination.cc.

◆ DetectEquivalencesInElementConstraint()

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

Definition at line 1333 of file cp_model_loader.cc.

◆ DetectImpliedIntegers()

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

Definition at line 235 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 978 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 153 of file disjunctive.cc.

◆ DisjunctiveWithBooleanPrecedencesOnly()

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

Definition at line 130 of file disjunctive.cc.

◆ DivideByGCD()

void DivideByGCD ( LinearConstraint * constraint )

Definition at line 188 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 951 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 1507 of file integer.h.

◆ Equality() [3/3]

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

inline

Definition at line 927 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 877 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 1016 of file sat_solver.h.

◆ ExcludeCurrentSolutionWithoutIgnoredVariableAndBacktrack()

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

Definition at line 1960 of file integer.cc.

◆ ExpandCpModel()

void ExpandCpModel	(	PresolveOptions	options,
		PresolveContext *	context
	)

Definition at line 1496 of file cp_model_expand.cc.

◆ ExploitDominanceRelations()

bool ExploitDominanceRelations	(	const VarDomination &	var_domination,
		PresolveContext *	context
	)

Definition at line 864 of file var_domination.cc.

◆ ExtractAssignment()

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

Definition at line 50 of file boolean_problem.cc.

◆ ExtractSubproblem()

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

Definition at line 486 of file boolean_problem.cc.

◆ FailedLiteralProbingRound()

bool FailedLiteralProbingRound	(	ProbingOptions	options,
		Model *	model
	)

Definition at line 349 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 CpModelProto &	problem,
		std::vector< std::unique_ptr< SparsePermutation >> *	generators,
		double	time_limit_seconds
	)

Definition at line 243 of file cp_model_symmetries.cc.

◆ FindDuplicateConstraints()

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

Definition at line 5147 of file cp_model_presolve.cc.

◆ FindLinearBooleanProblemSymmetries()

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

Definition at line 670 of file boolean_problem.cc.

◆ FindRationalFactor()

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

Definition at line 119 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 1154 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 1570 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 2018 of file cuts.cc.

◆ GenerateGraphForSymmetryDetection()

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

Definition at line 532 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 475 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 335 of file linear_constraint.cc.

◆ GetCoefficientOfPositiveVar()

IntegerValue GetCoefficientOfPositiveVar	(	const IntegerVariable	var,
		const LinearExpression &	expr
	)

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

◆ GetFactorT()

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

Definition at line 615 of file cuts.cc.

◆ GetKnapsackUpperBound()

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

Definition at line 317 of file cuts.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 249 of file cuts.cc.

◆ GetReferencesUsedByConstraint()

IndexReferences GetReferencesUsedByConstraint ( const ConstraintProto & ct )

Definition at line 46 of file cp_model_utils.cc.

◆ GetRINSNeighborhood()

RINSNeighborhood operations_research::sat::GetRINSNeighborhood	(	const SharedResponseManager *	response_manager,
		const SharedRelaxationSolutionRepository *	relaxation_solutions,
		const SharedLPSolutionRepository *	lp_solutions,
		SharedIncompleteSolutionManager *	incomplete_solutions,
		random_engine_t *	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 1685 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 623 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 1478 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 1520 of file integer.h.

◆ Implication() [2/2]

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

inline

Definition at line 920 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 1547 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	master,
		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 360 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 1462 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 171 of file cuts.cc.

◆ LinearBooleanProblemToCnfString()

std::string LinearBooleanProblemToCnfString ( const LinearBooleanProblem & problem )

Definition at line 390 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 292 of file linear_constraint.cc.

◆ LinExprUpperBound()

IntegerValue LinExprUpperBound	(	const LinearExpression &	expr,
		const IntegerTrail &	integer_trail
	)

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

◆ LoadAndConsumeBooleanProblem()

bool LoadAndConsumeBooleanProblem	(	LinearBooleanProblem *	problem,
		SatSolver *	solver
	)

Definition at line 259 of file boolean_problem.cc.

◆ LoadAtMostOneConstraint()

void LoadAtMostOneConstraint	(	const ConstraintProto &	ct,
		Model *	m
	)

Definition at line 969 of file cp_model_loader.cc.

◆ LoadAutomatonConstraint()

void LoadAutomatonConstraint	(	const ConstraintProto &	ct,
		Model *	m
	)

Definition at line 1663 of file cp_model_loader.cc.

◆ LoadBoolAndConstraint()

void LoadBoolAndConstraint	(	const ConstraintProto &	ct,
		Model *	m
	)

Definition at line 955 of file cp_model_loader.cc.

◆ LoadBooleanProblem()

bool LoadBooleanProblem	(	const LinearBooleanProblem &	problem,
		SatSolver *	solver
	)

Definition at line 219 of file boolean_problem.cc.

◆ LoadBoolOrConstraint()

void LoadBoolOrConstraint	(	const ConstraintProto &	ct,
		Model *	m
	)

Definition at line 946 of file cp_model_loader.cc.

◆ LoadBoolXorConstraint()

void LoadBoolXorConstraint	(	const ConstraintProto &	ct,
		Model *	m
	)

Definition at line 975 of file cp_model_loader.cc.

◆ LoadCircuitConstraint()

void LoadCircuitConstraint	(	const ConstraintProto &	ct,
		Model *	m
	)

Definition at line 1715 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 1740 of file cp_model_loader.cc.

◆ LoadCumulativeConstraint()

void LoadCumulativeConstraint	(	const ConstraintProto &	ct,
		Model *	m
	)

Definition at line 1317 of file cp_model_loader.cc.

◆ LoadElementConstraint()

void LoadElementConstraint	(	const ConstraintProto &	ct,
		Model *	m
	)

Definition at line 1565 of file cp_model_loader.cc.

◆ LoadElementConstraintAC()

void LoadElementConstraintAC	(	const ConstraintProto &	ct,
		Model *	m
	)

Definition at line 1443 of file cp_model_loader.cc.

◆ LoadElementConstraintBounds()

void LoadElementConstraintBounds	(	const ConstraintProto &	ct,
		Model *	m
	)

Definition at line 1391 of file cp_model_loader.cc.

◆ LoadIntDivConstraint()

void LoadIntDivConstraint	(	const ConstraintProto &	ct,
		Model *	m
	)

Definition at line 1242 of file cp_model_loader.cc.

◆ LoadIntMaxConstraint()

void LoadIntMaxConstraint	(	const ConstraintProto &	ct,
		Model *	m
	)

Definition at line 1292 of file cp_model_loader.cc.

◆ LoadIntMinConstraint()

void LoadIntMinConstraint	(	const ConstraintProto &	ct,
		Model *	m
	)

Definition at line 1259 of file cp_model_loader.cc.

◆ LoadIntProdConstraint()

void LoadIntProdConstraint	(	const ConstraintProto &	ct,
		Model *	m
	)

Definition at line 1233 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 1055 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 1278 of file cp_model_loader.cc.

◆ LoadNoOverlap2dConstraint()

void LoadNoOverlap2dConstraint	(	const ConstraintProto &	ct,
		Model *	m
	)

Definition at line 1305 of file cp_model_loader.cc.

◆ LoadNoOverlapConstraint()

void LoadNoOverlapConstraint	(	const ConstraintProto &	ct,
		Model *	m
	)

Definition at line 1300 of file cp_model_loader.cc.

◆ LoadRoutesConstraint()

void LoadRoutesConstraint	(	const ConstraintProto &	ct,
		Model *	m
	)

Definition at line 1727 of file cp_model_loader.cc.

◆ LoadTableConstraint()

void LoadTableConstraint	(	const ConstraintProto &	ct,
		Model *	m
	)

Definition at line 1642 of file cp_model_loader.cc.

◆ LogInfoFromContext()

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

Definition at line 4689 of file cp_model_presolve.cc.

◆ LookForTrivialSatSolution()

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

Definition at line 269 of file probing.cc.

◆ LowerBound()

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

inline

Definition at line 1450 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 1492 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 215 of file linear_constraint.cc.

◆ MakeAllLiteralsPositive()

void MakeAllLiteralsPositive ( LinearBooleanProblem * problem )

Definition at line 635 of file boolean_problem.cc.

◆ MakeAllVariablesPositive()

void MakeAllVariablesPositive ( LinearConstraint * constraint )

Definition at line 226 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 937 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	(	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 312 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 1395 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 1418 of file integer.h.

◆ NewIntegerVariable() [2/2]

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

inline

Definition at line 1409 of file integer.h.

◆ NewIntegerVariableFromLiteral()

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

inline

Definition at line 1427 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))

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 264 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 1036 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 320 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 144 of file cp_model_postsolve.cc.

◆ PostsolveIntMax()

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

Definition at line 118 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 52 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 207 of file cp_model_postsolve.cc.

◆ PresolveCpModel()

bool PresolveCpModel	(	const PresolveOptions &	options,
		PresolveContext *	context,
		std::vector< int > *	postsolve_mapping
	)

Definition at line 4710 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 1128 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 76 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 969 of file sat_solver.h.

◆ ReifiedBoolLe()

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

inline

Definition at line 985 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 935 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 182 of file sat/lp_utils.cc.

◆ RemoveZeroTerms()

void RemoveZeroTerms ( LinearConstraint * constraint )

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

◆ SatParameters_BinaryMinizationAlgorithm_descriptor()

const ::PROTOBUF_NAMESPACE_ID::EnumDescriptor * SatParameters_BinaryMinizationAlgorithm_descriptor ( )

Definition at line 666 of file sat_parameters.pb.cc.

◆ SatParameters_BinaryMinizationAlgorithm_IsValid()

bool SatParameters_BinaryMinizationAlgorithm_IsValid ( int value )

Definition at line 670 of file sat_parameters.pb.cc.

◆ SatParameters_BinaryMinizationAlgorithm_Name()

const std::string& operations_research::sat::SatParameters_BinaryMinizationAlgorithm_Name ( T enum_t_value )

inline

Definition at line 159 of file sat_parameters.pb.h.

◆ SatParameters_BinaryMinizationAlgorithm_Parse()

bool operations_research::sat::SatParameters_BinaryMinizationAlgorithm_Parse	(	::PROTOBUF_NAMESPACE_ID::ConstStringParam	name,
		SatParameters_BinaryMinizationAlgorithm *	value
	)

inline

Definition at line 166 of file sat_parameters.pb.h.

◆ SatParameters_ClauseOrdering_descriptor()

const ::PROTOBUF_NAMESPACE_ID::EnumDescriptor * SatParameters_ClauseOrdering_descriptor ( )

Definition at line 716 of file sat_parameters.pb.cc.

◆ SatParameters_ClauseOrdering_IsValid()

bool SatParameters_ClauseOrdering_IsValid ( int value )

Definition at line 720 of file sat_parameters.pb.cc.

◆ SatParameters_ClauseOrdering_Name()

const std::string& operations_research::sat::SatParameters_ClauseOrdering_Name ( T enum_t_value )

inline

Definition at line 206 of file sat_parameters.pb.h.

◆ SatParameters_ClauseOrdering_Parse()

bool operations_research::sat::SatParameters_ClauseOrdering_Parse	(	::PROTOBUF_NAMESPACE_ID::ConstStringParam	name,
		SatParameters_ClauseOrdering *	value
	)

inline

Definition at line 213 of file sat_parameters.pb.h.

◆ SatParameters_ClauseProtection_descriptor()

const ::PROTOBUF_NAMESPACE_ID::EnumDescriptor * SatParameters_ClauseProtection_descriptor ( )

Definition at line 693 of file sat_parameters.pb.cc.

◆ SatParameters_ClauseProtection_IsValid()

bool SatParameters_ClauseProtection_IsValid ( int value )

Definition at line 697 of file sat_parameters.pb.cc.

◆ SatParameters_ClauseProtection_Name()

const std::string& operations_research::sat::SatParameters_ClauseProtection_Name ( T enum_t_value )

inline

Definition at line 183 of file sat_parameters.pb.h.

◆ SatParameters_ClauseProtection_Parse()

bool operations_research::sat::SatParameters_ClauseProtection_Parse	(	::PROTOBUF_NAMESPACE_ID::ConstStringParam	name,
		SatParameters_ClauseProtection *	value
	)

inline

Definition at line 190 of file sat_parameters.pb.h.

◆ SatParameters_ConflictMinimizationAlgorithm_descriptor()

const ::PROTOBUF_NAMESPACE_ID::EnumDescriptor * SatParameters_ConflictMinimizationAlgorithm_descriptor ( )

Definition at line 641 of file sat_parameters.pb.cc.

◆ SatParameters_ConflictMinimizationAlgorithm_IsValid()

bool SatParameters_ConflictMinimizationAlgorithm_IsValid ( int value )

Definition at line 645 of file sat_parameters.pb.cc.

◆ SatParameters_ConflictMinimizationAlgorithm_Name()

const std::string& operations_research::sat::SatParameters_ConflictMinimizationAlgorithm_Name ( T enum_t_value )

inline

Definition at line 133 of file sat_parameters.pb.h.

◆ SatParameters_ConflictMinimizationAlgorithm_Parse()

bool operations_research::sat::SatParameters_ConflictMinimizationAlgorithm_Parse	(	::PROTOBUF_NAMESPACE_ID::ConstStringParam	name,
		SatParameters_ConflictMinimizationAlgorithm *	value
	)

inline

Definition at line 140 of file sat_parameters.pb.h.

◆ SatParameters_FPRoundingMethod_descriptor()

const ::PROTOBUF_NAMESPACE_ID::EnumDescriptor * SatParameters_FPRoundingMethod_descriptor ( )

Definition at line 841 of file sat_parameters.pb.cc.

◆ SatParameters_FPRoundingMethod_IsValid()

bool SatParameters_FPRoundingMethod_IsValid ( int value )

Definition at line 845 of file sat_parameters.pb.cc.

◆ SatParameters_FPRoundingMethod_Name()

const std::string& operations_research::sat::SatParameters_FPRoundingMethod_Name ( T enum_t_value )

inline

Definition at line 333 of file sat_parameters.pb.h.

◆ SatParameters_FPRoundingMethod_Parse()

bool operations_research::sat::SatParameters_FPRoundingMethod_Parse	(	::PROTOBUF_NAMESPACE_ID::ConstStringParam	name,
		SatParameters_FPRoundingMethod *	value
	)

inline

Definition at line 340 of file sat_parameters.pb.h.

◆ SatParameters_MaxSatAssumptionOrder_descriptor()

const ::PROTOBUF_NAMESPACE_ID::EnumDescriptor * SatParameters_MaxSatAssumptionOrder_descriptor ( )

Definition at line 764 of file sat_parameters.pb.cc.

◆ SatParameters_MaxSatAssumptionOrder_IsValid()

bool SatParameters_MaxSatAssumptionOrder_IsValid ( int value )

Definition at line 768 of file sat_parameters.pb.cc.

◆ SatParameters_MaxSatAssumptionOrder_Name()

const std::string& operations_research::sat::SatParameters_MaxSatAssumptionOrder_Name ( T enum_t_value )

inline

Definition at line 256 of file sat_parameters.pb.h.

◆ SatParameters_MaxSatAssumptionOrder_Parse()

bool operations_research::sat::SatParameters_MaxSatAssumptionOrder_Parse	(	::PROTOBUF_NAMESPACE_ID::ConstStringParam	name,
		SatParameters_MaxSatAssumptionOrder *	value
	)

inline

Definition at line 263 of file sat_parameters.pb.h.

◆ SatParameters_MaxSatStratificationAlgorithm_descriptor()

const ::PROTOBUF_NAMESPACE_ID::EnumDescriptor * SatParameters_MaxSatStratificationAlgorithm_descriptor ( )

Definition at line 787 of file sat_parameters.pb.cc.

◆ SatParameters_MaxSatStratificationAlgorithm_IsValid()

bool SatParameters_MaxSatStratificationAlgorithm_IsValid ( int value )

Definition at line 791 of file sat_parameters.pb.cc.

◆ SatParameters_MaxSatStratificationAlgorithm_Name()

const std::string& operations_research::sat::SatParameters_MaxSatStratificationAlgorithm_Name ( T enum_t_value )

inline

Definition at line 280 of file sat_parameters.pb.h.

◆ SatParameters_MaxSatStratificationAlgorithm_Parse()

bool operations_research::sat::SatParameters_MaxSatStratificationAlgorithm_Parse	(	::PROTOBUF_NAMESPACE_ID::ConstStringParam	name,
		SatParameters_MaxSatStratificationAlgorithm *	value
	)

inline

Definition at line 287 of file sat_parameters.pb.h.

◆ SatParameters_Polarity_descriptor()

const ::PROTOBUF_NAMESPACE_ID::EnumDescriptor * SatParameters_Polarity_descriptor ( )

Definition at line 614 of file sat_parameters.pb.cc.

◆ SatParameters_Polarity_IsValid()

bool SatParameters_Polarity_IsValid ( int value )

Definition at line 618 of file sat_parameters.pb.cc.

◆ SatParameters_Polarity_Name()

const std::string& operations_research::sat::SatParameters_Polarity_Name ( T enum_t_value )

inline

Definition at line 108 of file sat_parameters.pb.h.

◆ SatParameters_Polarity_Parse()

bool operations_research::sat::SatParameters_Polarity_Parse	(	::PROTOBUF_NAMESPACE_ID::ConstStringParam	name,
		SatParameters_Polarity *	value
	)

inline

Definition at line 115 of file sat_parameters.pb.h.

◆ SatParameters_RestartAlgorithm_descriptor()

const ::PROTOBUF_NAMESPACE_ID::EnumDescriptor * SatParameters_RestartAlgorithm_descriptor ( )

Definition at line 737 of file sat_parameters.pb.cc.

◆ SatParameters_RestartAlgorithm_IsValid()

bool SatParameters_RestartAlgorithm_IsValid ( int value )

Definition at line 741 of file sat_parameters.pb.cc.

◆ SatParameters_RestartAlgorithm_Name()

const std::string& operations_research::sat::SatParameters_RestartAlgorithm_Name ( T enum_t_value )

inline

Definition at line 232 of file sat_parameters.pb.h.

◆ SatParameters_RestartAlgorithm_Parse()

bool operations_research::sat::SatParameters_RestartAlgorithm_Parse	(	::PROTOBUF_NAMESPACE_ID::ConstStringParam	name,
		SatParameters_RestartAlgorithm *	value
	)

inline

Definition at line 239 of file sat_parameters.pb.h.

◆ SatParameters_SearchBranching_descriptor()

const ::PROTOBUF_NAMESPACE_ID::EnumDescriptor * SatParameters_SearchBranching_descriptor ( )

Definition at line 810 of file sat_parameters.pb.cc.

◆ SatParameters_SearchBranching_IsValid()

bool SatParameters_SearchBranching_IsValid ( int value )

Definition at line 814 of file sat_parameters.pb.cc.

◆ SatParameters_SearchBranching_Name()

const std::string& operations_research::sat::SatParameters_SearchBranching_Name ( T enum_t_value )

inline

Definition at line 308 of file sat_parameters.pb.h.

◆ SatParameters_SearchBranching_Parse()

bool operations_research::sat::SatParameters_SearchBranching_Parse	(	::PROTOBUF_NAMESPACE_ID::ConstStringParam	name,
		SatParameters_SearchBranching *	value
	)

inline

Definition at line 315 of file sat_parameters.pb.h.

◆ SatParameters_VariableOrder_descriptor()

const ::PROTOBUF_NAMESPACE_ID::EnumDescriptor * SatParameters_VariableOrder_descriptor ( )

Definition at line 591 of file sat_parameters.pb.cc.

◆ SatParameters_VariableOrder_IsValid()

bool SatParameters_VariableOrder_IsValid ( int value )

Definition at line 595 of file sat_parameters.pb.cc.

◆ SatParameters_VariableOrder_Name()

const std::string& operations_research::sat::SatParameters_VariableOrder_Name ( T enum_t_value )

inline

Definition at line 82 of file sat_parameters.pb.h.

◆ SatParameters_VariableOrder_Parse()

bool operations_research::sat::SatParameters_VariableOrder_Parse	(	::PROTOBUF_NAMESPACE_ID::ConstStringParam	name,
		SatParameters_VariableOrder *	value
	)

inline

Definition at line 89 of file sat_parameters.pb.h.

◆ 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 149 of file linear_constraint.cc.

◆ ScaleContinuousVariables()

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

Definition at line 100 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 2271 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 36 of file cp_model_utils.cc.

◆ SimplifyCanonicalBooleanLinearConstraint()

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

Definition at line 147 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 930 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 823 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 815 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 807 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 799 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 989 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 3206 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 2878 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 982 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 1190 of file sat/lp_utils.cc.

◆ SolveLpAndUseSolutionForSatAssignmentPreference()

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

Definition at line 1168 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 3211 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 3219 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 1246 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 475 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.

◆ 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 315 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 1456 of file integer.h.

◆ UsedIntervals()

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

Definition at line 444 of file cp_model_utils.cc.

◆ UsedVariables()

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

Definition at line 429 of file cp_model_utils.cc.

◆ UseObjectiveForSatAssignmentPreference()

void UseObjectiveForSatAssignmentPreference	(	const LinearBooleanProblem &	problem,
		SatSolver *	solver
	)

Definition at line 307 of file boolean_problem.cc.

◆ ValidateBooleanProblem()

absl::Status ValidateBooleanProblem ( const LinearBooleanProblem & problem )

Definition at line 131 of file boolean_problem.cc.

◆ ValidateCpModel()

std::string ValidateCpModel ( const CpModelProto & model )

Definition at line 409 of file cp_model_checker.cc.

◆ Value() [1/3]

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

inline

Definition at line 1004 of file sat_solver.h.

◆ Value() [2/3]

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

inline

Definition at line 1470 of file integer.h.

◆ Value() [3/3]

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

inline

Definition at line 995 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

◆ _AllDifferentConstraintProto_default_instance_

AllDifferentConstraintProtoDefaultTypeInternal _AllDifferentConstraintProto_default_instance_

Definition at line 61 of file cp_model.pb.h.

◆ _AutomatonConstraintProto_default_instance_

AutomatonConstraintProtoDefaultTypeInternal _AutomatonConstraintProto_default_instance_

Definition at line 64 of file cp_model.pb.h.

◆ _BoolArgumentProto_default_instance_

BoolArgumentProtoDefaultTypeInternal _BoolArgumentProto_default_instance_

Definition at line 67 of file cp_model.pb.h.

◆ _BooleanAssignment_default_instance_

BooleanAssignmentDefaultTypeInternal _BooleanAssignment_default_instance_

Definition at line 60 of file boolean_problem.pb.h.

◆ _CircuitConstraintProto_default_instance_

CircuitConstraintProtoDefaultTypeInternal _CircuitConstraintProto_default_instance_

Definition at line 70 of file cp_model.pb.h.

◆ _ConstraintProto_default_instance_

ConstraintProtoDefaultTypeInternal _ConstraintProto_default_instance_

Definition at line 73 of file cp_model.pb.h.

◆ _CpModelProto_default_instance_

CpModelProtoDefaultTypeInternal _CpModelProto_default_instance_

Definition at line 76 of file cp_model.pb.h.

◆ _CpObjectiveProto_default_instance_

CpObjectiveProtoDefaultTypeInternal _CpObjectiveProto_default_instance_

Definition at line 79 of file cp_model.pb.h.

◆ _CpSolverResponse_default_instance_

CpSolverResponseDefaultTypeInternal _CpSolverResponse_default_instance_

Definition at line 82 of file cp_model.pb.h.

◆ _CumulativeConstraintProto_default_instance_

CumulativeConstraintProtoDefaultTypeInternal _CumulativeConstraintProto_default_instance_

Definition at line 85 of file cp_model.pb.h.

◆ _DecisionStrategyProto_AffineTransformation_default_instance_

DecisionStrategyProto_AffineTransformationDefaultTypeInternal _DecisionStrategyProto_AffineTransformation_default_instance_

Definition at line 91 of file cp_model.pb.h.

◆ _DecisionStrategyProto_default_instance_

DecisionStrategyProtoDefaultTypeInternal _DecisionStrategyProto_default_instance_

Definition at line 88 of file cp_model.pb.h.

◆ _ElementConstraintProto_default_instance_

ElementConstraintProtoDefaultTypeInternal _ElementConstraintProto_default_instance_

Definition at line 94 of file cp_model.pb.h.

◆ _IntegerArgumentProto_default_instance_

IntegerArgumentProtoDefaultTypeInternal _IntegerArgumentProto_default_instance_

Definition at line 97 of file cp_model.pb.h.

◆ _IntegerVariableProto_default_instance_

IntegerVariableProtoDefaultTypeInternal _IntegerVariableProto_default_instance_

Definition at line 100 of file cp_model.pb.h.

◆ _IntervalConstraintProto_default_instance_

IntervalConstraintProtoDefaultTypeInternal _IntervalConstraintProto_default_instance_

Definition at line 103 of file cp_model.pb.h.

◆ _InverseConstraintProto_default_instance_

InverseConstraintProtoDefaultTypeInternal _InverseConstraintProto_default_instance_

Definition at line 106 of file cp_model.pb.h.

◆ _LinearArgumentProto_default_instance_

LinearArgumentProtoDefaultTypeInternal _LinearArgumentProto_default_instance_

Definition at line 109 of file cp_model.pb.h.

◆ _LinearBooleanConstraint_default_instance_

LinearBooleanConstraintDefaultTypeInternal _LinearBooleanConstraint_default_instance_

Definition at line 63 of file boolean_problem.pb.h.

◆ _LinearBooleanProblem_default_instance_

LinearBooleanProblemDefaultTypeInternal _LinearBooleanProblem_default_instance_

Definition at line 66 of file boolean_problem.pb.h.

◆ _LinearConstraintProto_default_instance_

LinearConstraintProtoDefaultTypeInternal _LinearConstraintProto_default_instance_

Definition at line 112 of file cp_model.pb.h.

◆ _LinearExpressionProto_default_instance_

LinearExpressionProtoDefaultTypeInternal _LinearExpressionProto_default_instance_

Definition at line 115 of file cp_model.pb.h.

◆ _LinearObjective_default_instance_

LinearObjectiveDefaultTypeInternal _LinearObjective_default_instance_

Definition at line 69 of file boolean_problem.pb.h.

◆ _NoOverlap2DConstraintProto_default_instance_

NoOverlap2DConstraintProtoDefaultTypeInternal _NoOverlap2DConstraintProto_default_instance_

Definition at line 118 of file cp_model.pb.h.

◆ _NoOverlapConstraintProto_default_instance_

NoOverlapConstraintProtoDefaultTypeInternal _NoOverlapConstraintProto_default_instance_

Definition at line 121 of file cp_model.pb.h.

◆ _PartialVariableAssignment_default_instance_

PartialVariableAssignmentDefaultTypeInternal _PartialVariableAssignment_default_instance_

Definition at line 124 of file cp_model.pb.h.

◆ _ReservoirConstraintProto_default_instance_

ReservoirConstraintProtoDefaultTypeInternal _ReservoirConstraintProto_default_instance_

Definition at line 127 of file cp_model.pb.h.

◆ _RoutesConstraintProto_default_instance_

RoutesConstraintProtoDefaultTypeInternal _RoutesConstraintProto_default_instance_

Definition at line 130 of file cp_model.pb.h.

◆ _SatParameters_default_instance_

SatParametersDefaultTypeInternal _SatParameters_default_instance_

Definition at line 61 of file sat_parameters.pb.h.

◆ _TableConstraintProto_default_instance_

TableConstraintProtoDefaultTypeInternal _TableConstraintProto_default_instance_

Definition at line 133 of file cp_model.pb.h.

◆ CpSolverStatus_ARRAYSIZE

constexpr int CpSolverStatus_ARRAYSIZE = CpSolverStatus_MAX + 1

constexpr

Definition at line 234 of file cp_model.pb.h.

◆ CpSolverStatus_MAX

constexpr CpSolverStatus CpSolverStatus_MAX = OPTIMAL

constexpr

Definition at line 233 of file cp_model.pb.h.

◆ CpSolverStatus_MIN

constexpr CpSolverStatus CpSolverStatus_MIN = UNKNOWN

constexpr

Definition at line 232 of file cp_model.pb.h.

◆ DecisionStrategyProto_DomainReductionStrategy_DomainReductionStrategy_ARRAYSIZE

constexpr int DecisionStrategyProto_DomainReductionStrategy_DomainReductionStrategy_ARRAYSIZE = DecisionStrategyProto_DomainReductionStrategy_DomainReductionStrategy_MAX + 1

constexpr

Definition at line 206 of file cp_model.pb.h.

◆ DecisionStrategyProto_DomainReductionStrategy_DomainReductionStrategy_MAX

constexpr DecisionStrategyProto_DomainReductionStrategy DecisionStrategyProto_DomainReductionStrategy_DomainReductionStrategy_MAX = DecisionStrategyProto_DomainReductionStrategy_SELECT_MEDIAN_VALUE

constexpr

Definition at line 205 of file cp_model.pb.h.

◆ DecisionStrategyProto_DomainReductionStrategy_DomainReductionStrategy_MIN

constexpr DecisionStrategyProto_DomainReductionStrategy DecisionStrategyProto_DomainReductionStrategy_DomainReductionStrategy_MIN = DecisionStrategyProto_DomainReductionStrategy_SELECT_MIN_VALUE

constexpr

Definition at line 204 of file cp_model.pb.h.

◆ DecisionStrategyProto_VariableSelectionStrategy_VariableSelectionStrategy_ARRAYSIZE

constexpr int DecisionStrategyProto_VariableSelectionStrategy_VariableSelectionStrategy_ARRAYSIZE = DecisionStrategyProto_VariableSelectionStrategy_VariableSelectionStrategy_MAX + 1

constexpr

Definition at line 178 of file cp_model.pb.h.

◆ DecisionStrategyProto_VariableSelectionStrategy_VariableSelectionStrategy_MAX

constexpr DecisionStrategyProto_VariableSelectionStrategy DecisionStrategyProto_VariableSelectionStrategy_VariableSelectionStrategy_MAX = DecisionStrategyProto_VariableSelectionStrategy_CHOOSE_MAX_DOMAIN_SIZE

constexpr

Definition at line 177 of file cp_model.pb.h.

◆ DecisionStrategyProto_VariableSelectionStrategy_VariableSelectionStrategy_MIN

constexpr DecisionStrategyProto_VariableSelectionStrategy DecisionStrategyProto_VariableSelectionStrategy_VariableSelectionStrategy_MIN = DecisionStrategyProto_VariableSelectionStrategy_CHOOSE_FIRST

constexpr

Definition at line 176 of file cp_model.pb.h.

◆ kAffineRelationConstraint

constexpr int kAffineRelationConstraint = -2

constexpr

Definition at line 34 of file presolve_context.h.

◆ kAssumptionsConstraint

constexpr int kAssumptionsConstraint = -3

constexpr

Definition at line 35 of file presolve_context.h.

◆ kObjectiveConstraint

constexpr int kObjectiveConstraint = -1

constexpr

Definition at line 33 of file presolve_context.h.

◆ kUnsatTrailIndex

const int kUnsatTrailIndex = -1

Definition at line 53 of file sat_solver.h.

◆ SatParameters_BinaryMinizationAlgorithm_BinaryMinizationAlgorithm_ARRAYSIZE

constexpr int SatParameters_BinaryMinizationAlgorithm_BinaryMinizationAlgorithm_ARRAYSIZE = SatParameters_BinaryMinizationAlgorithm_BinaryMinizationAlgorithm_MAX + 1

constexpr

Definition at line 155 of file sat_parameters.pb.h.

◆ SatParameters_BinaryMinizationAlgorithm_BinaryMinizationAlgorithm_MAX

constexpr SatParameters_BinaryMinizationAlgorithm SatParameters_BinaryMinizationAlgorithm_BinaryMinizationAlgorithm_MAX = SatParameters_BinaryMinizationAlgorithm_BINARY_MINIMIZATION_FIRST_WITH_TRANSITIVE_REDUCTION

constexpr

Definition at line 154 of file sat_parameters.pb.h.

◆ SatParameters_BinaryMinizationAlgorithm_BinaryMinizationAlgorithm_MIN

constexpr SatParameters_BinaryMinizationAlgorithm SatParameters_BinaryMinizationAlgorithm_BinaryMinizationAlgorithm_MIN = SatParameters_BinaryMinizationAlgorithm_NO_BINARY_MINIMIZATION

constexpr

Definition at line 153 of file sat_parameters.pb.h.

◆ SatParameters_ClauseOrdering_ClauseOrdering_ARRAYSIZE

constexpr int SatParameters_ClauseOrdering_ClauseOrdering_ARRAYSIZE = SatParameters_ClauseOrdering_ClauseOrdering_MAX + 1

constexpr

Definition at line 202 of file sat_parameters.pb.h.

◆ SatParameters_ClauseOrdering_ClauseOrdering_MAX

constexpr SatParameters_ClauseOrdering SatParameters_ClauseOrdering_ClauseOrdering_MAX = SatParameters_ClauseOrdering_CLAUSE_LBD

constexpr

Definition at line 201 of file sat_parameters.pb.h.

◆ SatParameters_ClauseOrdering_ClauseOrdering_MIN

constexpr SatParameters_ClauseOrdering SatParameters_ClauseOrdering_ClauseOrdering_MIN = SatParameters_ClauseOrdering_CLAUSE_ACTIVITY

constexpr

Definition at line 200 of file sat_parameters.pb.h.

◆ SatParameters_ClauseProtection_ClauseProtection_ARRAYSIZE

constexpr int SatParameters_ClauseProtection_ClauseProtection_ARRAYSIZE = SatParameters_ClauseProtection_ClauseProtection_MAX + 1

constexpr

Definition at line 179 of file sat_parameters.pb.h.

◆ SatParameters_ClauseProtection_ClauseProtection_MAX

constexpr SatParameters_ClauseProtection SatParameters_ClauseProtection_ClauseProtection_MAX = SatParameters_ClauseProtection_PROTECTION_LBD

constexpr

Definition at line 178 of file sat_parameters.pb.h.

◆ SatParameters_ClauseProtection_ClauseProtection_MIN

constexpr SatParameters_ClauseProtection SatParameters_ClauseProtection_ClauseProtection_MIN = SatParameters_ClauseProtection_PROTECTION_NONE

constexpr

Definition at line 177 of file sat_parameters.pb.h.

◆ SatParameters_ConflictMinimizationAlgorithm_ConflictMinimizationAlgorithm_ARRAYSIZE

constexpr int SatParameters_ConflictMinimizationAlgorithm_ConflictMinimizationAlgorithm_ARRAYSIZE = SatParameters_ConflictMinimizationAlgorithm_ConflictMinimizationAlgorithm_MAX + 1

constexpr

Definition at line 129 of file sat_parameters.pb.h.

◆ SatParameters_ConflictMinimizationAlgorithm_ConflictMinimizationAlgorithm_MAX

constexpr SatParameters_ConflictMinimizationAlgorithm SatParameters_ConflictMinimizationAlgorithm_ConflictMinimizationAlgorithm_MAX = SatParameters_ConflictMinimizationAlgorithm_EXPERIMENTAL

constexpr

Definition at line 128 of file sat_parameters.pb.h.

◆ SatParameters_ConflictMinimizationAlgorithm_ConflictMinimizationAlgorithm_MIN

constexpr SatParameters_ConflictMinimizationAlgorithm SatParameters_ConflictMinimizationAlgorithm_ConflictMinimizationAlgorithm_MIN = SatParameters_ConflictMinimizationAlgorithm_NONE

constexpr

Definition at line 127 of file sat_parameters.pb.h.

◆ SatParameters_FPRoundingMethod_FPRoundingMethod_ARRAYSIZE

constexpr int SatParameters_FPRoundingMethod_FPRoundingMethod_ARRAYSIZE = SatParameters_FPRoundingMethod_FPRoundingMethod_MAX + 1

constexpr

Definition at line 329 of file sat_parameters.pb.h.

◆ SatParameters_FPRoundingMethod_FPRoundingMethod_MAX

constexpr SatParameters_FPRoundingMethod SatParameters_FPRoundingMethod_FPRoundingMethod_MAX = SatParameters_FPRoundingMethod_ACTIVE_LOCK_BASED

constexpr

Definition at line 328 of file sat_parameters.pb.h.

◆ SatParameters_FPRoundingMethod_FPRoundingMethod_MIN

constexpr SatParameters_FPRoundingMethod SatParameters_FPRoundingMethod_FPRoundingMethod_MIN = SatParameters_FPRoundingMethod_NEAREST_INTEGER

constexpr

Definition at line 327 of file sat_parameters.pb.h.

◆ SatParameters_MaxSatAssumptionOrder_MaxSatAssumptionOrder_ARRAYSIZE

constexpr int SatParameters_MaxSatAssumptionOrder_MaxSatAssumptionOrder_ARRAYSIZE = SatParameters_MaxSatAssumptionOrder_MaxSatAssumptionOrder_MAX + 1

constexpr

Definition at line 252 of file sat_parameters.pb.h.

◆ SatParameters_MaxSatAssumptionOrder_MaxSatAssumptionOrder_MAX

constexpr SatParameters_MaxSatAssumptionOrder SatParameters_MaxSatAssumptionOrder_MaxSatAssumptionOrder_MAX = SatParameters_MaxSatAssumptionOrder_ORDER_ASSUMPTION_BY_WEIGHT

constexpr

Definition at line 251 of file sat_parameters.pb.h.

◆ SatParameters_MaxSatAssumptionOrder_MaxSatAssumptionOrder_MIN

constexpr SatParameters_MaxSatAssumptionOrder SatParameters_MaxSatAssumptionOrder_MaxSatAssumptionOrder_MIN = SatParameters_MaxSatAssumptionOrder_DEFAULT_ASSUMPTION_ORDER

constexpr

Definition at line 250 of file sat_parameters.pb.h.

◆ SatParameters_MaxSatStratificationAlgorithm_MaxSatStratificationAlgorithm_ARRAYSIZE

constexpr int SatParameters_MaxSatStratificationAlgorithm_MaxSatStratificationAlgorithm_ARRAYSIZE = SatParameters_MaxSatStratificationAlgorithm_MaxSatStratificationAlgorithm_MAX + 1

constexpr

Definition at line 276 of file sat_parameters.pb.h.

◆ SatParameters_MaxSatStratificationAlgorithm_MaxSatStratificationAlgorithm_MAX

constexpr SatParameters_MaxSatStratificationAlgorithm SatParameters_MaxSatStratificationAlgorithm_MaxSatStratificationAlgorithm_MAX = SatParameters_MaxSatStratificationAlgorithm_STRATIFICATION_ASCENT

constexpr

Definition at line 275 of file sat_parameters.pb.h.

◆ SatParameters_MaxSatStratificationAlgorithm_MaxSatStratificationAlgorithm_MIN

constexpr SatParameters_MaxSatStratificationAlgorithm SatParameters_MaxSatStratificationAlgorithm_MaxSatStratificationAlgorithm_MIN = SatParameters_MaxSatStratificationAlgorithm_STRATIFICATION_NONE

constexpr

Definition at line 274 of file sat_parameters.pb.h.

◆ SatParameters_Polarity_Polarity_ARRAYSIZE

constexpr int SatParameters_Polarity_Polarity_ARRAYSIZE = SatParameters_Polarity_Polarity_MAX + 1

constexpr

Definition at line 104 of file sat_parameters.pb.h.

◆ SatParameters_Polarity_Polarity_MAX

constexpr SatParameters_Polarity SatParameters_Polarity_Polarity_MAX = SatParameters_Polarity_POLARITY_REVERSE_WEIGHTED_SIGN

constexpr

Definition at line 103 of file sat_parameters.pb.h.

◆ SatParameters_Polarity_Polarity_MIN

constexpr SatParameters_Polarity SatParameters_Polarity_Polarity_MIN = SatParameters_Polarity_POLARITY_TRUE

constexpr

Definition at line 102 of file sat_parameters.pb.h.

◆ SatParameters_RestartAlgorithm_RestartAlgorithm_ARRAYSIZE

constexpr int SatParameters_RestartAlgorithm_RestartAlgorithm_ARRAYSIZE = SatParameters_RestartAlgorithm_RestartAlgorithm_MAX + 1

constexpr

Definition at line 228 of file sat_parameters.pb.h.

◆ SatParameters_RestartAlgorithm_RestartAlgorithm_MAX

constexpr SatParameters_RestartAlgorithm SatParameters_RestartAlgorithm_RestartAlgorithm_MAX = SatParameters_RestartAlgorithm_FIXED_RESTART

constexpr

Definition at line 227 of file sat_parameters.pb.h.

◆ SatParameters_RestartAlgorithm_RestartAlgorithm_MIN

constexpr SatParameters_RestartAlgorithm SatParameters_RestartAlgorithm_RestartAlgorithm_MIN = SatParameters_RestartAlgorithm_NO_RESTART

constexpr

Definition at line 226 of file sat_parameters.pb.h.

◆ SatParameters_SearchBranching_SearchBranching_ARRAYSIZE

constexpr int SatParameters_SearchBranching_SearchBranching_ARRAYSIZE = SatParameters_SearchBranching_SearchBranching_MAX + 1

constexpr

Definition at line 304 of file sat_parameters.pb.h.

◆ SatParameters_SearchBranching_SearchBranching_MAX

constexpr SatParameters_SearchBranching SatParameters_SearchBranching_SearchBranching_MAX = SatParameters_SearchBranching_HINT_SEARCH

constexpr

Definition at line 303 of file sat_parameters.pb.h.

◆ SatParameters_SearchBranching_SearchBranching_MIN

constexpr SatParameters_SearchBranching SatParameters_SearchBranching_SearchBranching_MIN = SatParameters_SearchBranching_AUTOMATIC_SEARCH

constexpr

Definition at line 302 of file sat_parameters.pb.h.

◆ SatParameters_VariableOrder_VariableOrder_ARRAYSIZE

constexpr int SatParameters_VariableOrder_VariableOrder_ARRAYSIZE = SatParameters_VariableOrder_VariableOrder_MAX + 1

constexpr

Definition at line 78 of file sat_parameters.pb.h.

◆ SatParameters_VariableOrder_VariableOrder_MAX

constexpr SatParameters_VariableOrder SatParameters_VariableOrder_VariableOrder_MAX = SatParameters_VariableOrder_IN_RANDOM_ORDER

constexpr

Definition at line 77 of file sat_parameters.pb.h.

◆ SatParameters_VariableOrder_VariableOrder_MIN

constexpr SatParameters_VariableOrder SatParameters_VariableOrder_VariableOrder_MIN = SatParameters_VariableOrder_IN_ORDER

constexpr

Definition at line 76 of file sat_parameters.pb.h.

Namespaces

Classes

Typedefs

Enumerations

Functions

Variables

Typedef Documentation

◆ InlinedIntegerLiteralVector

Enumeration Type Documentation

◆ CpSolverStatus

◆ DecisionStrategyProto_DomainReductionStrategy

◆ DecisionStrategyProto_VariableSelectionStrategy

◆ LogBehavior

◆ SatFormat

◆ SatParameters_BinaryMinizationAlgorithm

◆ SatParameters_ClauseOrdering

◆ SatParameters_ClauseProtection

◆ SatParameters_ConflictMinimizationAlgorithm

◆ SatParameters_FPRoundingMethod

◆ SatParameters_MaxSatAssumptionOrder

◆ SatParameters_MaxSatStratificationAlgorithm

◆ SatParameters_Polarity

◆ SatParameters_RestartAlgorithm

◆ SatParameters_SearchBranching

◆ SatParameters_VariableOrder

Function Documentation

◆ AddCumulativeCut()

◆ AddCumulativeEnergyConstraint()

◆ AddCumulativeOverloadChecker()

◆ AddCumulativeRelaxation()

◆ AddInferedAndDeletedClauses()

◆ AddIntegerVariableFromIntervals()

◆ AddNegatedTableConstraint()

◆ AddObjectiveConstraint()

◆ AddObjectiveUpperBound()

◆ AddOffsetAndScaleObjectiveValue()

◆ AddProblemClauses()

◆ AddProductTo()

◆ AddTableConstraint()

◆ AllDifferentAC()

◆ AllDifferentBinary()

◆ AllDifferentOnBounds()

◆ AllValuesInDomain()

◆ AppendCumulativeRelaxation()

◆ AppendFullEncodingRelaxation()

◆ AppendLinearConstraintRelaxation()

◆ AppendLinMaxRelaxation()

◆ AppendMaxRelaxation()

◆ AppendNoOverlapRelaxation()

◆ AppendPartialEncodingRelaxation()

◆ AppendPartialGreaterThanEncodingRelaxation()

◆ ApplyLiteralMapping()

◆ ApplyLiteralMappingToBooleanProblem()

◆ ApplyToAllIntervalIndices()

◆ ApplyToAllLiteralIndices()

◆ ApplyToAllVariableIndices()

◆ ApplyVariableMapping()

◆ AtMinValue()

◆ AtMostOneConstraint()

◆ BooleanLinearConstraint()

◆ BooleanLinearExpressionIsCanonical()

◆ BooleanProblemToCpModelproto()

◆ CanBeFilteredUsingCutLowerBound()

◆ CanBeFilteredUsingKnapsackUpperBound()

◆ CanFormValidKnapsackCover()

◆ CanonicalizeConstraint()

◆ CanonicalizeExpr()

◆ CardinalityConstraint()

◆ CeilRatio()

◆ ChangeOptimizationDirection()

◆ ChooseBestObjectiveValue()

◆ CircuitCovering()

◆ ClauseConstraint()

◆ CleanTermsAndFillConstraint()

◆ CompleteHeuristics()

◆ CompressTuples()

◆ ComputeActivity()

◆ ComputeBooleanLinearExpressionCanonicalForm()

◆ ComputeCanonicalRhs()

◆ ComputeCoreMinWeight()