package operations_research.sat

Get desktop application:
View/edit binary Protocol Buffers messages

All expressions must take different values.

Used in: ConstraintProto

• repeated LinearExpressionProto exprs = 1

An arc of a routes constraint, with its LP value.

Used in: RoutesSupportGraphProto

• optional int32 tail = 1

• optional int32 head = 2

• optional double lp_value = 3

This constraint forces a sequence of expressions to be accepted by an automaton.

Used in: ConstraintProto

• int64 starting_state = 2

  A state is identified by a non-negative number. It is preferable to keep all the states dense in says [0, num_states). The automaton starts at starting_state and must finish in any of the final states.

• repeated int64 final_states = 3

• repeated int64 transition_tail = 4

  List of transitions (all 3 vectors have the same size). Both tail and head are states, label is any variable value. No two outgoing transitions from the same state can have the same label.

• repeated int64 transition_head = 5

• repeated int64 transition_label = 6

• repeated int32 vars = 7

  Legacy field.

• repeated LinearExpressionProto exprs = 8

  The sequence of expressions. The automaton is ran for exprs_size() "steps" and the value of exprs[i] corresponds to the transition label at step i.

Argument of the constraints of the form OP(literals).

Used in: ConstraintProto

• repeated int32 literals = 1

Stores an assignment of variables as a list of true literals using their signed representation. There will be at most one literal per variable. The literals will be sorted by increasing variable index. The assignment may be partial in the sense that some variables may not appear and thus not be assigned.

Used in: LinearBooleanProblem

• repeated int32 literals = 1

The circuit constraint is defined on a graph where the arc presence are controlled by literals. Each arc is given by an index in the tails/heads/literals lists that must have the same size. For now, we ignore node indices with no incident arc. All the other nodes must have exactly one incoming and one outgoing selected arc (i.e. literal at true). All the selected arcs that are not self-loops must form a single circuit. Note that multi-arcs are allowed, but only one of them will be true at the same time. Multi-self loop are disallowed though.

Used in: ConstraintProto

• repeated int32 tails = 3

• repeated int32 heads = 4

• repeated int32 literals = 5

Next id: 31

Used in: CpModelProto

• string name = 1

  For debug/logging only. Can be empty.

• repeated int32 enforcement_literal = 2

  The constraint will be enforced iff all literals listed here are true. If this is empty, then the constraint will always be enforced. An enforced constraint must be satisfied, and an un-enforced one will simply be ignored. This is also called half-reification. To have an equivalence between a literal and a constraint (full reification), one must add both a constraint (controlled by a literal l) and its negation (controlled by the negation of l). Important: as of September 2025, some constraints might be less efficient with enforcement than without: circuit, routes, no_overlap, no_overlap_2d, and cumulative. If performance is not great, consider using a model without these constraints enforced.

• oneof constraint

  The actual constraint with its arguments.

  • BoolArgumentProto bool_or = 3

    The bool_or constraint forces at least one literal to be true.

  • BoolArgumentProto bool_and = 4

    The bool_and constraint forces all of the literals to be true. This is a "redundant" constraint in the sense that this can easily be encoded with many bool_or or at_most_one. It is just more space efficient and handled slightly differently internally.

  • BoolArgumentProto at_most_one = 26

    The at_most_one constraint enforces that no more than one literal is true at the same time. Note that an at most one constraint of length n could be encoded with n bool_and constraint with n-1 term on the right hand side. So in a sense, this constraint contribute directly to the "implication-graph" or the 2-SAT part of the model.

  • BoolArgumentProto exactly_one = 29

    The exactly_one constraint force exactly one literal to true and no more. Anytime a bool_or (it could have been called at_least_one) is included into an at_most_one, then the bool_or is actually an exactly one constraint, and the extra literal in the at_most_one can be set to false. So in this sense, this constraint is not really needed. it is just here for a better description of the problem structure and to facilitate some algorithm.

  • BoolArgumentProto bool_xor = 5

    The bool_xor constraint forces an odd number of the literals to be true.

  • LinearArgumentProto int_div = 7

    The int_div constraint forces the target to equal exprs[0] / exprs[1]. The division is "rounded" towards zero, so we can have for instance (2 = 12 / 5) or (-3 = -10 / 3). If you only want exact integer division, then you should use instead of t = a / b, the int_prod constraint a = b * t. If 0 belongs to the domain of exprs[1], then the model is deemed invalid.

  • LinearArgumentProto int_mod = 8

    The int_mod constraint forces the target to equal exprs[0] % exprs[1]. The domain of exprs[1] must be strictly positive. The sign of the target is the same as the sign of exprs[0].

  • LinearArgumentProto int_prod = 11

    The int_prod constraint forces the target to equal the product of all variables. By convention, because we can just remove term equal to one, the empty product forces the target to be one. Note that the solver checks for potential integer overflow. So the product of the maximum absolute value of all the terms (using the initial domain) should fit on an int64. Otherwise the model will be declared invalid.

  • LinearArgumentProto lin_max = 27

    The lin_max constraint forces the target to equal the maximum of all linear expressions. Note that this can model a minimum simply by negating all expressions.

  • LinearConstraintProto linear = 12

    The linear constraint enforces a linear inequality among the variables, such as 0 <= x + 2y <= 10.

  • AllDifferentConstraintProto all_diff = 13

    The all_diff constraint forces all variables to take different values.

  • ElementConstraintProto element = 14

    The element constraint forces the variable with the given index to be equal to the target.

  • CircuitConstraintProto circuit = 15

    The circuit constraint takes a graph and forces the arcs present (with arc presence indicated by a literal) to form a unique cycle.

  • RoutesConstraintProto routes = 23

    The routes constraint implements the vehicle routing problem.

  • TableConstraintProto table = 16

    The table constraint enforces what values a tuple of variables may take.

  • AutomatonConstraintProto automaton = 17

    The automaton constraint forces a sequence of variables to be accepted by an automaton.

  • InverseConstraintProto inverse = 18

    The inverse constraint forces two arrays to be inverses of each other: the values of one are the indices of the other, and vice versa.

  • ReservoirConstraintProto reservoir = 24

    The reservoir constraint forces the sum of a set of active demands to always be between a specified minimum and maximum value during specific times.

  • IntervalConstraintProto interval = 19

    The interval constraint takes a start, end, and size, and forces start + size == end.

  • NoOverlapConstraintProto no_overlap = 20

    The no_overlap constraint prevents a set of intervals from overlapping; in scheduling, this is called a disjunctive constraint.

  • NoOverlap2DConstraintProto no_overlap_2d = 21

    The no_overlap_2d constraint prevents a set of boxes from overlapping.

  • CumulativeConstraintProto cumulative = 22

    The cumulative constraint ensures that for any integer point, the sum of the demands of the intervals containing that point does not exceed the capacity.

  • ListOfVariablesProto dummy_constraint = 30

    This constraint is not meant to be used and will be rejected by the solver. It is meant to mark variable when testing the presolve code.

A constraint programming problem.

Used in: v1.CpSolverRequest

• string name = 1

  For debug/logging only. Can be empty.

• repeated IntegerVariableProto variables = 2

  The associated Protos should be referred by their index in these fields.

• repeated ConstraintProto constraints = 3

• optional CpObjectiveProto objective = 4

  The objective to minimize. Can be empty for pure decision problems.

• optional FloatObjectiveProto floating_point_objective = 9

  Advanced usage. It is invalid to have both an objective and a floating point objective. The objective of the model, in floating point format. The solver will automatically scale this to integer during expansion and thus convert it to a normal CpObjectiveProto. See the mip* parameters to control how this is scaled. In most situation the precision will be good enough, but you can see the logs to see what are the precision guaranteed when this is converted to a fixed point representation. Note that even if the precision is bad, the returned objective_value and best_objective_bound will be computed correctly. So at the end of the solve you can check the gap if you only want precise optimal.

• repeated DecisionStrategyProto search_strategy = 5

  Defines the strategy that the solver should follow when the search_branching parameter is set to FIXED_SEARCH. Note that this strategy is also used as a heuristic when we are not in fixed search. Advanced Usage: if not all variables appears and the parameter "instantiate_all_variables" is set to false, then the solver will not try to instantiate the variables that do not appear. Thus, at the end of the search, not all variables may be fixed. Currently, we will set them to their lower bound in the solution.

• optional PartialVariableAssignment solution_hint = 6

  Solution hint. If a feasible or almost-feasible solution to the problem is already known, it may be helpful to pass it to the solver so that it can be used. The solver will try to use this information to create its initial feasible solution. Note that it may not always be faster to give a hint like this to the solver. There is also no guarantee that the solver will use this hint or try to return a solution "close" to this assignment in case of multiple optimal solutions.

• repeated int32 assumptions = 7

  A list of literals. The model will be solved assuming all these literals are true. Compared to just fixing the domain of these literals, using this mechanism is slower but allows in case the model is INFEASIBLE to get a potentially small subset of them that can be used to explain the infeasibility. Think (IIS), except when you are only concerned by the provided assumptions. This is powerful as it allows to group a set of logically related constraint under only one enforcement literal which can potentially give you a good and interpretable explanation for infeasiblity. Such infeasibility explanation will be available in the sufficient_assumptions_for_infeasibility response field.

• optional SymmetryProto symmetry = 8

  For now, this is not meant to be filled by a client writing a model, but by our preprocessing step. Information about the symmetries of the feasible solution space. These usually leaves the objective invariant.

Optimization objective.

Used in: CpModelProto, CpSolverResponse

• repeated int32 vars = 1

  The linear terms of the objective to minimize. For a maximization problem, one can negate all coefficients in the objective and set scaling_factor to -1.

• repeated int64 coeffs = 4

• double offset = 2

  The displayed objective is always: scaling_factor * (sum(coefficients[i] * objective_vars[i]) + offset). This is needed to have a consistent objective after presolve or when scaling a double problem to express it with integers. Note that if scaling_factor is zero, then it is assumed to be 1, so that by default these fields have no effect.

• double scaling_factor = 3

• repeated int64 domain = 5

  If non-empty, only look for an objective value in the given domain. Note that this does not depend on the offset or scaling factor, it is a domain on the sum of the objective terms only.

• bool scaling_was_exact = 6

  Internal field. Do not set. When we scale a FloatObjectiveProto to a integer version, we set this to true if the scaling was exact (i.e. all original coeff were integer for instance). TODO(user): Put the error bounds we computed instead?

• int64 integer_before_offset = 7

  Internal fields to recover a bound on the original integer objective from the presolved one. Basically, initially the integer objective fit on an int64 and is in [Initial_lb, Initial_ub]. During presolve, we might change the linear expression to have a new domain [Presolved_lb, Presolved_ub] that will also always fit on an int64. The two domain will always be linked with an affine transformation between the two of the form: old = (new + before_offset) * integer_scaling_factor + after_offset. Note that we use both offsets to always be able to do the computation while staying in the int64 domain. In particular, the after_offset will always be in (-integer_scaling_factor, integer_scaling_factor).

• int64 integer_after_offset = 9

• int64 integer_scaling_factor = 8

The response returned by a solver trying to solve a CpModelProto. Next id: 32

Used as response type in: v1.CpSolver.SolveProblem

• CpSolverStatus status = 1

  The status of the solve.

• repeated int64 solution = 2

  A feasible solution to the given problem. Depending on the returned status it may be optimal or just feasible. This is in one-to-one correspondence with a CpModelProto::variables repeated field and list the values of all the variables.

• double objective_value = 3

  Only make sense for an optimization problem. The objective value of the returned solution if it is non-empty. If there is no solution, then for a minimization problem, this will be an upper-bound of the objective of any feasible solution, and a lower-bound for a maximization problem.

• double best_objective_bound = 4

  Only make sense for an optimization problem. A proven lower-bound on the objective for a minimization problem, or a proven upper-bound for a maximization problem.

• repeated CpSolverSolution additional_solutions = 27

  If the parameter fill_additional_solutions_in_response is set, then we copy all the solutions from our internal solution pool here. Note that the one returned in the solution field will likely appear here too. Do not rely on the solutions order as it depends on our internal representation (after postsolve).

• repeated IntegerVariableProto tightened_variables = 21

  Advanced usage. If the option fill_tightened_domains_in_response is set, then this field will be a copy of the CpModelProto.variables where each domain has been reduced using the information the solver was able to derive. Note that this is only filled with the info derived during a normal search and we do not have any dedicated algorithm to improve it. Warning: if you didn't set keep_all_feasible_solutions_in_presolve, then these domains might exclude valid feasible solution. Otherwise for a feasibility problem, all feasible solution should be there. Warning: For an optimization problem, these will correspond to valid bounds for the problem of finding an improving solution to the best one found so far. It might be better to solve a feasibility version if one just want to explore the feasible region.

• repeated int32 sufficient_assumptions_for_infeasibility = 23

  A subset of the model "assumptions" field. This will only be filled if the status is INFEASIBLE. This subset of assumption will be enough to still get an infeasible problem. This is related to what is called the irreducible inconsistent subsystem or IIS. Except one is only concerned by the provided assumptions. There is also no guarantee that we return an irreducible (aka minimal subset). However, this is based on SAT explanation and there is a good chance it is not too large. If you really want a minimal subset, a possible way to get one is by changing your model to minimize the number of assumptions at false, but this is likely an harder problem to solve. Important: Currently, this is minimized only in single-thread and if the problem is not an optimization problem, otherwise, it will always include all the assumptions. TODO(user): Allows for returning multiple core at once.

• optional CpObjectiveProto integer_objective = 28

  Contains the integer objective optimized internally. This is only filled if the problem had a floating point objective, and on the final response, not the ones given to callbacks.

• int64 inner_objective_lower_bound = 29

  Advanced usage. A lower bound on the integer expression of the objective. This is either a bound on the expression in the returned integer_objective or on the integer expression of the original objective if the problem already has an integer objective. TODO(user): This should be renamed integer_objective_lower_bound.

• int64 num_integers = 30

  Some statistics about the solve. Important: in multithread, this correspond the statistics of the first subsolver. Which is usually the one with the user defined parameters. Or the default-search if none are specified.

• int64 num_booleans = 10

• int64 num_fixed_booleans = 31

• int64 num_conflicts = 11

• int64 num_branches = 12

• int64 num_binary_propagations = 13

• int64 num_integer_propagations = 14

• int64 num_restarts = 24

• int64 num_lp_iterations = 25

• double wall_time = 15

  The time counted from the beginning of the Solve() call.

• double user_time = 16

• double deterministic_time = 17

• double gap_integral = 22

  The integral of log(1 + absolute_objective_gap) over time.

• string solution_info = 20

  Additional information about how the solution was found. It also stores model or parameters errors that caused the model to be invalid.

• string solve_log = 26

  The solve log will be filled if the parameter log_to_response is set to true.

Just a message used to store dense solution. This is used by the additional_solutions field.

Used in: CpSolverResponse

• repeated int64 values = 1

The status returned by a solver trying to solve a CpModelProto.

Used in: CpSolverResponse

• UNKNOWN = 0

  The status of the model is still unknown. A search limit has been reached before any of the statuses below could be determined.

• MODEL_INVALID = 1

  The given CpModelProto didn't pass the validation step. You can get a detailed error by calling ValidateCpModel(model_proto).

• FEASIBLE = 2

  A feasible solution has been found. But the search was stopped before we could prove optimality or before we enumerated all solutions of a feasibility problem (if asked).

• INFEASIBLE = 3

  The problem has been proven infeasible.

• OPTIMAL = 4

  An optimal feasible solution has been found. More generally, this status represent a success. So we also return OPTIMAL if we find a solution for a pure feasibility problem or if a gap limit has been specified and we return a solution within this limit. In the case where we need to return all the feasible solution, this status will only be returned if we enumerated all of them; If we stopped before, we will return FEASIBLE.

The sum of the demands of the intervals at each interval point cannot exceed a capacity. Note that intervals are interpreted as [start, end) and as such intervals like [2,3) and [3,4) do not overlap for the point of view of this constraint. Moreover, intervals of size zero are ignored. All demands must not contain any negative value in their domains. This is checked at validation. Even if there are no intervals, this constraint implicit enforces capacity >= 0. In other words, a negative capacity is considered valid but always infeasible.

Used in: ConstraintProto

• optional LinearExpressionProto capacity = 1

• repeated int32 intervals = 2

• repeated LinearExpressionProto demands = 3

  Same size as intervals.

Define the strategy to follow when the solver needs to take a new decision. Note that this strategy is only defined on a subset of variables.

Used in: CpModelProto

• repeated int32 variables = 1

  The variables to be considered for the next decision. The order matter and is always used as a tie-breaker after the variable selection strategy criteria defined below.

• repeated LinearExpressionProto exprs = 5

  If this is set, then the variables field must be empty. We currently only support affine expression. Note that this is needed so that if a variable has an affine representative, we can properly transform a DecisionStrategyProto through presolve.

• DecisionStrategyProto.VariableSelectionStrategy variable_selection_strategy = 2

• DecisionStrategyProto.DomainReductionStrategy domain_reduction_strategy = 3

Once a variable (resp. affine expression) has been chosen, this enum describe what decision is taken on its domain. TODO(user): extend as needed.

Used in: DecisionStrategyProto

• SELECT_MIN_VALUE = 0

• SELECT_MAX_VALUE = 1

• SELECT_LOWER_HALF = 2

• SELECT_UPPER_HALF = 3

• SELECT_MEDIAN_VALUE = 4

• SELECT_RANDOM_HALF = 5

The order in which the variables (resp. affine expression) above should be considered. Note that only variables that are not already fixed are considered. TODO(user): extend as needed.

Used in: DecisionStrategyProto

• CHOOSE_FIRST = 0

• CHOOSE_LOWEST_MIN = 1

• CHOOSE_HIGHEST_MAX = 2

• CHOOSE_MIN_DOMAIN_SIZE = 3

• CHOOSE_MAX_DOMAIN_SIZE = 4

A dense matrix of numbers encoded in a flat way, row by row. That is matrix[i][j] = entries[i * num_cols + j];

Used in: SymmetryProto

• int32 num_rows = 1

• int32 num_cols = 2

• repeated int32 entries = 3

The constraint linear_target = exprs[linear_index]. This enforces that index takes one of the value in [0, vars_size()).

Used in: ConstraintProto

• int32 index = 1

  Legacy field.

• int32 target = 2

  Legacy field.

• repeated int32 vars = 3

  Legacy field.

• optional LinearExpressionProto linear_index = 4

• optional LinearExpressionProto linear_target = 5

• repeated LinearExpressionProto exprs = 6

A linear floating point objective: sum coeffs[i] * vars[i] + offset. Note that the variable can only still take integer value.

Used in: CpModelProto

• repeated int32 vars = 1

• repeated double coeffs = 2

• double offset = 3

• bool maximize = 4

  The optimization direction. The default is to minimize

An integer variable. It will be referred to by an int32 corresponding to its index in a CpModelProto variables field. Depending on the context, a reference to a variable whose domain is in [0, 1] can also be seen as a Boolean that will be true if the variable value is 1 and false if it is 0. When used in this context, the field name will always contain the word "literal". Negative reference (advanced usage): to simplify the creation of a model and for efficiency reasons, all the "literal" or "variable" fields can also contain a negative index. A negative index i will refer to the negation of the integer variable at index -i -1 or to NOT the literal at the same index. Ex: A variable index 4 will refer to the integer variable model.variables(4) and an index of -5 will refer to the negation of the same variable. A literal index 4 will refer to the logical fact that model.variable(4) == 1 and a literal index of -5 will refer to the logical fact model.variable(4) == 0.

Used in: CpModelProto, CpSolverResponse

• string name = 1

  For debug/logging only. Can be empty.

• repeated int64 domain = 2

  The variable domain given as a sorted list of n disjoint intervals [min, max] and encoded as [min_0, max_0, ..., min_{n-1}, max_{n-1}]. The most common example being just [min, max]. If min == max, then this is a constant variable. We have: - domain_size() is always even. - min == domain.front(); - max == domain.back(); - for all i < n : min_i <= max_i - for all i < n-1 : max_i + 1 < min_{i+1}. Note that we check at validation that a variable domain is small enough so that we don't run into integer overflow in our algorithms. Because of that, you cannot just have "unbounded" variable like [0, kint64max] and should try to specify tighter domains.

This is not really a constraint. It is there so it can be referred by other constraints using this "interval" concept. IMPORTANT: For now, this constraint do not enforce any relations on the components, and it is up to the client to add in the model: - enforcement => start + size == end. - enforcement => size >= 0 // Only needed if size is not already >= 0.

Used in: ConstraintProto

• optional LinearExpressionProto start = 4

• optional LinearExpressionProto end = 5

• optional LinearExpressionProto size = 6

The two arrays of variable each represent a function, the second is the inverse of the first: f_direct[i] == j <=> f_inverse[j] == i.

Used in: ConstraintProto

• repeated int32 f_direct = 1

• repeated int32 f_inverse = 2

Used in: ConstraintProto

• optional LinearExpressionProto target = 1

• repeated LinearExpressionProto exprs = 2

A linear Boolean constraint which is a bounded sum of linear terms. Each term beeing a literal times an integer coefficient. If we assume that a literal takes the value 1 if it is true and 0 otherwise, the constraint is: lower_bound <= ... + coefficients[i] * literals[i] + ... <= upper_bound

Used in: LinearBooleanProblem

• repeated int32 literals = 1

  Linear terms involved in this constraint. literals[i] is the signed representation of the i-th literal of the constraint and coefficients[i] its coefficients. The signed representation is as follow: for a 0-based variable index x, (x + 1) represents the variable x and -(x + 1) represents its negation. Note that the same variable shouldn't appear twice and that zero coefficients are not allowed.

• repeated int64 coefficients = 2

• optional int64 lower_bound = 3

  Optional lower (resp. upper) bound of the constraint. If not present, it means that the constraint is not bounded in this direction. The bounds are INCLUSIVE.

• optional int64 upper_bound = 4

• optional string name = 5

  The name of this constraint.

A linear Boolean problem.

• optional string name = 1

  The name of the problem.

• optional int32 num_variables = 3

  The number of variables in the problem. All the signed representation of the problem literals must be in [-num_variables, num_variables], excluding 0.

• repeated LinearBooleanConstraint constraints = 4

  The constraints of the problem.

• optional LinearObjective objective = 5

  The objective of the problem. If left empty, we just have a satisfiability problem.

• repeated string var_names = 6

  The names of the problem variables. The variables index are 0-based and var_names[i] will be the name of the i-th variable which correspond to literals +(i + 1) or -(i + 1). This is optional and can be left empty.

• optional BooleanAssignment assignment = 7

  Stores an assignment of the problem variables. That may be an initial feasible solution, just a partial assignment or the optimal solution.

• optional int32 original_num_variables = 8

  Hack: When converting a wcnf formulat to a LinearBooleanProblem, extra variables need to be created. This stores the number of variables in the original problem (which are in one to one correspondence with the first variables of this problem).

The linear sum vars[i] * coeffs[i] must fall in the given domain. The domain has the same format as the one in IntegerVariableProto. Note that the validation code currently checks using the domain of the involved variables that the sum can always be computed without integer overflow and throws an error otherwise.

Used in: ConstraintProto

• repeated int32 vars = 1

• repeated int64 coeffs = 2

  Same size as vars.

• repeated int64 domain = 3

Some constraints supports linear expression instead of just using a reference to a variable. This is especially useful during presolve to reduce the model size.

Used in: AllDifferentConstraintProto, AutomatonConstraintProto, CumulativeConstraintProto, DecisionStrategyProto, ElementConstraintProto, IntervalConstraintProto, LinearArgumentProto, ReservoirConstraintProto, RoutesConstraintProto.NodeExpressions, TableConstraintProto

• repeated int32 vars = 1

• repeated int64 coeffs = 2

• int64 offset = 3

The objective of an optimization problem.

Used in: LinearBooleanProblem

• repeated int32 literals = 1

  The goal is always to minimize the linear Boolean formula defined by these two fields: sum_i literal_i * coefficient_i where literal_i is 1 iff literal_i is true in a given assignment. Note that the same variable shouldn't appear twice and that zero coefficients are not allowed.

• repeated int64 coefficients = 2

• optional double offset = 3

  For a given variable assignment, the "real" problem objective value is 'scaling_factor * (minimization_objective + offset)' where 'minimization_objective is the one defined just above. Note that this is not what we minimize, but it is what we display. In particular if scaling_factor is negative, then the "real" problem is a maximization problem, even if the "internal" objective is minimized.

• optional double scaling_factor = 4

A list of variables, without any semantics.

Used in: ConstraintProto

• repeated int32 vars = 1

A list of clauses to delete.

Used in: LratProofStep

• repeated int64 clause_ids = 1

  IDs of the imported or inferred clauses to delete. A deleted clause can no longer be used to infer clauses.

A clause to export, so that it can be imported from any worker. This is not needed for unary and binary clauses, which are always exported.

Used in: LratProofStep

• optional int64 clause_id = 1

• repeated int32 literals = 2

A clause imported from the input problem, or from another worker.

Used in: LratProofStep

• optional int64 clause_id = 1

• repeated int32 literals = 2

An LRAT inferred clause.

Used in: LratProofStep

• optional int64 clause_id = 1

• repeated int32 literals = 2

  Literals are represented with LiteralIndex values.

• repeated int64 unit_ids = 3

  Clauses which become unit and possibly empty if all the `literals` are assumed to be false (verification stops at the first empty clause). This list must be in unit propagation order. See LratChecker for more details.

• repeated LratInferredClause.RatInfo rat_infos = 4

• optional bool exported = 5

  Whether the clause must be exported, so that other workers can import it (a clause cannot be imported if it is not previously exported). This is not needed for unary and binary clauses, which are always exported.

If `rat_infos` is empty, the last `unit_ids` clause must become empty after unit propagation. If the last `unit_ids` clause does not become empty by unit propagation, then `rat_infos` must contain all the clauses which contain the negation of the first `literals` (called the pivot 'p') -- and no other clauses. Moreover, for each r in `rat_infos`, all the `r.unit_ids` clauses must become unit and eventually empty if all the literals of the `r.resolvant_id` clause (minus ~p), plus those in `literals`, are assumed to be false (this list must be in unit propagation order; verification stops at the first empty clause). See LratChecker for more details.

Used in: LratInferredClause

• optional int64 resolvant_id = 1

• repeated int64 unit_ids = 2

An LRAT UNSAT proof is a sequence of steps, starting from imported clauses and ending with the empty clause. At each step new clauses can be inferred from previous ones (with an explicit proof), or imported from another proof built by another thread. A proof step can also delete clauses which are no longer needed, or export a clause for other workers to import. Each clause is identified by a unique clause ID.

• oneof step

  • LratImportedClause imported_clause = 1

  • LratInferredClause inferred_clause = 2

  • LratExportedClause exported_clause = 3

  • LratDeletedClauses deleted_clauses = 4

The boxes defined by [start_x, end_x) * [start_y, end_y) cannot overlap. Furthermore, one box is optional if at least one of the x or y interval is optional. Note that the case of boxes of size zero is special. The following cases violate the constraint: - a point box inside a box with a non zero area - a line box overlapping a box with a non zero area - one vertical line box crossing an horizontal line box.

Used in: ConstraintProto

• repeated int32 x_intervals = 1

• repeated int32 y_intervals = 2

  Same size as x_intervals.

All the intervals (index of IntervalConstraintProto) must be disjoint. More formally, there must exist a sequence so that for each consecutive intervals, we have end_i <= start_{i+1}. In particular, intervals of size zero do matter for this constraint. This is also known as a disjunctive constraint in scheduling.

Used in: ConstraintProto

• repeated int32 intervals = 1

This message encodes a partial (or full) assignment of the variables of a CpModelProto. The variable indices should be unique and valid variable indices.

Used in: CpModelProto

• repeated int32 vars = 1

• repeated int64 values = 2

Maintain a reservoir level within bounds. The water level starts at 0, and at any time, it must be within [min_level, max_level]. If the variable active_literals[i] is true, and if the expression time_exprs[i] is assigned a value t, then the current level changes by level_changes[i] at the time t. Therefore, at any time t: sum(level_changes[i] * active_literals[i] if time_exprs[i] <= t) in [min_level, max_level] Note that min level must be <= 0, and the max level must be >= 0. Please use fixed level_changes to simulate initial state. The array of boolean variables 'actives', if defined, indicates which actions are actually performed. If this array is not defined, then it is assumed that all actions will be performed.

Used in: ConstraintProto

• int64 min_level = 1

• int64 max_level = 2

• repeated LinearExpressionProto time_exprs = 3

• repeated LinearExpressionProto level_changes = 6

• repeated int32 active_literals = 5

The "VRP" (Vehicle Routing Problem) constraint. The direct graph where arc #i (from tails[i] to head[i]) is present iff literals[i] is true must satisfy this set of properties: - #incoming arcs == 1 except for node 0. - #outgoing arcs == 1 except for node 0. - for node zero, #incoming arcs == #outgoing arcs. - There are no duplicate arcs. - Self-arcs are allowed except for node 0. - There is no cycle in this graph, except through node 0. Note: Currently this constraint expects all the nodes in [0, num_nodes) to have at least one incident arc. The model will be considered invalid if it is not the case. You can add self-arc fixed to one to ignore some nodes if needed. TODO(user): It is probably possible to generalize this constraint to a no-cycle in a general graph, or a no-cycle with sum incoming <= 1 and sum outgoing <= 1 (more efficient implementation). On the other hand, having this specific constraint allow us to add specific "cuts" to a VRP problem.

Used in: ConstraintProto

• repeated int32 tails = 1

• repeated int32 heads = 2

• repeated int32 literals = 3

• repeated int32 demands = 4

  DEPRECATED. These fields are no longer used. The solver ignores them.

• int64 capacity = 5

• repeated RoutesConstraintProto.NodeExpressions dimensions = 6

  Expressions associated with the nodes of the graph, such as the load of the vehicle arriving at a node, or the time at which a vehicle arrives at a node. Expressions with the same "dimension" (such as "load" or "time") must be listed together. This field is optional. If it is set, the linear constraints of size 1 or 2 between the variables in these expressions will be used to derive cuts for this constraint. If it is not set, the solver will try to automatically derive it, from the linear constraints of size 1 or 2 in the model (this can fail in complex cases).

A set of linear expressions associated with the nodes.

Used in: RoutesConstraintProto

• repeated LinearExpressionProto exprs = 1

  The i-th element is the linear expression associated with the i-th node.

The arcs of a routes constraint which have non-zero LP values, in the LP relaxation of the problem.

• repeated ArcLpValue arc_lp_values = 1

Contains the definitions for all the sat algorithm parameters and their default values. NEXT TAG: 356

Used in: RoutingSearchParameters, math_opt.SolveParametersProto, v1.CpSolverRequest

• optional string name = 171

  In some context, like in a portfolio of search, it makes sense to name a given parameters set for logging purpose.

• optional SatParameters.VariableOrder preferred_variable_order = 1

• optional SatParameters.Polarity initial_polarity = 2

• optional bool use_phase_saving = 44

  If this is true, then the polarity of a variable will be the last value it was assigned to, or its default polarity if it was never assigned since the call to ResetDecisionHeuristic(). Actually, we use a newer version where we follow the last value in the longest non-conflicting partial assignment in the current phase. This is called 'literal phase saving'. For details see 'A Lightweight Component Caching Scheme for Satisfiability Solvers' K. Pipatsrisawat and A.Darwiche, In 10th International Conference on Theory and Applications of Satisfiability Testing, 2007.

• optional int32 polarity_rephase_increment = 168

  If non-zero, then we change the polarity heuristic after that many number of conflicts in an arithmetically increasing fashion. So x the first time, 2 * x the second time, etc...

• optional bool polarity_exploit_ls_hints = 309

  If true and we have first solution LS workers, tries in some phase to follow a LS solutions that violates has litle constraints as possible.

• optional double random_polarity_ratio = 45

  The proportion of polarity chosen at random. Note that this take precedence over the phase saving heuristic. This is different from initial_polarity:POLARITY_RANDOM because it will select a new random polarity each time the variable is branched upon instead of selecting one initially and then always taking this choice.

• optional double random_branches_ratio = 32

  A number between 0 and 1 that indicates the proportion of branching variables that are selected randomly instead of choosing the first variable from the given variable_ordering strategy.

• optional bool use_erwa_heuristic = 75

  Whether we use the ERWA (Exponential Recency Weighted Average) heuristic as described in "Learning Rate Based Branching Heuristic for SAT solvers", J.H.Liang, V. Ganesh, P. Poupart, K.Czarnecki, SAT 2016.

• optional double initial_variables_activity = 76

  The initial value of the variables activity. A non-zero value only make sense when use_erwa_heuristic is true. Experiments with a value of 1e-2 together with the ERWA heuristic showed slighthly better result than simply using zero. The idea is that when the "learning rate" of a variable becomes lower than this value, then we prefer to branch on never explored before variables. This is not in the ERWA paper.

• optional bool also_bump_variables_in_conflict_reasons = 77

  When this is true, then the variables that appear in any of the reason of the variables in a conflict have their activity bumped. This is addition to the variables in the conflict, and the one that were used during conflict resolution.

• optional SatParameters.ConflictMinimizationAlgorithm minimization_algorithm = 4

• optional SatParameters.BinaryMinizationAlgorithm binary_minimization_algorithm = 34

• optional bool subsumption_during_conflict_analysis = 56

  At a really low cost, during the 1-UIP conflict computation, it is easy to detect if some of the involved reasons are subsumed by the current conflict. When this is true, such clauses are detached and later removed from the problem.

• optional bool extra_subsumption_during_conflict_analysis = 351

  It is possible that "intermediate" clauses during conflict resolution subsumes some of the clauses that propagated. This is quite cheap to detect and result in more subsumption/strengthening of clauses.

• optional bool decision_subsumption_during_conflict_analysis = 353

  Try even more subsumption options during conflict analysis.

• optional int32 eagerly_subsume_last_n_conflicts = 343

  If >=0, each time we have a conflict, we try to subsume the last n learned clause with it.

• optional bool subsume_during_vivification = 355

  If we remove clause that we now are "implied" by others. Note that this might not always be good as we might loose some propagation power.

• optional bool use_chronological_backtracking = 330

  If true, try to backtrack as little as possible on conflict and re-imply the clauses later. This means we discard less propagation than traditional backjumping, but requites additional bookkeeping to handle reimplication. See: https://doi.org/10.1007/978-3-319-94144-8_7

• optional int32 max_backjump_levels = 331

  If chronological backtracking is enabled, this is the maximum number of levels we will backjump over, otherwise we will backtrack.

• optional int32 chronological_backtrack_min_conflicts = 332

  If chronological backtracking is enabled, this is the minimum number of conflicts before we will consider backjumping.

• optional int32 clause_cleanup_period = 11

  Trigger a cleanup when this number of "deletable" clauses is learned.

• optional int32 clause_cleanup_period_increment = 337

  Increase clause_cleanup_period by this amount after each cleanup.

• optional int32 clause_cleanup_target = 13

  During a cleanup, we will always keep that number of "deletable" clauses. Note that this doesn't include the "protected" clauses.

• optional double clause_cleanup_ratio = 190

  During a cleanup, if clause_cleanup_target is 0, we will delete the clause_cleanup_ratio of "deletable" clauses instead of aiming for a fixed target of clauses to keep.

• optional int32 clause_cleanup_lbd_bound = 59

  All the clauses with a LBD (literal blocks distance) lower or equal to this parameters will always be kept. Note that the LBD of a clause that just propagated is 1 + number of different decision levels of its literals. So that the "classic" LBD of a learned conflict is the same as its LBD when we backjump and then propagate it.

• optional int32 clause_cleanup_lbd_tier1 = 349

  All the clause with a LBD lower or equal to this will be kept except if its activity hasn't been bumped in the last 32 cleanup phase. Note that this has no effect if it is <= clause_cleanup_lbd_bound.

• optional int32 clause_cleanup_lbd_tier2 = 350

  All the clause with a LBD lower or equal to this will be kept except if its activity hasn't been bumped since the previous cleanup phase. Note that this has no effect if it is <= clause_cleanup_lbd_bound or <= clause_cleanup_lbd_tier1.

• optional SatParameters.ClauseOrdering clause_cleanup_ordering = 60

• optional int32 pb_cleanup_increment = 46

  Same as for the clauses, but for the learned pseudo-Boolean constraints.

• optional double pb_cleanup_ratio = 47

• optional double variable_activity_decay = 15

  Each time a conflict is found, the activities of some variables are increased by one. Then, the activity of all variables are multiplied by variable_activity_decay. To implement this efficiently, the activity of all the variables is not decayed at each conflict. Instead, the activity increment is multiplied by 1 / decay. When an activity reach max_variable_activity_value, all the activity are multiplied by 1 / max_variable_activity_value.

• optional double max_variable_activity_value = 16

• optional double glucose_max_decay = 22

  The activity starts at 0.8 and increment by 0.01 every 5000 conflicts until 0.95. This "hack" seems to work well and comes from: Glucose 2.3 in the SAT 2013 Competition - SAT Competition 2013 http://edacc4.informatik.uni-ulm.de/SC13/solver-description-download/136

• optional double glucose_decay_increment = 23

• optional int32 glucose_decay_increment_period = 24

• optional double clause_activity_decay = 17

  Clause activity parameters (same effect as the one on the variables).

• optional double max_clause_activity_value = 18

• repeated SatParameters.RestartAlgorithm restart_algorithms = 61

  The restart strategies will change each time the strategy_counter is increased. The current strategy will simply be the one at index strategy_counter modulo the number of strategy. Note that if this list includes a NO_RESTART, nothing will change when it is reached because the strategy_counter will only increment after a restart. The idea of switching of search strategy tailored for SAT/UNSAT comes from Chanseok Oh with his COMiniSatPS solver, see http://cs.nyu.edu/~chanseok/. But more generally, it seems REALLY beneficial to try different strategy.

• optional string default_restart_algorithms = 70

• optional int32 restart_period = 30

  Restart period for the FIXED_RESTART strategy. This is also the multiplier used by the LUBY_RESTART strategy.

• optional int32 restart_running_window_size = 62

  Size of the window for the moving average restarts.

• optional double restart_dl_average_ratio = 63

  In the moving average restart algorithms, a restart is triggered if the window average times this ratio is greater that the global average.

• optional double restart_lbd_average_ratio = 71

• optional bool use_blocking_restart = 64

  Block a moving restart algorithm if the trail size of the current conflict is greater than the multiplier times the moving average of the trail size at the previous conflicts.

• optional int32 blocking_restart_window_size = 65

• optional double blocking_restart_multiplier = 66

• optional int32 num_conflicts_before_strategy_changes = 68

  After each restart, if the number of conflict since the last strategy change is greater that this, then we increment a "strategy_counter" that can be use to change the search strategy used by the following restarts.

• optional double strategy_change_increase_ratio = 69

  The parameter num_conflicts_before_strategy_changes is increased by that much after each strategy change.

• optional double max_time_in_seconds = 36

  Maximum time allowed in seconds to solve a problem. The counter will starts at the beginning of the Solve() call.

• optional double max_deterministic_time = 67

  Maximum time allowed in deterministic time to solve a problem. The deterministic time should be correlated with the real time used by the solver, the time unit being as close as possible to a second.

• optional int32 max_num_deterministic_batches = 291

  Stops after that number of batches has been scheduled. This only make sense when interleave_search is true.

• optional int64 max_number_of_conflicts = 37

  Maximum number of conflicts allowed to solve a problem. TODO(user): Maybe change the way the conflict limit is enforced? currently it is enforced on each independent internal SAT solve, rather than on the overall number of conflicts across all solves. So in the context of an optimization problem, this is not really usable directly by a client.

  kint64max

• optional int64 max_memory_in_mb = 40

  Maximum memory allowed for the whole thread containing the solver. The solver will abort as soon as it detects that this limit is crossed. As a result, this limit is approximative, but usually the solver will not go too much over. TODO(user): This is only used by the pure SAT solver, generalize to CP-SAT.

• optional double absolute_gap_limit = 159

  Stop the search when the gap between the best feasible objective (O) and our best objective bound (B) is smaller than a limit. The exact definition is: - Absolute: abs(O - B) - Relative: abs(O - B) / max(1, abs(O)). Important: The relative gap depends on the objective offset! If you artificially shift the objective, you will get widely different value of the relative gap. Note that if the gap is reached, the search status will be OPTIMAL. But one can check the best objective bound to see the actual gap. If the objective is integer, then any absolute gap < 1 will lead to a true optimal. If the objective is floating point, a gap of zero make little sense so is is why we use a non-zero default value. At the end of the search, we will display a warning if OPTIMAL is reported yet the gap is greater than this absolute gap.

• optional double relative_gap_limit = 160

• optional int32 random_seed = 31

  At the beginning of each solve, the random number generator used in some part of the solver is reinitialized to this seed. If you change the random seed, the solver may make different choices during the solving process. For some problems, the running time may vary a lot depending on small change in the solving algorithm. Running the solver with different seeds enables to have more robust benchmarks when evaluating new features.

• optional bool permute_variable_randomly = 178

  This is mainly here to test the solver variability. Note that in tests, if not explicitly set to false, all 3 options will be set to true so that clients do not rely on the solver returning a specific solution if they are many equivalent optimal solutions.

• optional bool permute_presolve_constraint_order = 179

• optional bool use_absl_random = 180

• optional bool log_search_progress = 41

  Whether the solver should log the search progress. This is the maing logging parameter and if this is false, none of the logging (callbacks, log_to_stdout, log_to_response, ...) will do anything.

• optional bool log_subsolver_statistics = 189

  Whether the solver should display per sub-solver search statistics. This is only useful is log_search_progress is set to true, and if the number of search workers is > 1. Note that in all case we display a bit of stats with one line per subsolver.

• optional string log_prefix = 185

  Add a prefix to all logs.

• optional bool log_to_stdout = 186

  Log to stdout.

• optional bool log_to_response = 187

  Log to response proto.

• optional bool use_pb_resolution = 43

  Experimental. This is an old experiment, it might cause crashes in multi-thread and you should double check the solver result. It can still be used if you only care about feasible solutions (these are checked) and it gives good result on your problem. We might revive it at some point. Whether to use pseudo-Boolean resolution to analyze a conflict. Note that this option only make sense if your problem is modelized using pseudo-Boolean constraints. If you only have clauses, this shouldn't change anything (except slow the solver down).

• optional bool minimize_reduction_during_pb_resolution = 48

  A different algorithm during PB resolution. It minimizes the number of calls to ReduceCoefficients() which can be time consuming. However, the search space will be different and if the coefficients are large, this may lead to integer overflows that could otherwise be prevented.

• optional bool count_assumption_levels_in_lbd = 49

  Whether or not the assumption levels are taken into account during the LBD computation. According to the reference below, not counting them improves the solver in some situation. Note that this only impact solves under assumptions. Gilles Audemard, Jean-Marie Lagniez, Laurent Simon, "Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction" Theory and Applications of Satisfiability Testing - SAT 2013, Lecture Notes in Computer Science Volume 7962, 2013, pp 309-317.

• optional int32 presolve_bve_threshold = 54

  During presolve, only try to perform the bounded variable elimination (BVE) of a variable x if the number of occurrences of x times the number of occurrences of not(x) is not greater than this parameter.

• optional bool filter_sat_postsolve_clauses = 324

  Internal parameter. During BVE, if we eliminate a variable x, by default we will push all clauses containing x and all clauses containing not(x) to the postsolve. However, it is possible to write the postsolve code so that only one such set is needed. The idea is that, if we push the set containing a literal l, is to set l to false except if it is needed to satisfy one of the clause in the set. This is always beneficial, but for historical reason, not all our postsolve algorithm support this.

• optional int32 presolve_bve_clause_weight = 55

  During presolve, we apply BVE only if this weight times the number of clauses plus the number of clause literals is not increased.

• optional double probing_deterministic_time_limit = 226

  The maximum "deterministic" time limit to spend in probing. A value of zero will disable the probing. TODO(user): Clean up. The first one is used in CP-SAT, the other in pure SAT presolve.

• optional double presolve_probing_deterministic_time_limit = 57

• optional bool presolve_blocked_clause = 88

  Whether we use an heuristic to detect some basic case of blocked clause in the SAT presolve.

• optional bool presolve_use_bva = 72

  Whether or not we use Bounded Variable Addition (BVA) in the presolve.

• optional int32 presolve_bva_threshold = 73

  Apply Bounded Variable Addition (BVA) if the number of clauses is reduced by stricly more than this threshold. The algorithm described in the paper uses 0, but quick experiments showed that 1 is a good value. It may not be worth it to add a new variable just to remove one clause.

• optional int32 max_presolve_iterations = 138

  In case of large reduction in a presolve iteration, we perform multiple presolve iterations. This parameter controls the maximum number of such presolve iterations.

• optional bool cp_model_presolve = 86

  Whether we presolve the cp_model before solving it.

• optional int32 cp_model_probing_level = 110

  How much effort do we spend on probing. 0 disables it completely.

• optional bool cp_model_use_sat_presolve = 93

  Whether we also use the sat presolve when cp_model_presolve is true.

• optional bool load_at_most_ones_in_sat_presolve = 335

  If we try to load at most ones and exactly ones constraints when running the pure SAT presolve. Or if we just ignore them. If one detects at_most_one via merge_at_most_one_work_limit or exactly one with find_clauses_that_are_exactly_one, it might be good to also set this to true.

• optional bool remove_fixed_variables_early = 310

  If cp_model_presolve is true and there is a large proportion of fixed variable after the first model copy, remap all the model to a dense set of variable before the full presolve even starts. This should help for LNS on large models.

• optional bool detect_table_with_cost = 216

  If true, we detect variable that are unique to a table constraint and only there to encode a cost on each tuple. This is usually the case when a WCSP (weighted constraint program) is encoded into CP-SAT format. This can lead to a dramatic speed-up for such problems but is still experimental at this point.

• optional int32 table_compression_level = 217

  How much we try to "compress" a table constraint. Compressing more leads to less Booleans and faster propagation but can reduced the quality of the lp relaxation. Values goes from 0 to 3 where we always try to fully compress a table. At 2, we try to automatically decide if it is worth it.

• optional bool expand_alldiff_constraints = 170

  If true, expand all_different constraints that are not permutations. Permutations (#Variables = #Values) are always expanded.

• optional int32 max_alldiff_domain_size = 320

  Max domain size for all_different constraints to be expanded.

• optional bool expand_reservoir_constraints = 182

  If true, expand the reservoir constraints by creating booleans for all possible precedences between event and encoding the constraint.

• optional int32 max_domain_size_for_linear2_expansion = 340

  Max domain size for expanding linear2 constraints (ax + by ==/!= c).

• optional bool expand_reservoir_using_circuit = 288

  Mainly useful for testing. If this and expand_reservoir_constraints is true, we use a different encoding of the reservoir constraint using circuit instead of precedences. Note that this is usually slower, but can exercise different part of the solver. Note that contrary to the precedence encoding, this easily support variable demands. WARNING: with this encoding, the constraint takes a slightly different meaning. There must exist a permutation of the events occurring at the same time such that the level is within the reservoir after each of these events (in this permuted order). So we cannot have +100 and -100 at the same time if the level must be between 0 and 10 (as authorized by the reservoir constraint).

• optional bool encode_cumulative_as_reservoir = 287

  Encore cumulative with fixed demands and capacity as a reservoir constraint. The only reason you might want to do that is to test the reservoir propagation code!

• optional int32 max_lin_max_size_for_expansion = 280

  If the number of expressions in the lin_max is less that the max size parameter, model expansion replaces target = max(xi) by linear constraint with the introduction of new booleans bi such that bi => target == xi. This is mainly for experimenting compared to a custom lin_max propagator.

• optional bool disable_constraint_expansion = 181

  If true, it disable all constraint expansion. This should only be used to test the presolve of expanded constraints.

• optional bool encode_complex_linear_constraint_with_integer = 223

  Linear constraint with a complex right hand side (more than a single interval) need to be expanded, there is a couple of way to do that.

• optional double merge_no_overlap_work_limit = 145

  During presolve, we use a maximum clique heuristic to merge together no-overlap constraints or at most one constraints. This code can be slow, so we have a limit in place on the number of explored nodes in the underlying graph. The internal limit is an int64, but we use double here to simplify manual input.

• optional double merge_at_most_one_work_limit = 146

• optional int32 presolve_substitution_level = 147

  How much substitution (also called free variable aggregation in MIP litterature) should we perform at presolve. This currently only concerns variable appearing only in linear constraints. For now the value 0 turns it off and any positive value performs substitution.

• optional bool presolve_extract_integer_enforcement = 174

  If true, we will extract from linear constraints, enforcement literals of the form "integer variable at bound => simplified constraint". This should always be beneficial except that we don't always handle them as efficiently as we could for now. This causes problem on manna81.mps (LP relaxation not as tight it seems) and on neos-3354841-apure.mps.gz (too many literals created this way).

• optional int64 presolve_inclusion_work_limit = 201

  A few presolve operations involve detecting constraints included in other constraint. Since there can be a quadratic number of such pairs, and processing them usually involve scanning them, the complexity of these operations can be big. This enforce a local deterministic limit on the number of entries scanned. Default is 1e8. A value of zero will disable these presolve rules completely.

• optional bool ignore_names = 202

  If true, we don't keep names in our internal copy of the user given model.

• optional bool infer_all_diffs = 233

  Run a max-clique code amongst all the x != y we can find and try to infer set of variables that are all different. This allows to close neos16.mps for instance. Note that we only run this code if there is no all_diff already in the model so that if a user want to add some all_diff, we assume it is well done and do not try to add more. This will also detect and add no_overlap constraints, if all the relations x != y have "offsets" between them. I.e. x > y + offset.

• optional bool find_big_linear_overlap = 234

  Try to find large "rectangle" in the linear constraint matrix with identical lines. If such rectangle is big enough, we can introduce a new integer variable corresponding to the common expression and greatly reduce the number of non-zero.

• optional bool find_clauses_that_are_exactly_one = 333

  By propagating (or just using binary clauses), one can detect that all literal of a clause are actually in at most one relationship. Thus this constraint can be promoted to an exactly one constraints. This should help as it convey more structure. Note that this is expensive, so we have a deterministic limit in place.

• optional bool use_sat_inprocessing = 163

  Enable or disable "inprocessing" which is some SAT presolving done at each restart to the root level.

• optional double inprocessing_dtime_ratio = 273

  Proportion of deterministic time we should spend on inprocessing. At each "restart", if the proportion is below this ratio, we will do some inprocessing, otherwise, we skip it for this restart.

• optional double inprocessing_probing_dtime = 274

  The amount of dtime we should spend on probing for each inprocessing round.

• optional double inprocessing_minimization_dtime = 275

  Parameters for an heuristic similar to the one described in "An effective learnt clause minimization approach for CDCL Sat Solvers", https://www.ijcai.org/proceedings/2017/0098.pdf This is the amount of dtime we should spend on this technique during each inprocessing phase. The minimization technique is the same as the one used to minimize core in max-sat. We also minimize problem clauses and not just the learned clause that we keep forever like in the paper.

• optional bool inprocessing_minimization_use_conflict_analysis = 297

• optional bool inprocessing_minimization_use_all_orderings = 298

• optional bool inprocessing_use_congruence_closure = 342

  Whether we use the algorithm described in "Clausal Congruence closure", Armin Biere, Katalin Fazekas, Mathias Fleury, Nils Froleyks, 2024. Note that we only have a basic version currently.

• optional bool inprocessing_use_sat_sweeping = 354

  Whether we use the SAT sweeping algorithm described in "Clausal Equivalence Sweeping", Armin Biere, Katalin Fazekas, Mathias Fleury, Nils Froleyks, 2025.

• optional int32 num_workers = 206

  Specify the number of parallel workers (i.e. threads) to use during search. This should usually be lower than your number of available cpus + hyperthread in your machine. A value of 0 means the solver will try to use all cores on the machine. A number of 1 means no parallelism. Note that 'num_workers' is the preferred name, but if it is set to zero, we will still read the deprecated 'num_search_workers'. As of 2020-04-10, if you're using SAT via MPSolver (to solve integer programs) this field is overridden with a value of 8, if the field is not set *explicitly*. Thus, always set this field explicitly or via MPSolver::SetNumThreads().

• optional int32 num_search_workers = 100

• optional int32 num_full_subsolvers = 294

  We distinguish subsolvers that consume a full thread, and the ones that are always interleaved. If left at zero, we will fix this with a default formula that depends on num_workers. But if you start modifying what runs, you might want to fix that to a given value depending on the num_workers you use.

• repeated string subsolvers = 207

  In multi-thread, the solver can be mainly seen as a portfolio of solvers with different parameters. This field indicates the names of the parameters that are used in multithread. This only applies to "full" subsolvers. See cp_model_search.cc to see a list of the names and the default value (if left empty) that looks like: - default_lp (linearization_level:1) - fixed (only if fixed search specified or scheduling) - no_lp (linearization_level:0) - max_lp (linearization_level:2) - pseudo_costs (only if objective, change search heuristic) - reduced_costs (only if objective, change search heuristic) - quick_restart (kind of probing) - quick_restart_no_lp (kind of probing with linearization_level:0) - lb_tree_search (to improve lower bound, MIP like tree search) - probing (continuous probing and shaving) Also, note that some set of parameters will be ignored if they do not make sense. For instance if there is no objective, pseudo_cost or reduced_cost search will be ignored. Core based search will only work if the objective has many terms. If there is no fixed strategy fixed will be ignored. And so on. The order is important, as only the first num_full_subsolvers will be scheduled. You can see in the log which one are selected for a given run.

• repeated string extra_subsolvers = 219

  A convenient way to add more workers types. These will be added at the beginning of the list.

• repeated string ignore_subsolvers = 209

  Rather than fully specifying subsolvers, it is often convenient to just remove the ones that are not useful on a given problem or only keep specific ones for testing. Each string is interpreted as a "glob", so we support '*' and '?'. The way this work is that we will only accept a name that match a filter pattern (if non-empty) and do not match an ignore pattern. Note also that these fields work on LNS or LS names even if these are currently not specified via the subsolvers field.

• repeated string filter_subsolvers = 293

• repeated SatParameters subsolver_params = 210

  It is possible to specify additional subsolver configuration. These can be referred by their params.name() in the fields above. Note that only the specified field will "overwrite" the ones of the base parameter. If a subsolver_params has the name of an existing subsolver configuration, the named parameters will be merged into the subsolver configuration.

• optional bool interleave_search = 136

  Experimental. If this is true, then we interleave all our major search strategy and distribute the work amongst num_workers. The search is deterministic (independently of num_workers!), and we schedule and wait for interleave_batch_size task to be completed before synchronizing and scheduling the next batch of tasks.

• optional int32 interleave_batch_size = 134

• optional bool share_objective_bounds = 113

  Allows objective sharing between workers.

• optional bool share_level_zero_bounds = 114

  Allows sharing of the bounds of modified variables at level 0.

• optional bool share_linear2_bounds = 326

  Allows sharing of the bounds on linear2 discovered at level 0. This is mainly interesting on scheduling type of problems when we branch on precedences. Warning: This currently non-deterministic.

• optional bool share_binary_clauses = 203

  Allows sharing of new learned binary clause between workers.

• optional bool share_glue_clauses = 285

  Allows sharing of short glue clauses between workers. Implicitly disabled if share_binary_clauses is false.

• optional bool minimize_shared_clauses = 300

  Minimize and detect subsumption of shared clauses immediately after they are imported.

• optional double share_glue_clauses_dtime = 322

  The amount of dtime between each export of shared glue clauses.

• optional bool check_lrat_proof = 344

  If true, inferred clauses are checked with an LRAT checker as they are learned, in presolve (reduced to trivial simplifications if cp_model_presolve is false), and in each worker. As of December 2025, this only works with pure SAT problems, with - cp_model_presolve = false, - linearization_level <= 1, - symmetry_level <= 1.

• optional bool check_merged_lrat_proof = 352

  If true, and if output_lrat_proof is true and the problem is UNSAT, check that the merged proof file is valid, i.e., that clause sharing between workers is correct. This checks each inferred clause, so you might want to disable check_lrat_proof to avoid redundant work. As of November 2025, this only works for pure SAT problems, with num_workers = 1.

• optional bool output_lrat_proof = 345

  If true, an LRAT proof that all the clauses inferred by the solver are valid is output to several files (one for presolve -- reduced to trivial simplifications if cp_model_presolve is false, one per worker, and one for the merged proof). As of December 2025, this only works for pure SAT problems, with - cp_model_presolve = false, - linearization_level <= 1, - symmetry_level <= 1.

• optional bool check_drat_proof = 346

  If true, and if the problem is UNSAT, a DRAT proof of this UNSAT property is checked after the solver has finished. As of November 2025, this only works for pure SAT problems, with - num_workers = 1, - cp_model_presolve = false, - linearization_level <= 1, - symmetry_level <= 1.

• optional bool output_drat_proof = 347

  If true, a DRAT proof that all the clauses inferred by the solver are valid is output to a file. As of December 2025, this only works for pure SAT problems, with - num_workers = 1, - cp_model_presolve = false, - linearization_level <= 1, - symmetry_level <= 1.

• optional double max_drat_time_in_seconds = 348

  The maximum time allowed to check the DRAT proof (this can take more time than the solve itself). Only used if check_drat_proof is true.

• optional bool debug_postsolve_with_full_solver = 162

  We have two different postsolve code. The default one should be better and it allows for a more powerful presolve, but it can be useful to postsolve using the full solver instead.

• optional int32 debug_max_num_presolve_operations = 151

  If positive, try to stop just after that many presolve rules have been applied. This is mainly useful for debugging presolve.

• optional bool debug_crash_on_bad_hint = 195

  Crash if we do not manage to complete the hint into a full solution.

• optional bool debug_crash_if_presolve_breaks_hint = 306

  Crash if presolve breaks a feasible hint.

• optional bool debug_crash_if_lrat_check_fails = 339

  Crash if the LRAT UNSAT proof is invalid.

• optional bool use_optimization_hints = 35

  For an optimization problem, whether we follow some hints in order to find a better first solution. For a variable with hint, the solver will always try to follow the hint. It will revert to the variable_branching default otherwise.

• optional int32 core_minimization_level = 50

  If positive, we spend some effort on each core: - At level 1, we use a simple heuristic to try to minimize an UNSAT core. - At level 2, we use propagation to minimize the core but also identify literal in at most one relationship in this core.

• optional bool find_multiple_cores = 84

  Whether we try to find more independent cores for a given set of assumptions in the core based max-SAT algorithms.

• optional bool cover_optimization = 89

  If true, when the max-sat algo find a core, we compute the minimal number of literals in the core that needs to be true to have a feasible solution. This is also called core exhaustion in more recent max-SAT papers.

• optional SatParameters.MaxSatAssumptionOrder max_sat_assumption_order = 51

• optional bool max_sat_reverse_assumption_order = 52

  If true, adds the assumption in the reverse order of the one defined by max_sat_assumption_order.

• optional SatParameters.MaxSatStratificationAlgorithm max_sat_stratification = 53

• optional double propagation_loop_detection_factor = 221

  Some search decisions might cause a really large number of propagations to happen when integer variables with large domains are only reduced by 1 at each step. If we propagate more than the number of variable times this parameters we try to take counter-measure. Setting this to 0.0 disable this feature. TODO(user): Setting this to something like 10 helps in most cases, but the code is currently buggy and can cause the solve to enter a bad state where no progress is made.

• optional bool use_precedences_in_disjunctive_constraint = 74

  When this is true, then a disjunctive constraint will try to use the precedence relations between time intervals to propagate their bounds further. For instance if task A and B are both before C and task A and B are in disjunction, then we can deduce that task C must start after duration(A) + duration(B) instead of simply max(duration(A), duration(B)), provided that the start time for all task was currently zero. This always result in better propagation, but it is usually slow, so depending on the problem, turning this off may lead to a faster solution.

• optional int32 transitive_precedences_work_limit = 327

  At root level, we might compute the transitive closure of "precedences" relations so that we can exploit that in scheduling problems. Setting this to zero disable the feature.

• optional int32 max_size_to_create_precedence_literals_in_disjunctive = 229

  Create one literal for each disjunction of two pairs of tasks. This slows down the solve time, but improves the lower bound of the objective in the makespan case. This will be triggered if the number of intervals is less or equal than the parameter and if use_strong_propagation_in_disjunctive is true.

• optional bool use_strong_propagation_in_disjunctive = 230

  Enable stronger and more expensive propagation on no_overlap constraint.

• optional bool use_dynamic_precedence_in_disjunctive = 263

  Whether we try to branch on decision "interval A before interval B" rather than on intervals bounds. This usually works better, but slow down a bit the time to find the first solution. These parameters are still EXPERIMENTAL, the result should be correct, but it some corner cases, they can cause some failing CHECK in the solver.

• optional bool use_dynamic_precedence_in_cumulative = 268

• optional bool use_overload_checker_in_cumulative = 78

  When this is true, the cumulative constraint is reinforced with overload checking, i.e., an additional level of reasoning based on energy. This additional level supplements the default level of reasoning as well as timetable edge finding. This always result in better propagation, but it is usually slow, so depending on the problem, turning this off may lead to a faster solution.

• optional bool use_conservative_scale_overload_checker = 286

  Enable a heuristic to solve cumulative constraints using a modified energy constraint. We modify the usual energy definition by applying a super-additive function (also called "conservative scale" or "dual-feasible function") to the demand and the durations of the tasks. This heuristic is fast but for most problems it does not help much to find a solution.

• optional bool use_timetable_edge_finding_in_cumulative = 79

  When this is true, the cumulative constraint is reinforced with timetable edge finding, i.e., an additional level of reasoning based on the conjunction of energy and mandatory parts. This additional level supplements the default level of reasoning as well as overload_checker. This always result in better propagation, but it is usually slow, so depending on the problem, turning this off may lead to a faster solution.

• optional int32 max_num_intervals_for_timetable_edge_finding = 260

  Max number of intervals for the timetable_edge_finding algorithm to propagate. A value of 0 disables the constraint.

• optional bool use_hard_precedences_in_cumulative = 215

  If true, detect and create constraint for integer variable that are "after" a set of intervals in the same cumulative constraint. Experimental: by default we just use "direct" precedences. If exploit_all_precedences is true, we explore the full precedence graph. This assumes we have a DAG otherwise it fails.

• optional bool exploit_all_precedences = 220

• optional bool use_disjunctive_constraint_in_cumulative = 80

  When this is true, the cumulative constraint is reinforced with propagators from the disjunctive constraint to improve the inference on a set of tasks that are disjunctive at the root of the problem. This additional level supplements the default level of reasoning. Propagators of the cumulative constraint will not be used at all if all the tasks are disjunctive at root node. This always result in better propagation, but it is usually slow, so depending on the problem, turning this off may lead to a faster solution.

• optional int32 no_overlap_2d_boolean_relations_limit = 321

  If less than this number of boxes are present in a no-overlap 2d, we create 4 Booleans per pair of boxes: - Box 2 is after Box 1 on x. - Box 1 is after Box 2 on x. - Box 2 is after Box 1 on y. - Box 1 is after Box 2 on y. Note that at least one of them must be true, and at most one on x and one on y can be true. This can significantly help in closing small problem. The SAT reasoning can be a lot more powerful when we take decision on such positional relations.

• optional bool use_timetabling_in_no_overlap_2d = 200

  When this is true, the no_overlap_2d constraint is reinforced with propagators from the cumulative constraints. It consists of ignoring the position of rectangles in one position and projecting the no_overlap_2d on the other dimension to create a cumulative constraint. This is done on both axis. This additional level supplements the default level of reasoning.

• optional bool use_energetic_reasoning_in_no_overlap_2d = 213

  When this is true, the no_overlap_2d constraint is reinforced with energetic reasoning. This additional level supplements the default level of reasoning.

• optional bool use_area_energetic_reasoning_in_no_overlap_2d = 271

  When this is true, the no_overlap_2d constraint is reinforced with an energetic reasoning that uses an area-based energy. This can be combined with the two other overlap heuristics above.

• optional bool use_try_edge_reasoning_in_no_overlap_2d = 299

• optional int32 max_pairs_pairwise_reasoning_in_no_overlap_2d = 276

  If the number of pairs to look is below this threshold, do an extra step of propagation in the no_overlap_2d constraint by looking at all pairs of intervals.

• optional int32 maximum_regions_to_split_in_disconnected_no_overlap_2d = 315

  Detects when the space where items of a no_overlap_2d constraint can placed is disjoint (ie., fixed boxes split the domain). When it is the case, we can introduce a boolean for each pair <item, component> encoding whether the item is in the component or not. Then we replace the original no_overlap_2d constraint by one no_overlap_2d constraint for each component, with the new booleans as the enforcement_literal of the intervals. This is equivalent to expanding the original no_overlap_2d constraint into a bin packing problem with each connected component being a bin. This heuristic is only done when the number of regions to split is less than this parameter and <= 1 disables it.

• optional bool use_linear3_for_no_overlap_2d_precedences = 323

  When set, this activates a propagator for the no_overlap_2d constraint that uses any eventual linear constraints of the model in the form `{start interval 1} - {end interval 2} + c*w <= ub` to detect that two intervals must overlap in one dimension for some values of `w`. This is particularly useful for problems where the distance between two boxes is part of the model.

• optional bool use_dual_scheduling_heuristics = 214

  When set, it activates a few scheduling parameters to improve the lower bound of scheduling problems. This is only effective with multiple workers as it modifies the reduced_cost, lb_tree_search, and probing workers.

• optional bool use_all_different_for_circuit = 311

  Turn on extra propagation for the circuit constraint. This can be quite slow.

• optional int32 routing_cut_subset_size_for_binary_relation_bound = 312

  If the size of a subset of nodes of a RoutesConstraint is less than this value, use linear constraints of size 1 and 2 (such as capacity and time window constraints) enforced by the arc literals to compute cuts for this subset (unless the subset size is less than routing_cut_subset_size_for_tight_binary_relation_bound, in which case the corresponding algorithm is used instead). The algorithm for these cuts has a O(n^3) complexity, where n is the subset size. Hence the value of this parameter should not be too large (e.g. 10 or 20).

• optional int32 routing_cut_subset_size_for_tight_binary_relation_bound = 313

  Similar to above, but with a different algorithm producing better cuts, at the price of a higher O(2^n) complexity, where n is the subset size. Hence the value of this parameter should be small (e.g. less than 10).

• optional int32 routing_cut_subset_size_for_exact_binary_relation_bound = 316

  Similar to above, but with an even stronger algorithm in O(n!). We try to be defensive and abort early or not run that often. Still the value of that parameter shouldn't really be much more than 10.

• optional int32 routing_cut_subset_size_for_shortest_paths_bound = 318

  Similar to routing_cut_subset_size_for_exact_binary_relation_bound but use a bound based on shortest path distances (which respect triangular inequality). This allows to derive bounds that are valid for any superset of a given subset. This is slow, so it shouldn't really be larger than 10.

• optional double routing_cut_dp_effort = 314

  The amount of "effort" to spend in dynamic programming for computing routing cuts. This is in term of basic operations needed by the algorithm in the worst case, so a value like 1e8 should take less than a second to compute.

• optional int32 routing_cut_max_infeasible_path_length = 317

  If the length of an infeasible path is less than this value, a cut will be added to exclude it.

• optional SatParameters.SearchBranching search_branching = 82

• optional int32 hint_conflict_limit = 153

  Conflict limit used in the phase that exploit the solution hint.

• optional bool repair_hint = 167

  If true, the solver tries to repair the solution given in the hint. This search terminates after the 'hint_conflict_limit' is reached and the solver switches to regular search. If false, then we do a FIXED_SEARCH using the hint until the hint_conflict_limit is reached.

• optional bool fix_variables_to_their_hinted_value = 192

  If true, variables appearing in the solution hints will be fixed to their hinted value.

• optional bool use_probing_search = 176

  If true, search will continuously probe Boolean variables, and integer variable bounds. This parameter is set to true in parallel on the probing worker.

• optional bool use_extended_probing = 269

  Use extended probing (probe bool_or, at_most_one, exactly_one).

• optional int32 probing_num_combinations_limit = 272

  How many combinations of pairs or triplets of variables we want to scan.

• optional double shaving_deterministic_time_in_probing_search = 204

  Add a shaving phase (where the solver tries to prove that the lower or upper bound of a variable are infeasible) to the probing search. (<= 0 disables it).

• optional double shaving_search_deterministic_time = 205

  Specifies the amount of deterministic time spent of each try at shaving a bound in the shaving search.

• optional int64 shaving_search_threshold = 290

  Specifies the threshold between two modes in the shaving procedure. If the range of the variable/objective is less than this threshold, then the shaving procedure will try to remove values one by one. Otherwise, it will try to remove one range at a time.

• optional bool use_objective_lb_search = 228

  If true, search will search in ascending max objective value (when minimizing) starting from the lower bound of the objective.

• optional bool use_objective_shaving_search = 253

  This search differs from the previous search as it will not use assumptions to bound the objective, and it will recreate a full model with the hardcoded objective value.

• optional int32 variables_shaving_level = 289

  This search takes all Boolean or integer variables, and maximize or minimize them in order to reduce their domain. -1 is automatic, otherwise value 0 disables it, and 1, 2, or 3 changes something.

• optional int64 pseudo_cost_reliability_threshold = 123

  The solver ignores the pseudo costs of variables with number of recordings less than this threshold.

• optional bool optimize_with_core = 83

  The default optimization method is a simple "linear scan", each time trying to find a better solution than the previous one. If this is true, then we use a core-based approach (like in max-SAT) when we try to increase the lower bound instead.

• optional bool optimize_with_lb_tree_search = 188

  Do a more conventional tree search (by opposition to SAT based one) where we keep all the explored node in a tree. This is meant to be used in a portfolio and focus on improving the objective lower bound. Keeping the whole tree allow us to report a better objective lower bound coming from the worst open node in the tree.

• optional bool save_lp_basis_in_lb_tree_search = 284

  Experimental. Save the current LP basis at each node of the search tree so that when we jump around, we can load it and reduce the number of LP iterations needed. It currently works okay if we do not change the lp with cuts or simplification... More work is needed to make it robust in all cases.

• optional int32 binary_search_num_conflicts = 99

  If non-negative, perform a binary search on the objective variable in order to find an [min, max] interval outside of which the solver proved unsat/sat under this amount of conflict. This can quickly reduce the objective domain on some problems.

• optional bool optimize_with_max_hs = 85

  This has no effect if optimize_with_core is false. If true, use a different core-based algorithm similar to the max-HS algo for max-SAT. This is a hybrid MIP/CP approach and it uses a MIP solver in addition to the CP/SAT one. This is also related to the PhD work of tobyodavies@ "Automatic Logic-Based Benders Decomposition with MiniZinc" http://aaai.org/ocs/index.php/AAAI/AAAI17/paper/view/14489

• optional bool use_feasibility_jump = 265

  Parameters for an heuristic similar to the one described in the paper: "Feasibility Jump: an LP-free Lagrangian MIP heuristic", Bjørnar Luteberget, Giorgio Sartor, 2023, Mathematical Programming Computation.

• optional bool use_ls_only = 240

  Disable every other type of subsolver, setting this turns CP-SAT into a pure local-search solver.

• optional double feasibility_jump_decay = 242

  On each restart, we randomly choose if we use decay (with this parameter) or no decay.

• optional int32 feasibility_jump_linearization_level = 257

  How much do we linearize the problem in the local search code.

• optional int32 feasibility_jump_restart_factor = 258

  This is a factor that directly influence the work before each restart. Increasing it leads to longer restart.

• optional double feasibility_jump_batch_dtime = 292

  How much dtime for each LS batch.

• optional double feasibility_jump_var_randomization_probability = 247

  Probability for a variable to have a non default value upon restarts or perturbations.

• optional double feasibility_jump_var_perburbation_range_ratio = 248

  Max distance between the default value and the pertubated value relative to the range of the domain of the variable.

• optional bool feasibility_jump_enable_restarts = 250

  When stagnating, feasibility jump will either restart from a default solution (with some possible randomization), or randomly pertubate the current solution. This parameter selects the first option.

• optional int32 feasibility_jump_max_expanded_constraint_size = 264

  Maximum size of no_overlap or no_overlap_2d constraint for a quadratic expansion. This might look a lot, but by expanding such constraint, we get a linear time evaluation per single variable moves instead of a slow O(n log n) one.

• optional int32 num_violation_ls = 244

  This will create incomplete subsolvers (that are not LNS subsolvers) that use the feasibility jump code to find improving solution, treating the objective improvement as a hard constraint.

• optional int32 violation_ls_perturbation_period = 249

  How long violation_ls should wait before perturbating a solution.

• optional double violation_ls_compound_move_probability = 259

  Probability of using compound move search each restart. TODO(user): Add reference to paper when published.

• optional int32 shared_tree_num_workers = 235

  Enables shared tree search. If positive, start this many complete worker threads to explore a shared search tree. These workers communicate objective bounds and simple decision nogoods relating to the shared prefix of the tree, and will avoid exploring the same subtrees as one another. Specifying a negative number uses a heuristic to select an appropriate number of shared tree workeres based on the total number of workers.

• optional bool use_shared_tree_search = 236

  Set on shared subtree workers. Users should not set this directly.

• optional int32 shared_tree_worker_min_restarts_per_subtree = 282

  Minimum restarts before a worker will replace a subtree that looks "bad" based on the average LBD of learned clauses.

• optional bool shared_tree_worker_enable_trail_sharing = 295

  If true, workers share more of the information from their local trail. Specifically, literals implied by the shared tree decisions.

• optional bool shared_tree_worker_enable_phase_sharing = 304

  If true, shared tree workers share their target phase when returning an assigned subtree for the next worker to use.

• optional double shared_tree_open_leaves_per_worker = 281

  How many open leaf nodes should the shared tree maintain per worker.

• optional int32 shared_tree_max_nodes_per_worker = 238

  In order to limit total shared memory and communication overhead, limit the total number of nodes that may be generated in the shared tree. If the shared tree runs out of unassigned leaves, workers act as portfolio workers. Note: this limit includes interior nodes, not just leaves.

• optional SatParameters.SharedTreeSplitStrategy shared_tree_split_strategy = 239

• optional int32 shared_tree_balance_tolerance = 305

  How much deeper compared to the ideal max depth of the tree is considered "balanced" enough to still accept a split. Without such a tolerance, sometimes the tree can only be split by a single worker, and they may not generate a split for some time. In contrast, with a tolerance of 1, at least half of all workers should be able to split the tree as soon as a split becomes required. This only has an effect on SPLIT_STRATEGY_BALANCED_TREE and SPLIT_STRATEGY_DISCREPANCY.

• optional double shared_tree_split_min_dtime = 328

  How much dtime a worker will wait between proposing splits. This limits the contention in splitting the shared tree, and also reduces the number of too-easy subtrees that are generates.

• optional bool enumerate_all_solutions = 87

  Whether we enumerate all solutions of a problem without objective. WARNING: - This can be used with num_workers > 1 but then each solutions can be found more than once, so it is up to the client to deduplicate them. - If keep_all_feasible_solutions_in_presolve is unset, we will set it to true as otherwise, many feasible solution can just be removed by the presolve. It is still possible to manually set this to false if one only wants to enumerate all solutions of the presolved model.

• optional bool keep_all_feasible_solutions_in_presolve = 173

  If true, we disable the presolve reductions that remove feasible solutions from the search space. Such solution are usually dominated by a "better" solution that is kept, but depending on the situation, we might want to keep all solutions. A trivial example is when a variable is unused. If this is true, then the presolve will not fix it to an arbitrary value and it will stay in the search space.

• optional bool fill_tightened_domains_in_response = 132

  If true, add information about the derived variable domains to the CpSolverResponse. It is an option because it makes the response slighly bigger and there is a bit more work involved during the postsolve to construct it, but it should still have a low overhead. See the tightened_variables field in CpSolverResponse for more details.

• optional bool fill_additional_solutions_in_response = 194

  If true, the final response addition_solutions field will be filled with all solutions from our solutions pool. Note that if both this field and enumerate_all_solutions is true, we will copy to the pool all of the solution found. So if solution_pool_size is big enough, you can get all solutions this way instead of using the solution callback. Note that this only affect the "final" solution, not the one passed to the solution callbacks.

• optional bool instantiate_all_variables = 106

  If true, the solver will add a default integer branching strategy to the already defined search strategy. If not, some variable might still not be fixed at the end of the search. For now we assume these variable can just be set to their lower bound.

• optional bool auto_detect_greater_than_at_least_one_of = 95

  If true, then the precedences propagator try to detect for each variable if it has a set of "optional incoming arc" for which at least one of them is present. This is usually useful to have but can be slow on model with a lot of precedence.

• optional bool stop_after_first_solution = 98

  For an optimization problem, stop the solver as soon as we have a solution.

• optional bool stop_after_presolve = 149

  Mainly used when improving the presolver. When true, stops the solver after the presolve is complete (or after loading and root level propagation).

• optional bool stop_after_root_propagation = 252

• optional double lns_initial_difficulty = 307

  Initial parameters for neighborhood generation.

• optional double lns_initial_deterministic_limit = 308

• optional bool use_lns = 283

  Testing parameters used to disable all lns workers.

• optional bool use_lns_only = 101

  Experimental parameters to disable everything but lns.

• optional int32 solution_pool_size = 193

  Size of the top-n different solutions kept by the solver. This parameter must be > 0. Currently, having this larger than one mainly impact the "base" solution chosen for a LNS/LS fragment.

• optional int32 solution_pool_diversity_limit = 329

  If solution_pool_size is <= this, we will use DP to keep a "diverse" set of solutions (the one further apart via hamming distance) in the pool. Setting this to large value might be slow, especially if your solution are large.

• optional int32 alternative_pool_size = 325

  In order to not get stuck in local optima, when this is non-zero, we try to also work on "older" solutions with a worse objective value so we get a chance to follow a different LS/LNS trajectory.

• optional bool use_rins_lns = 129

  Turns on relaxation induced neighborhood generator.

• optional bool use_feasibility_pump = 164

  Adds a feasibility pump subsolver along with lns subsolvers.

• optional bool use_lb_relax_lns = 255

  Turns on neighborhood generator based on local branching LP. Based on Huang et al., "Local Branching Relaxation Heuristics for Integer Linear Programs", 2023.

• optional int32 lb_relax_num_workers_threshold = 296

  Only use lb-relax if we have at least that many workers.

• optional SatParameters.FPRoundingMethod fp_rounding = 165

• optional bool diversify_lns_params = 137

  If true, registers more lns subsolvers with different parameters.

• optional bool randomize_search = 103

  Randomize fixed search.

• optional int64 search_random_variable_pool_size = 104

  Search randomization will collect the top 'search_random_variable_pool_size' valued variables, and pick one randomly. The value of the variable is specific to each strategy.

• optional bool push_all_tasks_toward_start = 262

  Experimental code: specify if the objective pushes all tasks toward the start of the schedule.

• optional bool use_optional_variables = 108

  If true, we automatically detect variables whose constraint are always enforced by the same literal and we mark them as optional. This allows to propagate them as if they were present in some situation. TODO(user): This is experimental and seems to lead to wrong optimal in some situation. It should however gives correct solutions. Fix.

• optional bool use_exact_lp_reason = 109

  The solver usually exploit the LP relaxation of a model. If this option is true, then whatever is infered by the LP will be used like an heuristic to compute EXACT propagation on the IP. So with this option, there is no numerical imprecision issues.

• optional bool use_combined_no_overlap = 133

  This can be beneficial if there is a lot of no-overlap constraints but a relatively low number of different intervals in the problem. Like 1000 intervals, but 1M intervals in the no-overlap constraints covering them.

• optional int32 at_most_one_max_expansion_size = 270

  All at_most_one constraints with a size <= param will be replaced by a quadratic number of binary implications.

• optional bool catch_sigint_signal = 135

  Indicates if the CP-SAT layer should catch Control-C (SIGINT) signals when calling solve. If set, catching the SIGINT signal will terminate the search gracefully, as if a time limit was reached.

• optional bool use_implied_bounds = 144

  Stores and exploits "implied-bounds" in the solver. That is, relations of the form literal => (var >= bound). This is currently used to derive stronger cuts.

• optional bool polish_lp_solution = 175

  Whether we try to do a few degenerate iteration at the end of an LP solve to minimize the fractionality of the integer variable in the basis. This helps on some problems, but not so much on others. It also cost of bit of time to do such polish step.

• optional double lp_primal_tolerance = 266

  The internal LP tolerances used by CP-SAT. These applies to the internal and scaled problem. If the domains of your variables are large it might be good to use lower tolerances. If your problem is binary with low coefficients, it might be good to use higher ones to speed-up the lp solves.

• optional double lp_dual_tolerance = 267

• optional bool convert_intervals = 177

  Temporary flag util the feature is more mature. This convert intervals to the newer proto format that support affine start/var/end instead of just variables.

• optional int32 symmetry_level = 183

  Whether we try to automatically detect the symmetries in a model and exploit them. Currently, at level 1 we detect them in presolve and try to fix Booleans. At level 2, we also do some form of dynamic symmetry breaking during search. At level 3, we also detect symmetries for very large models, which can be slow. At level 4, we try to break as much symmetry as possible in presolve.

• optional bool use_symmetry_in_lp = 301

  When we have symmetry, it is possible to "fold" all variables from the same orbit into a single variable, while having the same power of LP relaxation. This can help significantly on symmetric problem. However there is currently a bit of overhead as the rest of the solver need to do some translation between the folded LP and the rest of the problem.

• optional bool keep_symmetry_in_presolve = 303

  Experimental. This will compute the symmetry of the problem once and for all. All presolve operations we do should keep the symmetry group intact or modify it properly. For now we have really little support for this. We will disable a bunch of presolve operations that could be supported.

• optional double symmetry_detection_deterministic_time_limit = 302

  Deterministic time limit for symmetry detection.

• optional bool new_linear_propagation = 224

  The new linear propagation code treat all constraints at once and use an adaptation of Bellman-Ford-Tarjan to propagate constraint in a smarter order and potentially detect propagation cycle earlier.

• optional int32 linear_split_size = 256

  Linear constraints that are not pseudo-Boolean and that are longer than this size will be split into sqrt(size) intermediate sums in order to have faster propation in the CP engine.

• optional int32 linearization_level = 90

  A non-negative level indicating the type of constraints we consider in the LP relaxation. At level zero, no LP relaxation is used. At level 1, only the linear constraint and full encoding are added. At level 2, we also add all the Boolean constraints.

• optional int32 boolean_encoding_level = 107

  A non-negative level indicating how much we should try to fully encode Integer variables as Boolean.

• optional int32 max_domain_size_when_encoding_eq_neq_constraints = 191

  When loading a*x + b*y ==/!= c when x and y are both fully encoded. The solver may decide to replace the linear equation by a set of clauses. This is triggered if the sizes of the domains of x and y are below the threshold.

• optional int32 max_num_cuts = 91

  The limit on the number of cuts in our cut pool. When this is reached we do not generate cuts anymore. TODO(user): We should probably remove this parameters, and just always generate cuts but only keep the best n or something.

• optional int32 cut_level = 196

  Control the global cut effort. Zero will turn off all cut. For now we just have one level. Note also that most cuts are only used at linearization level >= 2.

• optional bool only_add_cuts_at_level_zero = 92

  For the cut that can be generated at any level, this control if we only try to generate them at the root node.

• optional bool add_objective_cut = 197

  When the LP objective is fractional, do we add the cut that forces the linear objective expression to be greater or equal to this fractional value rounded up? We can always do that since our objective is integer, and combined with MIR heuristic to reduce the coefficient of such cut, it can help.

• optional bool add_cg_cuts = 117

  Whether we generate and add Chvatal-Gomory cuts to the LP at root node. Note that for now, this is not heavily tuned.

• optional bool add_mir_cuts = 120

  Whether we generate MIR cuts at root node. Note that for now, this is not heavily tuned.

• optional bool add_zero_half_cuts = 169

  Whether we generate Zero-Half cuts at root node. Note that for now, this is not heavily tuned.

• optional bool add_clique_cuts = 172

  Whether we generate clique cuts from the binary implication graph. Note that as the search goes on, this graph will contains new binary clauses learned by the SAT engine.

• optional bool add_rlt_cuts = 279

  Whether we generate RLT cuts. This is still experimental but can help on binary problem with a lot of clauses of size 3.

• optional int32 max_all_diff_cut_size = 148

  Cut generator for all diffs can add too many cuts for large all_diff constraints. This parameter restricts the large all_diff constraints to have a cut generator.

• optional bool add_lin_max_cuts = 152

  For the lin max constraints, generates the cuts described in "Strong mixed-integer programming formulations for trained neural networks" by Ross Anderson et. (https://arxiv.org/pdf/1811.01988.pdf)

• optional int32 max_integer_rounding_scaling = 119

  In the integer rounding procedure used for MIR and Gomory cut, the maximum "scaling" we use (must be positive). The lower this is, the lower the integer coefficients of the cut will be. Note that cut generated by lower values are not necessarily worse than cut generated by larger value. There is no strict dominance relationship. Setting this to 2 result in the "strong fractional rouding" of Letchford and Lodi.

• optional bool add_lp_constraints_lazily = 112

  If true, we start by an empty LP, and only add constraints not satisfied by the current LP solution batch by batch. A constraint that is only added like this is known as a "lazy" constraint in the literature, except that we currently consider all constraints as lazy here.

• optional int32 root_lp_iterations = 227

  Even at the root node, we do not want to spend too much time on the LP if it is "difficult". So we solve it in "chunks" of that many iterations. The solve will be continued down in the tree or the next time we go back to the root node.

• optional double min_orthogonality_for_lp_constraints = 115

  While adding constraints, skip the constraints which have orthogonality less than 'min_orthogonality_for_lp_constraints' with already added constraints during current call. Orthogonality is defined as 1 - cosine(vector angle between constraints). A value of zero disable this feature.

• optional int32 max_cut_rounds_at_level_zero = 154

  Max number of time we perform cut generation and resolve the LP at level 0.

• optional int32 max_consecutive_inactive_count = 121

  If a constraint/cut in LP is not active for that many consecutive OPTIMAL solves, remove it from the LP. Note that it might be added again later if it become violated by the current LP solution.

• optional double cut_max_active_count_value = 155

  These parameters are similar to sat clause management activity parameters. They are effective only if the number of generated cuts exceed the storage limit. Default values are based on a few experiments on miplib instances.

• optional double cut_active_count_decay = 156

• optional int32 cut_cleanup_target = 157

  Target number of constraints to remove during cleanup.

• optional int32 new_constraints_batch_size = 122

  Add that many lazy constraints (or cuts) at once in the LP. Note that at the beginning of the solve, we do add more than this.

• optional bool exploit_integer_lp_solution = 94

  If true and the Lp relaxation of the problem has an integer optimal solution, try to exploit it. Note that since the LP relaxation may not contain all the constraints, such a solution is not necessarily a solution of the full problem.

• optional bool exploit_all_lp_solution = 116

  If true and the Lp relaxation of the problem has a solution, try to exploit it. This is same as above except in this case the lp solution might not be an integer solution.

• optional bool exploit_best_solution = 130

  When branching on a variable, follow the last best solution value.

• optional bool exploit_relaxation_solution = 161

  When branching on a variable, follow the last best relaxation solution value. We use the relaxation with the tightest bound on the objective as the best relaxation solution.

• optional bool exploit_objective = 131

  When branching an a variable that directly affect the objective, branch on the value that lead to the best objective first.

• optional bool detect_linearized_product = 277

  Infer products of Boolean or of Boolean time IntegerVariable from the linear constrainst in the problem. This can be used in some cuts, altough for now we don't really exploit it.

• optional bool use_new_integer_conflict_resolution = 336

  This should be better on integer problems. But it is still work in progress.

• optional bool create_1uip_boolean_during_icr = 341

  If true, and during integer conflict resolution (icr) the 1-UIP is an integer literal for which we do not have an associated Boolean. Create one.

• optional double mip_max_bound = 124

  We need to bound the maximum magnitude of the variables for CP-SAT, and that is the bound we use. If the MIP model expect larger variable value in the solution, then the converted model will likely not be relevant.

• optional double mip_var_scaling = 125

  All continuous variable of the problem will be multiplied by this factor. By default, we don't do any variable scaling and rely on the MIP model to specify continuous variable domain with the wanted precision.

• optional bool mip_scale_large_domain = 225

  If this is false, then mip_var_scaling is only applied to variables with "small" domain. If it is true, we scale all floating point variable independenlty of their domain.

• optional bool mip_automatically_scale_variables = 166

  If true, some continuous variable might be automatically scaled. For now, this is only the case where we detect that a variable is actually an integer multiple of a constant. For instance, variables of the form k * 0.5 are quite frequent, and if we detect this, we will scale such variable domain by 2 to make it implied integer.

• optional bool only_solve_ip = 222

  If one try to solve a MIP model with CP-SAT, because we assume all variable to be integer after scaling, we will not necessarily have the correct optimal. Note however that all feasible solutions are valid since we will just solve a more restricted version of the original problem. This parameters is here to prevent user to think the solution is optimal when it might not be. One will need to manually set this to false to solve a MIP model where the optimal might be different. Note that this is tested after some MIP presolve steps, so even if not all original variable are integer, we might end up with a pure IP after presolve and after implied integer detection.

• optional double mip_wanted_precision = 126

  When scaling constraint with double coefficients to integer coefficients, we will multiply by a power of 2 and round the coefficients. We will choose the lowest power such that we have no potential overflow (see mip_max_activity_exponent) and the worst case constraint activity error does not exceed this threshold. Note that we also detect constraint with rational coefficients and scale them accordingly when it seems better instead of using a power of 2. We also relax all constraint bounds by this absolute value. For pure integer constraint, if this value if lower than one, this will not change anything. However it is needed when scaling MIP problems. If we manage to scale a constraint correctly, the maximum error we can make will be twice this value (once for the scaling error and once for the relaxed bounds). If we are not able to scale that well, we will display that fact but still scale as best as we can.

• optional int32 mip_max_activity_exponent = 127

  To avoid integer overflow, we always force the maximum possible constraint activity (and objective value) according to the initial variable domain to be smaller than 2 to this given power. Because of this, we cannot always reach the "mip_wanted_precision" parameter above. This can go as high as 62, but some internal algo currently abort early if they might run into integer overflow, so it is better to keep it a bit lower than this.

• optional double mip_check_precision = 128

  As explained in mip_precision and mip_max_activity_exponent, we cannot always reach the wanted precision during scaling. We use this threshold to enphasize in the logs when the precision seems bad.

• optional bool mip_compute_true_objective_bound = 198

  Even if we make big error when scaling the objective, we can always derive a correct lower bound on the original objective by using the exact lower bound on the scaled integer version of the objective. This should be fast, but if you don't care about having a precise lower bound, you can turn it off.

• optional double mip_max_valid_magnitude = 199

  Any finite values in the input MIP must be below this threshold, otherwise the model will be reported invalid. This is needed to avoid floating point overflow when evaluating bounds * coeff for instance. We are a bit more defensive, but in practice, users shouldn't use super large values in a MIP.

• optional bool mip_treat_high_magnitude_bounds_as_infinity = 278

  By default, any variable/constraint bound with a finite value and a magnitude greater than the mip_max_valid_magnitude will result with a invalid model. This flags change the behavior such that such bounds are silently transformed to +∞ or -∞. It is recommended to keep it at false, and create valid bounds.

• optional double mip_drop_tolerance = 232

  Any value in the input mip with a magnitude lower than this will be set to zero. This is to avoid some issue in LP presolving.

• optional int32 mip_presolve_level = 261

  When solving a MIP, we do some basic floating point presolving before scaling the problem to integer to be handled by CP-SAT. This control how much of that presolve we do. It can help to better scale floating point model, but it is not always behaving nicely.

Whether to expoit the binary clause to minimize learned clauses further.

Used in: SatParameters

• NO_BINARY_MINIMIZATION = 0

• BINARY_MINIMIZATION_FROM_UIP = 1

• BINARY_MINIMIZATION_FROM_UIP_AND_DECISIONS = 5

The clauses that will be kept during a cleanup are the ones that come first under this order. We always keep or exclude ties together.

Used in: SatParameters

• CLAUSE_ACTIVITY = 0

  Order clause by decreasing activity, then by increasing LBD.

• CLAUSE_LBD = 1

  Order clause by increasing LBD, then by decreasing activity.

Do we try to minimize conflicts (greedily) when creating them.

Used in: SatParameters

• NONE = 0

• SIMPLE = 1

• RECURSIVE = 2

Rounding method to use for feasibility pump.

Used in: SatParameters

• NEAREST_INTEGER = 0

  Rounds to the nearest integer value.

• LOCK_BASED = 1

  Counts the number of linear constraints restricting the variable in the increasing values (up locks) and decreasing values (down locks). Rounds the variable in the direction of lesser locks.

• ACTIVE_LOCK_BASED = 3

  Similar to lock based rounding except this only considers locks of active constraints from the last lp solve.

• PROPAGATION_ASSISTED = 2

  This is expensive rounding algorithm. We round variables one by one and propagate the bounds in between. If none of the rounded values fall in the continuous domain specified by lower and upper bound, we use the current lower/upper bound (whichever one is closest) instead of rounding the fractional lp solution value. If both the rounded values are in the domain, we round to nearest integer.

In what order do we add the assumptions in a core-based max-sat algorithm

Used in: SatParameters

• DEFAULT_ASSUMPTION_ORDER = 0

• ORDER_ASSUMPTION_BY_DEPTH = 1

• ORDER_ASSUMPTION_BY_WEIGHT = 2

What stratification algorithm we use in the presence of weight.

Used in: SatParameters

• STRATIFICATION_NONE = 0

  No stratification of the problem.

• STRATIFICATION_DESCENT = 1

  Start with literals with the highest weight, and when SAT, add the literals with the next highest weight and so on.

• STRATIFICATION_ASCENT = 2

  Start with all literals. Each time a core is found with a given minimum weight, do not consider literals with a lower weight for the next core computation. If the subproblem is SAT, do like in STRATIFICATION_DESCENT and just add the literals with the next highest weight.

Specifies the initial polarity (true/false) when the solver branches on a variable. This can be modified later by the user, or the phase saving heuristic. Note(user): POLARITY_FALSE is usually a good choice because of the "natural" way to express a linear boolean problem.

Used in: SatParameters

• POLARITY_TRUE = 0

• POLARITY_FALSE = 1

• POLARITY_RANDOM = 2

Restart algorithms. A reference for the more advanced ones is: Gilles Audemard, Laurent Simon, "Refining Restarts Strategies for SAT and UNSAT", Principles and Practice of Constraint Programming Lecture Notes in Computer Science 2012, pp 118-126

Used in: SatParameters

• NO_RESTART = 0

• LUBY_RESTART = 1

  Just follow a Luby sequence times restart_period.

• DL_MOVING_AVERAGE_RESTART = 2

  Moving average restart based on the decision level of conflicts.

• LBD_MOVING_AVERAGE_RESTART = 3

  Moving average restart based on the LBD of conflicts.

• FIXED_RESTART = 4

  Fixed period restart every restart period.

The search branching will be used to decide how to branch on unfixed nodes.

Used in: SatParameters

• AUTOMATIC_SEARCH = 0

  Try to fix all literals using the underlying SAT solver's heuristics, then generate and fix literals until integer variables are fixed. New literals on integer variables are generated using the fixed search specified by the user or our default one.

• FIXED_SEARCH = 1

  If used then all decisions taken by the solver are made using a fixed order as specified in the API or in the CpModelProto search_strategy field.

• PORTFOLIO_SEARCH = 2

  Simple portfolio search used by LNS workers.

• LP_SEARCH = 3

  If used, the solver will use heuristics from the LP relaxation. This exploit the reduced costs of the variables in the relaxation.

• PSEUDO_COST_SEARCH = 4

  If used, the solver uses the pseudo costs for branching. Pseudo costs are computed using the historical change in objective bounds when some decision are taken. Note that this works whether we use an LP or not.

• PORTFOLIO_WITH_QUICK_RESTART_SEARCH = 5

  Mainly exposed here for testing. This quickly tries a lot of randomized heuristics with a low conflict limit. It usually provides a good first solution.

• HINT_SEARCH = 6

  Mainly used internally. This is like FIXED_SEARCH, except we follow the solution_hint field of the CpModelProto rather than using the information provided in the search_strategy.

• PARTIAL_FIXED_SEARCH = 7

  Similar to FIXED_SEARCH, but differ in how the variable not listed into the fixed search heuristics are branched on. This will always start the search tree according to the specified fixed search strategy, but will complete it using the default automatic search.

• RANDOMIZED_SEARCH = 8

  Randomized search. Used to increase entropy in the search.

Used in: SatParameters

• SPLIT_STRATEGY_AUTO = 0

  Uses the default strategy, currently equivalent to SPLIT_STRATEGY_DISCREPANCY.

• SPLIT_STRATEGY_DISCREPANCY = 1

  Only accept splits if the node to be split's depth+discrepancy is minimal for the desired number of leaves. The preferred child for discrepancy calculation is the one with the lowest objective lower bound or the original branch direction if the bounds are equal. This rule allows twice as many workers to work in the preferred subtree as non-preferred.

• SPLIT_STRATEGY_OBJECTIVE_LB = 2

  Only split nodes with an objective lb equal to the global lb. If there is no objective, this is equivalent to SPLIT_STRATEGY_FIRST_PROPOSAL.

• SPLIT_STRATEGY_BALANCED_TREE = 3

  Attempt to keep the shared tree balanced.

• SPLIT_STRATEGY_FIRST_PROPOSAL = 4

  Workers race to split their subtree, the winner's proposal is accepted.

Variables without activity (i.e. at the beginning of the search) will be tried in this preferred order.

Used in: SatParameters

• IN_ORDER = 0

  As specified by the problem.

• IN_REVERSE_ORDER = 1

• IN_RANDOM_ORDER = 2

A permutation of integers encoded as a list of cycles, hence the "sparse" format. The image of an element cycle[i] is cycle[(i + 1) % cycle_length].

Used in: SymmetryProto

• repeated int32 support = 1

  Each cycle is listed one after the other in the support field. The size of each cycle is given (in order) in the cycle_sizes field.

• repeated int32 cycle_sizes = 2

EXPERIMENTAL. For now, this is meant to be used by the solver and not filled by clients. Hold symmetry information about the set of feasible solutions. If we permute the variable values of any feasible solution using one of the permutation described here, we should always get another feasible solution. We usually also enforce that the objective of the new solution is the same. The group of permutations encoded here is usually computed from the encoding of the model, so it is not meant to be a complete representation of the feasible solution symmetries, just a valid subgroup.

Used in: CpModelProto

• repeated SparsePermutationProto permutations = 1

  A list of variable indices permutations that leave the feasible space of solution invariant. Usually, we only encode a set of generators of the group.

• repeated DenseMatrixProto orbitopes = 2

  An orbitope is a special symmetry structure of the solution space. If the variable indices are arranged in a matrix (with no duplicates), then any permutation of the columns will be a valid permutation of the feasible space. This arise quite often. The typical example is a graph coloring problem where for each node i, you have j booleans to indicate its color. If the variables color_of_i_is_j are arranged in a matrix[i][j], then any columns permutations leave the problem invariant.

The values of the n-tuple formed by the given expression can only be one of the listed n-tuples in values. The n-tuples are encoded in a flattened way: [tuple0_v0, tuple0_v1, ..., tuple0_v{n-1}, tuple1_v0, ...]. Corner cases: - If all `vars`, `values` and `exprs` are empty, the constraint is trivially true, irrespective of the value of `negated`. - If `values` is empty but either vars or exprs is not, the constraint is trivially false if `negated` is false, and trivially true if `negated` is true. - If `vars` and `exprs` are empty but `values` is not, the model is invalid.

Used in: ConstraintProto

• repeated int32 vars = 1

  Legacy field.

• repeated int64 values = 2

• repeated LinearExpressionProto exprs = 4

• bool negated = 3

  If true, the meaning is "negated", that is we forbid any of the given tuple from a feasible assignment.