always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

some more dual presolve on exactly_one, at_most one in CP-SAT; minor cleaning

Browse Source
This commit is contained in:
Laurent Perron
2021-02-19 10:58:09 +01:00
parent 48303577e8
commit 247de5ae2a
15 changed files with 275 additions and 1164 deletions
Download Patch File Download Diff File Expand all files Collapse all files

32
ortools/sat/cp_model_postsolve.cc
View File

@@ -47,6 +47,35 @@ void PostsolveClause(const ConstraintProto& ct, std::vector<Domain>* domains) {
(*domains)[PositiveRef(first_ref)] = Domain(RefIsPositive(first_ref) ? 1 : 0);
}
void PostsolveExactlyOne(const ConstraintProto& ct,
std::vector<Domain>* domains) {
bool satisfied = false;
std::vector<int> free_variables;
for (const int ref : ct.exactly_one().literals()) {
const int var = PositiveRef(ref);
if ((*domains)[var].IsFixed()) {
if ((*domains)[var].FixedValue() == (RefIsPositive(ref) ? 1 : 0)) {
CHECK(!satisfied) << "Two variables at one in exactly one.";
satisfied = true;
}
} else {
free_variables.push_back(ref);
}
}
if (!satisfied) {
// Fix one at true.
CHECK(!free_variables.empty()) << "All zero in exactly one";
const int ref = free_variables.back();
(*domains)[PositiveRef(ref)] = Domain(RefIsPositive(ref) ? 1 : 0);
free_variables.pop_back();
}
// Fix any free variable left at false.
for (const int ref : free_variables) {
(*domains)[PositiveRef(ref)] = Domain(RefIsPositive(ref) ? 0 : 1);
}
}
// Here we simply assign all non-fixed variable to a feasible value. Which
// should always exists by construction.
void PostsolveLinear(const ConstraintProto& ct,
@@ -285,6 +314,9 @@ void PostsolveResponse(const int64 num_variables_in_original_model,
case ConstraintProto::kBoolOr:
PostsolveClause(ct, &domains);
break;
case ConstraintProto::kExactlyOne:
PostsolveExactlyOne(ct, &domains);
break;
case ConstraintProto::kLinear:
PostsolveLinear(ct, prefer_lower_value, &domains);
break;

41
ortools/sat/cp_model_presolve.cc
View File

@@ -343,8 +343,7 @@ bool CpModelPresolver::PresolveBoolAnd(ConstraintProto* ct) {
}
bool CpModelPresolver::PresolveAtMostOrExactlyOne(ConstraintProto* ct) {
const bool is_at_most_one =
ct->constraint_case() == ConstraintProto::kAtMostOne;
bool is_at_most_one = ct->constraint_case() == ConstraintProto::kAtMostOne;
const std::string name = is_at_most_one ? "at_most_one: " : "exactly_one: ";
auto* literals = is_at_most_one
? ct->mutable_at_most_one()->mutable_literals()
@@ -388,6 +387,7 @@ bool CpModelPresolver::PresolveAtMostOrExactlyOne(ConstraintProto* ct) {
// Remove fixed variables.
bool changed = false;
bool transform_to_at_most_one = false;
context_->tmp_literals.clear();
for (const int literal : *literals) {
if (context_->LiteralIsTrue(literal)) {
@@ -405,16 +405,45 @@ bool CpModelPresolver::PresolveAtMostOrExactlyOne(ConstraintProto* ct) {
continue;
}
// TODO(user): Most situation are already dealt with by the dual presolve
// code in var_domination.cc, so maybe we don't need it here.
if (context_->VariableIsUniqueAndRemovable(literal) ||
// A singleton variable in an at most one can just be set to zero.
//
// In an exactly one, it can be left to the postsolve to decide, and the
// rest of the constraint can be transformed to an at most one.
bool is_removable = context_->VariableIsUniqueAndRemovable(literal);
if (is_at_most_one && !is_removable &&
context_->VariableWithCostIsUniqueAndRemovable(literal)) {
context_->UpdateRuleStats("TODO [exactly/at_most]_one: singleton");
const auto it = context_->ObjectiveMap().find(PositiveRef(literal));
CHECK(it != context_->ObjectiveMap().end());
const int64 coeff = it->second;
// Fixing it to zero need to go in the correct direction.
is_removable = (coeff > 0) == RefIsPositive(literal);
}
if (is_removable) {
if (is_at_most_one) {
context_->UpdateRuleStats("at_most_one: singleton");
if (!context_->SetLiteralToFalse(literal)) return false;
changed = true;
continue;
} else {
changed = true;
is_at_most_one = true;
transform_to_at_most_one = true;
*(context_->mapping_model->add_constraints()) = *ct;
context_->UpdateRuleStats("exactly_one: singleton");
continue;
}
}
context_->tmp_literals.push_back(literal);
}
if (transform_to_at_most_one) {
CHECK(changed);
ct->Clear();
literals = ct->mutable_at_most_one()->mutable_literals();
}
if (changed) {
literals->Clear();
for (const int lit : context_->tmp_literals) {

22
ortools/sat/cp_model_symmetries.cc
View File

@@ -85,7 +85,7 @@ void Append(
// between each other.
template <typename Graph>
std::unique_ptr<Graph> GenerateGraphForSymmetryDetection(
const CpModelProto& problem,
bool log_info, const CpModelProto& problem,
std::vector<int>* initial_equivalence_classes) {
CHECK(initial_equivalence_classes != nullptr);
@@ -275,9 +275,11 @@ std::unique_ptr<Graph> GenerateGraphForSymmetryDetection(
// The other cases should be presolved before this is called.
// TODO(user): not 100% true, this happen on rmatr200-p5, Fix.
if (constraint.enforcement_literal_size() != 1) {
VLOG(1) << "BoolAnd with multiple enforcement literal are not "
"supported in symmetry code:"
<< constraint.ShortDebugString();
if (log_info) {
LOG(INFO) << "BoolAnd with multiple enforcement literal are not "
"supported in symmetry code:"
<< constraint.ShortDebugString();
}
return nullptr;
}
@@ -295,8 +297,10 @@ std::unique_ptr<Graph> GenerateGraphForSymmetryDetection(
// TODO(user): support other types of constraints. Or at least, we
// could associate to them an unique node so that their variables can
// appear in no symmetry.
LOG(ERROR) << "Unsupported constraint type "
<< ConstraintCaseName(constraint.constraint_case());
if (log_info) {
LOG(INFO) << "Unsupported constraint type "
<< ConstraintCaseName(constraint.constraint_case());
}
return nullptr;
}
}
@@ -331,7 +335,7 @@ std::unique_ptr<Graph> GenerateGraphForSymmetryDetection(
}
for (int i = 0; i < num_nodes; ++i) {
if (in_degree[i] >= num_nodes || out_degree[i] >= num_nodes) {
LOG(ERROR) << "Too many multi-arcs";
if (log_info) LOG(INFO) << "Too many multi-arcs in symmetry code.";
return nullptr;
}
}
@@ -377,8 +381,8 @@ void FindCpModelSymmetries(
typedef GraphSymmetryFinder::Graph Graph;
std::vector<int> equivalence_classes;
std::unique_ptr<Graph> graph(
GenerateGraphForSymmetryDetection<Graph>(problem, &equivalence_classes));
std::unique_ptr<Graph> graph(GenerateGraphForSymmetryDetection<Graph>(
log_info, problem, &equivalence_classes));
if (graph == nullptr) return;
if (log_info) {

1
ortools/sat/doc/README.md
View File

@@ -14,7 +14,6 @@
* [Java code samples](#java-code-samples)
* [C# code samples](#c-code-samples-1)
<!-- Added by: lperron, at: Fri Dec 18 09:46:38 CET 2020 -->
<!--te-->

1
ortools/sat/doc/boolean_logic.md
View File

@@ -26,7 +26,6 @@
* [Product of two Boolean Variables](#product-of-two-boolean-variables)
* [Python code](#python-code-3)
<!-- Added by: lperron, at: Fri Dec 18 09:46:39 CET 2020 -->
<!--te-->

1
ortools/sat/doc/channeling.md
View File

@@ -17,7 +17,6 @@
* [Java code](#java-code-1)
* [C# code](#c-code-3)
<!-- Added by: lperron, at: Fri Dec 18 09:46:40 CET 2020 -->
<!--te-->

1
ortools/sat/doc/integer_arithmetic.md
View File

@@ -33,7 +33,6 @@
* [Java code](#java-code-2)
* [C# code](#c-code-5)
<!-- Added by: lperron, at: Fri Dec 18 09:46:40 CET 2020 -->
<!--te-->

1
ortools/sat/doc/model.md
View File

@@ -16,7 +16,6 @@
* [Python code](#python-code-1)
* [C code](#c-code-2)
<!-- Added by: lperron, at: Wed Feb 17 18:36:47 CET 2021 -->
<!--te-->

928
ortools/sat/doc/reference.md
View File

@@ -1,928 +0,0 @@
| [home](README.md) | [boolean logic](boolean_logic.md) | [integer arithmetic](integer_arithmetic.md) | [channeling constraints](channeling.md) | [scheduling](scheduling.md) | [Using the CP-SAT solver](solver.md) | [Model manipulation](model.md) | [Reference manual](reference.md) |
| ----------------- | --------------------------------- | ------------------------------------------- | --------------------------------------- | --------------------------- | ------------------------------------ | ------------------------------ | -------------------------------- |
# ortools.sat.python.cp_model
Methods for building and solving CP-SAT models.
## DisplayBounds
```python
DisplayBounds(bounds)
```
Displays a flattened list of intervals.
## ShortName
```python
ShortName(model, i)
```
Returns a short name of an integer variable, or its negation.
## LinearExpr
```python
LinearExpr(self, /, *args, **kwargs)
```
Holds an integer linear expression.
A linear expression is built from integer constants and variables.
For example, x + 2 * (y - z + 1).
Linear expressions are used in CP-SAT models in two ways:
* To define constraints. For example
model.Add(x + 2 * y <= 5)
model.Add(sum(array_of_vars) == 5)
* To define the objective function. For example
model.Minimize(x + 2 * y + z)
For large arrays, you can create constraints and the objective
from lists of linear expressions or coefficients as follows:
model.Minimize(cp_model.LinearExpr.Sum(expressions))
model.Add(cp_model.LinearExpr.ScalProd(expressions, coefficients) >= 0)
### Sum
```python
LinearExpr.Sum(expressions)
```
Create the expression sum(expressions).
### ScalProd
```python
LinearExpr.ScalProd(expressions, coefficients)
```
Create the expression sum(expressions[i] * coefficients[i]).
### GetVarValueMap
```python
LinearExpr.GetVarValueMap(self)
```
Scan the expression, and return a list of (var_coef_map, constant).
## IntVar
```python
IntVar(self, model, domain, name)
```
An integer variable.
An IntVar is an object that can take on any integer value within defined
ranges. Variables appear in constraint like:
x + y >= 5
AllDifferent([x, y, z])
Solving a model is equivalent to finding, for each variable, a single value
from the set of initial values (called the initial domain), such that the
model is feasible, or optimal if you provided an objective function.
### Index
```python
IntVar.Index(self)
```
Returns the index of the variable in the model.
### Proto
```python
IntVar.Proto(self)
```
Returns the variable protobuf.
### Not
```python
IntVar.Not(self)
```
Returns the negation of a Boolean variable.
This method implements the logical negation of a Boolean variable.
It is only valid if the variable has a Boolean domain (0 or 1).
Note that this method is nilpotent: `x.Not().Not() == x`.
## BoundedLinearExpression
```python
BoundedLinearExpression(self, expr, bounds)
```
Represents a linear constraint: `lb <= linear expression <= ub`.
The only use of this class is to be added to the CpModel through
`CpModel.Add(expression)`, as in:
model.Add(x + 2 * y -1 >= z)
## Constraint
```python
Constraint(self, constraints)
```
Base class for constraints.
Constraints are built by the CpModel through the Add<XXX> methods.
Once created by the CpModel class, they are automatically added to the model.
The purpose of this class is to allow specification of enforcement literals
for this constraint.
b = model.BoolVar('b')
x = model.IntVar(0, 10, 'x')
y = model.IntVar(0, 10, 'y')
model.Add(x + 2 * y == 5).OnlyEnforceIf(b.Not())
### OnlyEnforceIf
```python
Constraint.OnlyEnforceIf(self, boolvar)
```
Adds an enforcement literal to the constraint.
**Args:**
- *boolvar:* A boolean literal or a list of boolean literals.
**Returns:**
self.
This method adds one or more literals (that is, a boolean variable or its
negation) as enforcement literals. The conjunction of all these literals
determines whether the constraint is active or not. It acts as an
implication, so if the conjunction is true, it implies that the constraint
must be enforced. If it is false, then the constraint is ignored.
BoolOr, BoolAnd, and linear constraints all support enforcement literals.
### Index
```python
Constraint.Index(self)
```
Returns the index of the constraint in the model.
### Proto
```python
Constraint.Proto(self)
```
Returns the constraint protobuf.
## IntervalVar
```python
IntervalVar(self, model, start_index, size_index, end_index, is_present_index, name)
```
Represents an Interval variable.
An interval variable is both a constraint and a variable. It is defined by
three integer variables: start, size, and end.
It is a constraint because, internally, it enforces that start + size == end.
It is also a variable as it can appear in specific scheduling constraints:
NoOverlap, NoOverlap2D, Cumulative.
Optionally, an enforcement literal can be added to this constraint, in which
case these scheduling constraints will ignore interval variables with
enforcement literals assigned to false. Conversely, these constraints will
also set these enforcement literals to false if they cannot fit these
intervals into the schedule.
### Index
```python
IntervalVar.Index(self)
```
Returns the index of the interval constraint in the model.
### Proto
```python
IntervalVar.Proto(self)
```
Returns the interval protobuf.
## CpModel
```python
CpModel(self)
```
Methods for building a CP model.
Methods beginning with:
* ```New``` create integer, boolean, or interval variables.
* ```Add``` create new constraints and add them to the model.
### NewIntVar
```python
CpModel.NewIntVar(self, lb, ub, name)
```
Create an integer variable with domain [lb, ub].
### NewIntVarFromDomain
```python
CpModel.NewIntVarFromDomain(self, domain, name)
```
Create an integer variable from a domain.
**Args:**
- *domain:* A instance of the Domain class.
- *name:* The name of the variable.
**Returns:**
a variable whose domain is the given domain.
### NewBoolVar
```python
CpModel.NewBoolVar(self, name)
```
Creates a 0-1 variable with the given name.
### NewConstant
```python
CpModel.NewConstant(self, value)
```
Declares a constant integer.
### AddLinearConstraint
```python
CpModel.AddLinearConstraint(self, linear_expr, lb, ub)
```
Adds the constraint: `lb <= linear_expr <= ub`.
### AddLinearExpressionInDomain
```python
CpModel.AddLinearExpressionInDomain(self, linear_expr, domain)
```
Adds the constraint: `linear_expr in domain`.
### Add
```python
CpModel.Add(self, ct)
```
Adds a BoundedLinearExpression to the model.
### AddAllDifferent
```python
CpModel.AddAllDifferent(self, variables)
```
Adds AllDifferent(variables).
This constraint forces all variables to have different values.
**Args:**
- *variables:* a list of integer variables.
**Returns:**
An instance of the `Constraint` class.
### AddElement
```python
CpModel.AddElement(self, index, variables, target)
```
Adds the element constraint: `variables[index] == target`.
### AddCircuit
```python
CpModel.AddCircuit(self, arcs)
```
Adds Circuit(arcs).
Adds a circuit constraint from a sparse list of arcs that encode the graph.
A circuit is a unique Hamiltonian path in a subgraph of the total
graph. In case a node 'i' is not in the path, then there must be a
loop arc 'i -> i' associated with a true literal. Otherwise
this constraint will fail.
**Args:**
- *arcs:* a list of arcs. An arc is a tuple (source_node, destination_node,
literal). The arc is selected in the circuit if the literal is true.
Both source_node and destination_node must be integers between 0 and the
number of nodes - 1.
**Returns:**
An instance of the `Constraint` class.
**Raises:**
- *ValueError:* If the list of arcs is empty.
### AddAllowedAssignments
```python
CpModel.AddAllowedAssignments(self, variables, tuples_list)
```
Adds AllowedAssignments(variables, tuples_list).
An AllowedAssignments constraint is a constraint on an array of variables
that forces, when all variables are fixed to a single value, the
corresponding list of values to be equal to one of the tuples of
`tuple_list`.
**Args:**
- *variables:* A list of variables.
- *tuples_list:* A list of admissible tuples. Each tuple must have the same
length as the variables, and the ith value of a tuple corresponds to the
ith variable.
**Returns:**
An instance of the `Constraint` class.
**Raises:**
- *TypeError:* If a tuple does not have the same size as the list of
variables.
- *ValueError:* If the array of variables is empty.
### AddForbiddenAssignments
```python
CpModel.AddForbiddenAssignments(self, variables, tuples_list)
```
Adds AddForbiddenAssignments(variables, [tuples_list]).
A ForbiddenAssignments constraint is a constraint on an array of variables
where the list of impossible combinations is provided in the tuples list.
**Args:**
- *variables:* A list of variables.
- *tuples_list:* A list of forbidden tuples. Each tuple must have the same
length as the variables, and the ith value of a tuple corresponds to the
ith variable.
**Returns:**
An instance of the `Constraint` class.
**Raises:**
- *TypeError:* If a tuple does not have the same size as the list of
variables.
- *ValueError:* If the array of variables is empty.
### AddAutomaton
```python
CpModel.AddAutomaton(self, transition_variables, starting_state, final_states, transition_triples)
```
Adds an automaton constraint.
An automaton constraint takes a list of variables (of size n), an initial
state, a set of final states, and a set of transitions. A transition is a
triplet (*tail*, *transition*, *head*), where *tail* and *head* are states,
and *transition* is the label of an arc from *head* to *tail*,
corresponding to the value of one variable in the list of variables.
This automaton will be unrolled into a flow with n + 1 phases. Each phase
contains the possible states of the automaton. The first state contains the
initial state. The last phase contains the final states.
Between two consecutive phases i and i + 1, the automaton creates a set of
arcs. For each transition (*tail*, *transition*, *head*), it will add an arc
from the state *tail* of phase i and the state *head* of phase i + 1. This
arc is labeled by the value *transition* of the variables `variables[i]`.
That is, this arc can only be selected if `variables[i]` is assigned the
value *transition*.
A feasible solution of this constraint is an assignment of variables such
that, starting from the initial state in phase 0, there is a path labeled by
the values of the variables that ends in one of the final states in the
final phase.
**Args:**
- *transition_variables:* A non-empty list of variables whose values
correspond to the labels of the arcs traversed by the automaton.
- *starting_state:* The initial state of the automaton.
- *final_states:* A non-empty list of admissible final states.
- *transition_triples:* A list of transitions for the automaton, in the
following format (current_state, variable_value, next_state).
**Returns:**
An instance of the `Constraint` class.
**Raises:**
- *ValueError:* if transition_variables, final_states, or transition_triples
are empty.
### AddInverse
```python
CpModel.AddInverse(self, variables, inverse_variables)
```
Adds Inverse(variables, inverse_variables).
An inverse constraint enforces that if `variables[i]` is assigned a value
`j`, then `inverse_variables[j]` is assigned a value `i`. And vice versa.
**Args:**
- *variables:* An array of integer variables.
- *inverse_variables:* An array of integer variables.
**Returns:**
An instance of the `Constraint` class.
**Raises:**
- *TypeError:* if variables and inverse_variables have different lengths, or
if they are empty.
### AddReservoirConstraint
```python
CpModel.AddReservoirConstraint(self, times, demands, min_level, max_level)
```
Adds Reservoir(times, demands, min_level, max_level).
Maintains a reservoir level within bounds. The water level starts at 0, and
at any time >= 0, it must be between min_level and max_level. Furthermore,
this constraints expect all times variables to be >= 0.
If the variable `times[i]` is assigned a value t, then the current level
changes by `demands[i]`, which is constant, at time t.
Note that level min can be > 0, or level max can be < 0. It just forces
some demands to be executed at time 0 to make sure that we are within those
bounds with the executed demands. Therefore, at any time t >= 0:
sum(demands[i] if times[i] <= t) in [min_level, max_level]
**Args:**
- *times:* A list of positive integer variables which specify the time of the
filling or emptying the reservoir.
- *demands:* A list of integer values that specifies the amount of the
emptying or feeling.
- *min_level:* At any time >= 0, the level of the reservoir must be greater of
equal than the min level.
- *max_level:* At any time >= 0, the level of the reservoir must be less or
equal than the max level.
**Returns:**
An instance of the `Constraint` class.
**Raises:**
- *ValueError:* if max_level < min_level.
### AddReservoirConstraintWithActive
```python
CpModel.AddReservoirConstraintWithActive(self, times, demands, actives, min_level, max_level)
```
Adds Reservoir(times, demands, actives, min_level, max_level).
Maintain a reservoir level within bounds. The water level starts at 0, and
at
any time >= 0, it must be within min_level, and max_level. Furthermore, this
constraints expect all times variables to be >= 0.
If `actives[i]` is true, and if `times[i]` is assigned a value t, then the
level of the reservoir changes by `demands[i]`, which is constant, at
time t.
Note that level_min can be > 0, or level_max can be < 0. It just forces
some demands to be executed at time 0 to make sure that we are within those
bounds with the executed demands. Therefore, at any time t >= 0:
sum(demands[i] * actives[i] if times[i] <= t) in [min_level, max_level]
The array of boolean variables 'actives', if defined, indicates which
actions are actually performed.
**Args:**
- *times:* A list of positive integer variables which specify the time of the
filling or emptying the reservoir.
- *demands:* A list of integer values that specifies the amount of the
emptying or feeling.
- *actives:* a list of boolean variables. They indicates if the
emptying/refilling events actually take place.
- *min_level:* At any time >= 0, the level of the reservoir must be greater of
equal than the min level.
- *max_level:* At any time >= 0, the level of the reservoir must be less or
equal than the max level.
**Returns:**
An instance of the `Constraint` class.
**Raises:**
- *ValueError:* if max_level < min_level.
### AddMapDomain
```python
CpModel.AddMapDomain(self, var, bool_var_array, offset=0)
```
Adds `var == i + offset <=> bool_var_array[i] == true for all i`.
### AddImplication
```python
CpModel.AddImplication(self, a, b)
```
Adds `a => b`.
### AddBoolOr
```python
CpModel.AddBoolOr(self, literals)
```
Adds `Or(literals) == true`.
### AddBoolAnd
```python
CpModel.AddBoolAnd(self, literals)
```
Adds `And(literals) == true`.
### AddBoolXOr
```python
CpModel.AddBoolXOr(self, literals)
```
Adds `XOr(literals) == true`.
### AddMinEquality
```python
CpModel.AddMinEquality(self, target, variables)
```
Adds `target == Min(variables)`.
### AddMaxEquality
```python
CpModel.AddMaxEquality(self, target, variables)
```
Adds `target == Max(variables)`.
### AddDivisionEquality
```python
CpModel.AddDivisionEquality(self, target, num, denom)
```
Adds `target == num // denom` (integer division rounded towards 0).
### AddAbsEquality
```python
CpModel.AddAbsEquality(self, target, var)
```
Adds `target == Abs(var)`.
### AddModuloEquality
```python
CpModel.AddModuloEquality(self, target, var, mod)
```
Adds `target = var % mod`.
### AddMultiplicationEquality
```python
CpModel.AddMultiplicationEquality(self, target, variables)
```
Adds `target == variables[0] * .. * variables[n]`.
### AddProdEquality
```python
CpModel.AddProdEquality(self, target, variables)
```
Deprecated, use AddMultiplicationEquality.
### NewIntervalVar
```python
CpModel.NewIntervalVar(self, start, size, end, name)
```
Creates an interval variable from start, size, and end.
An interval variable is a constraint, that is itself used in other
constraints like NoOverlap.
Internally, it ensures that `start + size == end`.
**Args:**
- *start:* The start of the interval. It can be an integer value, or an
integer variable.
- *size:* The size of the interval. It can be an integer value, or an integer
variable.
- *end:* The end of the interval. It can be an integer value, or an integer
variable.
- *name:* The name of the interval variable.
**Returns:**
An `IntervalVar` object.
### NewOptionalIntervalVar
```python
CpModel.NewOptionalIntervalVar(self, start, size, end, is_present, name)
```
Creates an optional interval var from start, size, end, and is_present.
An optional interval variable is a constraint, that is itself used in other
constraints like NoOverlap. This constraint is protected by an is_present
literal that indicates if it is active or not.
Internally, it ensures that `is_present implies start + size == end`.
**Args:**
- *start:* The start of the interval. It can be an integer value, or an
integer variable.
- *size:* The size of the interval. It can be an integer value, or an integer
variable.
- *end:* The end of the interval. It can be an integer value, or an integer
variable.
- *is_present:* A literal that indicates if the interval is active or not. A
inactive interval is simply ignored by all constraints.
- *name:* The name of the interval variable.
**Returns:**
An `IntervalVar` object.
### AddNoOverlap
```python
CpModel.AddNoOverlap(self, interval_vars)
```
Adds NoOverlap(interval_vars).
A NoOverlap constraint ensures that all present intervals do not overlap
in time.
**Args:**
- *interval_vars:* The list of interval variables to constrain.
**Returns:**
An instance of the `Constraint` class.
### AddNoOverlap2D
```python
CpModel.AddNoOverlap2D(self, x_intervals, y_intervals)
```
Adds NoOverlap2D(x_intervals, y_intervals).
A NoOverlap2D constraint ensures that all present rectangles do not overlap
on a plane. Each rectangle is aligned with the X and Y axis, and is defined
by two intervals which represent its projection onto the X and Y axis.
**Args:**
- *x_intervals:* The X coordinates of the rectangles.
- *y_intervals:* The Y coordinates of the rectangles.
**Returns:**
An instance of the `Constraint` class.
### AddCumulative
```python
CpModel.AddCumulative(self, intervals, demands, capacity)
```
Adds Cumulative(intervals, demands, capacity).
This constraint enforces that:
for all t:
sum(demands[i]
if (start(intervals[t]) <= t < end(intervals[t])) and
(t is present)) <= capacity
**Args:**
- *intervals:* The list of intervals.
- *demands:* The list of demands for each interval. Each demand must be >= 0.
Each demand can be an integer value, or an integer variable.
- *capacity:* The maximum capacity of the cumulative constraint. It must be a
positive integer value or variable.
**Returns:**
An instance of the `Constraint` class.
### Proto
```python
CpModel.Proto(self)
```
Returns the underling CpModelProto.
### GetOrMakeIndex
```python
CpModel.GetOrMakeIndex(self, arg)
```
Returns the index of a variables, its negation, or a number.
### GetOrMakeBooleanIndex
```python
CpModel.GetOrMakeBooleanIndex(self, arg)
```
Returns an index from a boolean expression.
### Minimize
```python
CpModel.Minimize(self, obj)
```
Sets the objective of the model to minimize(obj).
### Maximize
```python
CpModel.Maximize(self, obj)
```
Sets the objective of the model to maximize(obj).
### AddDecisionStrategy
```python
CpModel.AddDecisionStrategy(self, variables, var_strategy, domain_strategy)
```
Adds a search strategy to the model.
**Args:**
- *variables:* a list of variables this strategy will assign.
- *var_strategy:* heuristic to choose the next variable to assign.
- *domain_strategy:* heuristic to reduce the domain of the selected variable.
Currently, this is advanced code: the union of all strategies added to
the model must be complete, i.e. instantiates all variables.
Otherwise, Solve() will fail.
### ModelStats
```python
CpModel.ModelStats(self)
```
Returns a string containing some model statistics.
### Validate
```python
CpModel.Validate(self)
```
Returns a string indicating that the model is invalid.
## EvaluateLinearExpr
```python
EvaluateLinearExpr(expression, solution)
```
Evaluate a linear expression against a solution.
## EvaluateBooleanExpression
```python
EvaluateBooleanExpression(literal, solution)
```
Evaluate a boolean expression against a solution.
## CpSolver
```python
CpSolver(self)
```
Main solver class.
The purpose of this class is to search for a solution to the model provided
to the Solve() method.
Once Solve() is called, this class allows inspecting the solution found
with the Value() and BooleanValue() methods, as well as general statistics
about the solve procedure.
### Solve
```python
CpSolver.Solve(self, model)
```
Solves the given model and returns the solve status.
### SolveWithSolutionCallback
```python
CpSolver.SolveWithSolutionCallback(self, model, callback)
```
Solves a problem and passes each solution found to the callback.
### SearchForAllSolutions
```python
CpSolver.SearchForAllSolutions(self, model, callback)
```
Search for all solutions of a satisfiability problem.
This method searches for all feasible solutions of a given model.
Then it feeds the solution to the callback.
Note that the model cannot contain an objective.
**Args:**
- *model:* The model to solve.
- *callback:* The callback that will be called at each solution.
**Returns:**
The status of the solve:
* *FEASIBLE* if some solutions have been found
* *INFEASIBLE* if the solver has proved there are no solution
* *OPTIMAL* if all solutions have been found
### Value
```python
CpSolver.Value(self, expression)
```
Returns the value of a linear expression after solve.
### BooleanValue
```python
CpSolver.BooleanValue(self, literal)
```
Returns the boolean value of a literal after solve.
### ObjectiveValue
```python
CpSolver.ObjectiveValue(self)
```
Returns the value of the objective after solve.
### BestObjectiveBound
```python
CpSolver.BestObjectiveBound(self)
```
Returns the best lower (upper) bound found when min(max)imizing.
### StatusName
```python
CpSolver.StatusName(self, status)
```
Returns the name of the status returned by Solve().
### NumBooleans
```python
CpSolver.NumBooleans(self)
```
Returns the number of boolean variables managed by the SAT solver.
### NumConflicts
```python
CpSolver.NumConflicts(self)
```
Returns the number of conflicts since the creation of the solver.
### NumBranches
```python
CpSolver.NumBranches(self)
```
Returns the number of search branches explored by the solver.
### WallTime
```python
CpSolver.WallTime(self)
```
Returns the wall time in seconds since the creation of the solver.
### UserTime
```python
CpSolver.UserTime(self)
```
Returns the user time in seconds since the creation of the solver.
### ResponseStats
```python
CpSolver.ResponseStats(self)
```
Returns some statistics on the solution found as a string.
### ResponseProto
```python
CpSolver.ResponseProto(self)
```
Returns the response object.
## CpSolverSolutionCallback
```python
CpSolverSolutionCallback(self)
```
Solution callback.
This class implements a callback that will be called at each new solution
found during search.
The method OnSolutionCallback() will be called by the solver, and must be
implemented. The current solution can be queried using the BooleanValue()
and Value() methods.
It inherits the following methods from its base class:
* `ObjectiveValue(self)`
* `BestObjectiveBound(self)`
* `NumBooleans(self)`
* `NumConflicts(self)`
* `NumBranches(self)`
* `WallTime(self)`
* `UserTime(self)`
These methods returns the same information as their counterpart in the
`CpSolver` class.
### OnSolutionCallback
```python
CpSolverSolutionCallback.OnSolutionCallback(self)
```
Proxy for the same method in snake case.
### BooleanValue
```python
CpSolverSolutionCallback.BooleanValue(self, lit)
```
Returns the boolean value of a boolean literal.
**Args:**
- *lit:* A boolean variable or its negation.
**Returns:**
The Boolean value of the literal in the solution.
**Raises:**
- *RuntimeError:* if `lit` is not a boolean variable or its negation.
### Value
```python
CpSolverSolutionCallback.Value(self, expression)
```
Evaluates an linear expression in the current solution.
**Args:**
- *expression:* a linear expression of the model.
**Returns:**
An integer value equal to the evaluation of the linear expression
against the current solution.
**Raises:**
- *RuntimeError:* if 'expression' is not a LinearExpr.
## ObjectiveSolutionPrinter
```python
ObjectiveSolutionPrinter(self)
```
Display the objective value and time of intermediate solutions.
### on_solution_callback
```python
ObjectiveSolutionPrinter.on_solution_callback(self)
```
Called on each new solution.
### solution_count
```python
ObjectiveSolutionPrinter.solution_count(self)
```
Returns the number of solutions found.
## VarArrayAndObjectiveSolutionPrinter
```python
VarArrayAndObjectiveSolutionPrinter(self, variables)
```
Print intermediate solutions (objective, variable values, time).
### on_solution_callback
```python
VarArrayAndObjectiveSolutionPrinter.on_solution_callback(self)
```
Called on each new solution.
### solution_count
```python
VarArrayAndObjectiveSolutionPrinter.solution_count(self)
```
Returns the number of solutions found.
## VarArraySolutionPrinter
```python
VarArraySolutionPrinter(self, variables)
```
Print intermediate solutions (variable values, time).
### on_solution_callback
```python
VarArraySolutionPrinter.on_solution_callback(self)
```
Called on each new solution.
### solution_count
```python
VarArraySolutionPrinter.solution_count(self)
```
Returns the number of solutions found.

1
ortools/sat/doc/scheduling.md
View File

@@ -36,7 +36,6 @@
* [Convex hull of a set of intervals](#convex-hull-of-a-set-of-intervals)
* [Reservoir constraint](#reservoir-constraint)
<!-- Added by: lperron, at: Fri Dec 18 09:46:42 CET 2020 -->
<!--te-->

1
ortools/sat/doc/solver.md
View File

@@ -27,7 +27,6 @@
* [Java code](#java-code-2)
* [C# code](#c-code-5)
<!-- Added by: lperron, at: Fri Dec 18 09:46:43 CET 2020 -->
<!--te-->

122
ortools/sat/samples/AssignmentSat.java
View File

@@ -41,79 +41,75 @@ public class AssignmentSat {
// [END data_model]
// Model
try {
// [START model]
CpModel model = new CpModel();
// [END model]
// [START model]
CpModel model = new CpModel();
// [END model]
// Variables
// [START variables]
IntVar[][] x = new IntVar[numWorkers][numTasks];
// Variables in a 1-dim array.
IntVar[] xFlat = new IntVar[numWorkers * numTasks];
int[] costsFlat = new int[numWorkers * numTasks];
for (int i = 0; i < numWorkers; ++i) {
for (int j = 0; j < numTasks; ++j) {
x[i][j] = model.newIntVar(0, 1, "");
int k = i * numTasks + j;
xFlat[k] = x[i][j];
costsFlat[k] = costs[i][j];
}
}
// [END variables]
// Constraints
// [START constraints]
// Each worker is assigned to at most one task.
for (int i = 0; i < numWorkers; ++i) {
IntVar[] vars = new IntVar[numTasks];
for (int j = 0; j < numTasks; ++j) {
vars[j] = x[i][j];
}
model.addLessOrEqual(LinearExpr.sum(vars), 1);
}
// Each task is assigned to exactly one worker.
// Variables
// [START variables]
IntVar[][] x = new IntVar[numWorkers][numTasks];
// Variables in a 1-dim array.
IntVar[] xFlat = new IntVar[numWorkers * numTasks];
int[] costsFlat = new int[numWorkers * numTasks];
for (int i = 0; i < numWorkers; ++i) {
for (int j = 0; j < numTasks; ++j) {
// LinearExpr taskSum;
IntVar[] vars = new IntVar[numWorkers];
for (int i = 0; i < numWorkers; ++i) {
vars[i] = x[i][j];
}
model.addEquality(LinearExpr.sum(vars), 1);
x[i][j] = model.newIntVar(0, 1, "");
int k = i * numTasks + j;
xFlat[k] = x[i][j];
costsFlat[k] = costs[i][j];
}
// [END constraints]
}
// [END variables]
// Objective
// [START objective]
model.minimize(LinearExpr.scalProd(xFlat, costsFlat));
// [END objective]
// Constraints
// [START constraints]
// Each worker is assigned to at most one task.
for (int i = 0; i < numWorkers; ++i) {
IntVar[] vars = new IntVar[numTasks];
for (int j = 0; j < numTasks; ++j) {
vars[j] = x[i][j];
}
model.addLessOrEqual(LinearExpr.sum(vars), 1);
}
// Each task is assigned to exactly one worker.
for (int j = 0; j < numTasks; ++j) {
// LinearExpr taskSum;
IntVar[] vars = new IntVar[numWorkers];
for (int i = 0; i < numWorkers; ++i) {
vars[i] = x[i][j];
}
model.addEquality(LinearExpr.sum(vars), 1);
}
// [END constraints]
// Solve
// [START solve]
CpSolver solver = new CpSolver();
CpSolverStatus status = solver.solve(model);
// [END solve]
// Objective
// [START objective]
model.minimize(LinearExpr.scalProd(xFlat, costsFlat));
// [END objective]
// Print solution.
// [START print_solution]
// Check that the problem has a feasible solution.
if (status == CpSolverStatus.OPTIMAL || status == CpSolverStatus.FEASIBLE) {
System.out.println("Total cost: " + solver.objectiveValue() + "\n");
for (int i = 0; i < numWorkers; ++i) {
for (int j = 0; j < numTasks; ++j) {
if (solver.value(x[i][j]) == 1) {
System.out.println(
"Worker " + i + " assigned to task " + j + ". Cost: " + costs[i][j]);
}
// Solve
// [START solve]
CpSolver solver = new CpSolver();
CpSolverStatus status = solver.solve(model);
// [END solve]
// Print solution.
// [START print_solution]
// Check that the problem has a feasible solution.
if (status == CpSolverStatus.OPTIMAL || status == CpSolverStatus.FEASIBLE) {
System.out.println("Total cost: " + solver.objectiveValue() + "\n");
for (int i = 0; i < numWorkers; ++i) {
for (int j = 0; j < numTasks; ++j) {
if (solver.value(x[i][j]) == 1) {
System.out.println(
"Worker " + i + " assigned to task " + j + ". Cost: " + costs[i][j]);
}
}
} else {
System.err.println("No solution found.");
}
// [END print_solution]
} catch (Exception e) {
System.err.println("Caught " + e + " while building the model");
} else {
System.err.println("No solution found.");
}
// [END print_solution]
}
private AssignmentSat() {}

120
ortools/sat/samples/MultipleKnapsackSat.java
View File

@@ -69,72 +69,68 @@ public class MultipleKnapsackSat {
totalValue = totalValue + data.values[i];
}
try {
// [START model]
CpModel model = new CpModel();
// [END model]
// [START model]
CpModel model = new CpModel();
// [END model]
// [START variables]
IntVar[][] x = new IntVar[data.numItems][data.numBins];
for (int i = 0; i < data.numItems; ++i) {
for (int b = 0; b < data.numBins; ++b) {
x[i][b] = model.newIntVar(0, 1, "x_" + i + "_" + b);
}
}
// Main variables.
// Load and value variables.
IntVar[] load = new IntVar[data.numBins];
IntVar[] value = new IntVar[data.numBins];
// [START variables]
IntVar[][] x = new IntVar[data.numItems][data.numBins];
for (int i = 0; i < data.numItems; ++i) {
for (int b = 0; b < data.numBins; ++b) {
load[b] = model.newIntVar(0, data.binCapacities[b], "load_" + b);
value[b] = model.newIntVar(0, totalValue, "value_" + b);
x[i][b] = model.newIntVar(0, 1, "x_" + i + "_" + b);
}
// Links load and value with x.
int[] sizes = new int[data.numItems];
for (int i = 0; i < data.numItems; ++i) {
sizes[i] = data.items[i];
}
for (int b = 0; b < data.numBins; ++b) {
IntVar[] vars = new IntVar[data.numItems];
for (int i = 0; i < data.numItems; ++i) {
vars[i] = x[i][b];
}
model.addEquality(LinearExpr.scalProd(vars, data.items), load[b]);
model.addEquality(LinearExpr.scalProd(vars, data.values), value[b]);
}
// [END variables]
// [START constraints]
// Each item can be in at most one bin.
// Place all items.
for (int i = 0; i < data.numItems; ++i) {
IntVar[] vars = new IntVar[data.numBins];
for (int b = 0; b < data.numBins; ++b) {
vars[b] = x[i][b];
}
model.addLessOrEqual(LinearExpr.sum(vars), 1);
}
// [END constraints]
// Maximize sum of load.
// [START objective]
model.maximize(LinearExpr.sum(value));
// [END objective]
// [START solve]
CpSolver solver = new CpSolver();
CpSolverStatus status = solver.solve(model);
// [END solve]
// [START print_solution]
System.out.println("Solve status: " + status);
if (status == CpSolverStatus.OPTIMAL) {
printSolution(data, solver, x, load, value);
}
// [END print_solution]
} catch (Exception e) {
System.err.println("Caught " + e + " while building the model");
}
// Main variables.
// Load and value variables.
IntVar[] load = new IntVar[data.numBins];
IntVar[] value = new IntVar[data.numBins];
for (int b = 0; b < data.numBins; ++b) {
load[b] = model.newIntVar(0, data.binCapacities[b], "load_" + b);
value[b] = model.newIntVar(0, totalValue, "value_" + b);
}
// Links load and value with x.
int[] sizes = new int[data.numItems];
for (int i = 0; i < data.numItems; ++i) {
sizes[i] = data.items[i];
}
for (int b = 0; b < data.numBins; ++b) {
IntVar[] vars = new IntVar[data.numItems];
for (int i = 0; i < data.numItems; ++i) {
vars[i] = x[i][b];
}
model.addEquality(LinearExpr.scalProd(vars, data.items), load[b]);
model.addEquality(LinearExpr.scalProd(vars, data.values), value[b]);
}
// [END variables]
// [START constraints]
// Each item can be in at most one bin.
// Place all items.
for (int i = 0; i < data.numItems; ++i) {
IntVar[] vars = new IntVar[data.numBins];
for (int b = 0; b < data.numBins; ++b) {
vars[b] = x[i][b];
}
model.addLessOrEqual(LinearExpr.sum(vars), 1);
}
// [END constraints]
// Maximize sum of load.
// [START objective]
model.maximize(LinearExpr.sum(value));
// [END objective]
// [START solve]
CpSolver solver = new CpSolver();
CpSolverStatus status = solver.solve(model);
// [END solve]
// [START print_solution]
System.out.println("Solve status: " + status);
if (status == CpSolverStatus.OPTIMAL) {
printSolution(data, solver, x, load, value);
}
// [END print_solution]
}
private MultipleKnapsackSat() {}

162
ortools/sat/samples/RankingSampleSat.java
View File

@@ -29,14 +29,12 @@ public class RankingSampleSat {
/**
* This code takes a list of interval variables in a noOverlap constraint, and a parallel list of
* integer variables and enforces the following constraint
*
* <ul>
* <li>rank[i] == -1 iff interval[i] is not active.
* <li>rank[i] == number of active intervals that precede interval[i].
* <li>rank[i] == -1 iff interval[i] is not active.
* <li>rank[i] == number of active intervals that precede interval[i].
* </ul>
*/
static void rankTasks(CpModel model, IntVar[] starts, Literal[] presences, IntVar[] ranks)
throws Exception {
static void rankTasks(CpModel model, IntVar[] starts, Literal[] presences, IntVar[] ranks) {
int numTasks = starts.length;
// Creates precedence variables between pairs of intervals.
@@ -97,91 +95,85 @@ public class RankingSampleSat {
public static void main(String[] args) throws Exception {
Loader.loadNativeLibraries();
try {
CpModel model = new CpModel();
int horizon = 100;
int numTasks = 4;
CpModel model = new CpModel();
int horizon = 100;
int numTasks = 4;
IntVar[] starts = new IntVar[numTasks];
IntVar[] ends = new IntVar[numTasks];
IntervalVar[] intervals = new IntervalVar[numTasks];
Literal[] presences = new Literal[numTasks];
IntVar[] ranks = new IntVar[numTasks];
IntVar[] starts = new IntVar[numTasks];
IntVar[] ends = new IntVar[numTasks];
IntervalVar[] intervals = new IntervalVar[numTasks];
Literal[] presences = new Literal[numTasks];
IntVar[] ranks = new IntVar[numTasks];
IntVar trueVar = model.newConstant(1);
IntVar trueVar = model.newConstant(1);
// Creates intervals, half of them are optional.
for (int t = 0; t < numTasks; ++t) {
starts[t] = model.newIntVar(0, horizon, "start_" + t);
int duration = t + 1;
ends[t] = model.newIntVar(0, horizon, "end_" + t);
if (t < numTasks / 2) {
intervals[t] = model.newIntervalVar(starts[t], duration, ends[t], "interval_" + t);
presences[t] = trueVar;
} else {
presences[t] = model.newBoolVar("presence_" + t);
intervals[t] = model.newOptionalIntervalVar(
starts[t], duration, ends[t], presences[t], "o_interval_" + t);
}
// The rank will be -1 iff the task is not performed.
ranks[t] = model.newIntVar(-1, numTasks - 1, "rank_" + t);
}
// Adds NoOverlap constraint.
model.addNoOverlap(intervals);
// Adds ranking constraint.
rankTasks(model, starts, presences, ranks);
// Adds a constraint on ranks (ranks[0] < ranks[1]).
model.addLessOrEqualWithOffset(ranks[0], ranks[1], 1);
// Creates makespan variable.
IntVar makespan = model.newIntVar(0, horizon, "makespan");
for (int t = 0; t < numTasks; ++t) {
model.addLessOrEqual(ends[t], makespan).onlyEnforceIf(presences[t]);
}
// The objective function is a mix of a fixed gain per task performed, and a fixed cost for
// each
// additional day of activity.
// The solver will balance both cost and gain and minimize makespan * per-day-penalty - number
// of tasks performed * per-task-gain.
//
// On this problem, as the fixed cost is less that the duration of the last interval, the
// solver
// will not perform the last interval.
IntVar[] objectiveVars = new IntVar[numTasks + 1];
int[] objectiveCoefs = new int[numTasks + 1];
for (int t = 0; t < numTasks; ++t) {
objectiveVars[t] = (IntVar) presences[t];
objectiveCoefs[t] = -7;
}
objectiveVars[numTasks] = makespan;
objectiveCoefs[numTasks] = 2;
model.minimize(LinearExpr.scalProd(objectiveVars, objectiveCoefs));
// Creates a solver and solves the model.
CpSolver solver = new CpSolver();
CpSolverStatus status = solver.solve(model);
if (status == CpSolverStatus.OPTIMAL) {
System.out.println("Optimal cost: " + solver.objectiveValue());
System.out.println("Makespan: " + solver.value(makespan));
for (int t = 0; t < numTasks; ++t) {
if (solver.booleanValue(presences[t])) {
System.out.printf("Task %d starts at %d with rank %d%n", t, solver.value(starts[t]),
solver.value(ranks[t]));
} else {
System.out.printf(
"Task %d in not performed and ranked at %d%n", t, solver.value(ranks[t]));
}
}
// Creates intervals, half of them are optional.
for (int t = 0; t < numTasks; ++t) {
starts[t] = model.newIntVar(0, horizon, "start_" + t);
int duration = t + 1;
ends[t] = model.newIntVar(0, horizon, "end_" + t);
if (t < numTasks / 2) {
intervals[t] = model.newIntervalVar(starts[t], duration, ends[t], "interval_" + t);
presences[t] = trueVar;
} else {
System.out.println("Solver exited with nonoptimal status: " + status);
presences[t] = model.newBoolVar("presence_" + t);
intervals[t] = model.newOptionalIntervalVar(
starts[t], duration, ends[t], presences[t], "o_interval_" + t);
}
} catch (Exception e) {
System.err.println("Caught " + e + " while building the model");
// The rank will be -1 iff the task is not performed.
ranks[t] = model.newIntVar(-1, numTasks - 1, "rank_" + t);
}
// Adds NoOverlap constraint.
model.addNoOverlap(intervals);
// Adds ranking constraint.
rankTasks(model, starts, presences, ranks);
// Adds a constraint on ranks (ranks[0] < ranks[1]).
model.addLessOrEqualWithOffset(ranks[0], ranks[1], 1);
// Creates makespan variable.
IntVar makespan = model.newIntVar(0, horizon, "makespan");
for (int t = 0; t < numTasks; ++t) {
model.addLessOrEqual(ends[t], makespan).onlyEnforceIf(presences[t]);
}
// The objective function is a mix of a fixed gain per task performed, and a fixed cost for each
// additional day of activity.
// The solver will balance both cost and gain and minimize makespan * per-day-penalty - number
// of tasks performed * per-task-gain.
//
// On this problem, as the fixed cost is less that the duration of the last interval, the solver
// will not perform the last interval.
IntVar[] objectiveVars = new IntVar[numTasks + 1];
int[] objectiveCoefs = new int[numTasks + 1];
for (int t = 0; t < numTasks; ++t) {
objectiveVars[t] = (IntVar) presences[t];
objectiveCoefs[t] = -7;
}
objectiveVars[numTasks] = makespan;
objectiveCoefs[numTasks] = 2;
model.minimize(LinearExpr.scalProd(objectiveVars, objectiveCoefs));
// Creates a solver and solves the model.
CpSolver solver = new CpSolver();
CpSolverStatus status = solver.solve(model);
if (status == CpSolverStatus.OPTIMAL) {
System.out.println("Optimal cost: " + solver.objectiveValue());
System.out.println("Makespan: " + solver.value(makespan));
for (int t = 0; t < numTasks; ++t) {
if (solver.booleanValue(presences[t])) {
System.out.printf("Task %d starts at %d with rank %d%n", t, solver.value(starts[t]),
solver.value(ranks[t]));
} else {
System.out.printf(
"Task %d in not performed and ranked at %d%n", t, solver.value(ranks[t]));
}
}
} else {
System.out.println("Solver exited with nonoptimal status: " + status);
}
}
}

5
ortools/sat/util.h
View File

@@ -57,10 +57,7 @@ class ModelRandomGenerator : public absl::BitGenRef {
// log.
//
// TODO(user): I didn't find a cleaner way to log this.
void LogSalt() const {
// absl::BitGen(
// absl::MakeTaggedSeedSeq("UNUSED", absl::LogInfoStreamer().stream()));
}
void LogSalt() const {}
private:
random_engine_t deterministic_random_;