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

[CP-SAT] better dtime for scheduling constraints; connect the time limit in the repair_hint mode; fix #4743

Browse Source
This commit is contained in:
Laurent Perron
2025-07-29 09:07:13 -07:00
parent a3fc2000e4
commit 9fa9bd4da4
15 changed files with 685 additions and 466 deletions
Download Patch File Download Diff File Expand all files Collapse all files

5
ortools/sat/BUILD.bazel
View File

@@ -1800,6 +1800,7 @@ cc_test(
deps = [
":integer_base",
"//ortools/base:gmock_main",
"@abseil-cpp//absl/log:check",
],
)
@@ -2098,9 +2099,7 @@ cc_library(
"//ortools/base",
"//ortools/base:mathutil",
"//ortools/base:strong_vector",
"//ortools/graph",
"//ortools/graph:topologicalsorter",
"//ortools/util:bitset",
"//ortools/util:logging",
"//ortools/util:rev",
"//ortools/util:strong_integers",
@@ -2335,6 +2334,7 @@ cc_library(
"//ortools/util:sort",
"//ortools/util:strong_integers",
"@abseil-cpp//absl/algorithm:container",
"@abseil-cpp//absl/cleanup",
"@abseil-cpp//absl/log",
"@abseil-cpp//absl/log:check",
"@abseil-cpp//absl/log:vlog_is_on",
@@ -3614,6 +3614,7 @@ cc_library(
":synchronization",
":timetable",
":util",
"//ortools/base:stl_util",
"//ortools/util:bitset",
"//ortools/util:saturated_arithmetic",
"//ortools/util:strong_integers",

11
ortools/sat/cp_model_solver.cc
View File

@@ -1076,7 +1076,9 @@ class FullProblemSolver : public SubSolver {
previous_task_is_completed_ = false;
}
return [this]() {
auto* time_limit = local_model_.GetOrCreate<TimeLimit>();
if (solving_first_chunk_) {
const double init_dtime = time_limit->GetElapsedDeterministicTime();
LoadCpModel(shared_->model_proto, &local_model_);
// Level zero variable bounds sharing. It is important to register
@@ -1127,15 +1129,18 @@ class FullProblemSolver : public SubSolver {
// No need for mutex since we only run one task at the time.
solving_first_chunk_ = false;
// Make sure we count the loading/hint dtime.
absl::MutexLock mutex_lock(&mutex_);
dtime_since_last_sync_ +=
time_limit->GetElapsedDeterministicTime() - init_dtime;
// Abort first chunk and allow to schedule the next.
if (split_in_chunks_) {
// Abort first chunk and allow to schedule the next.
absl::MutexLock mutex_lock(&mutex_);
previous_task_is_completed_ = true;
return;
}
}
auto* time_limit = local_model_.GetOrCreate<TimeLimit>();
if (split_in_chunks_) {
// Configure time limit for chunk solving. Note that we do not want
// to do that for the hint search for now.

11
ortools/sat/cp_model_solver_helpers.cc
View File

@@ -1866,10 +1866,9 @@ void QuickSolveWithHint(const CpModelProto& model_proto, Model* model) {
void MinimizeL1DistanceWithHint(const CpModelProto& model_proto, Model* model) {
Model local_model;
// Forward some shared class.
local_model.Register<ModelSharedTimeLimit>(
model->GetOrCreate<ModelSharedTimeLimit>());
local_model.Register<WallTimer>(model->GetOrCreate<WallTimer>());
// Pass the time limit and stop boolean to local limit.
model->GetOrCreate<ModelSharedTimeLimit>()->UpdateLocalLimit(
local_model.GetOrCreate<TimeLimit>());
if (!model_proto.has_solution_hint()) return;
@@ -1967,6 +1966,10 @@ void MinimizeL1DistanceWithHint(const CpModelProto& model_proto, Model* model) {
shared_response_manager->NewSolution(
solution, absl::StrCat(solution_info, " [repaired]"), &local_model);
}
// Make sure we update the higher model with the timing info.
model->GetOrCreate<TimeLimit>()->AdvanceDeterministicTime(
local_model.GetOrCreate<TimeLimit>()->GetElapsedDeterministicTime());
}
// TODO(user): If this ever shows up in the profile, we could avoid copying

9
ortools/sat/disjunctive.cc
View File

@@ -18,6 +18,7 @@
#include <vector>
#include "absl/algorithm/container.h"
#include "absl/cleanup/cleanup.h"
#include "absl/log/check.h"
#include "absl/log/log.h"
#include "absl/types/span.h"
@@ -1195,6 +1196,13 @@ bool DisjunctivePrecedences::Propagate() {
}
bool DisjunctivePrecedences::PropagateSubwindow() {
// This function can be slow, so count it in the dtime.
int64_t num_hash_lookup = 0;
auto cleanup = ::absl::MakeCleanup([&num_hash_lookup, this]() {
time_limit_->AdvanceDeterministicTime(static_cast<double>(num_hash_lookup) *
5e-8);
});
// TODO(user): We shouldn't consider ends for fixed intervals here. But
// then we should do a better job of computing the min-end of a subset of
// intervals from this disjunctive (like using fixed intervals even if there
@@ -1278,6 +1286,7 @@ bool DisjunctivePrecedences::PropagateSubwindow() {
// TODO(user): The lookup here is a bit slow, so we avoid fetching
// the offset as much as possible.
++num_hash_lookup;
const IntegerValue inner_offset =
-linear2_bounds_->NonTrivialUpperBound(lin2_index);
DCHECK_NE(inner_offset, kMinIntegerValue);

2
ortools/sat/disjunctive.h
View File

@@ -355,6 +355,7 @@ class DisjunctivePrecedences : public PropagatorInterface {
integer_trail_(model->GetOrCreate<IntegerTrail>()),
precedence_relations_(model->GetOrCreate<EnforcedLinear2Bounds>()),
linear2_bounds_(model->GetOrCreate<Linear2Bounds>()),
time_limit_(model->GetOrCreate<TimeLimit>()),
stats_("DisjunctivePrecedences", model) {
window_.ClearAndReserve(helper->NumTasks());
index_to_end_vars_.ClearAndReserve(helper->NumTasks());
@@ -372,6 +373,7 @@ class DisjunctivePrecedences : public PropagatorInterface {
IntegerTrail* integer_trail_;
EnforcedLinear2Bounds* precedence_relations_;
Linear2Bounds* linear2_bounds_;
TimeLimit* time_limit_;
FixedCapacityVector<TaskTime> window_;
FixedCapacityVector<IntegerVariable> index_to_end_vars_;

209
ortools/sat/docs/boolean_logic.md
View File

@@ -20,7 +20,21 @@ negation of `x`.
### Python code
```python
# Snippet from ortools/sat/samples/literal_sample_sat.py
#!/usr/bin/env python3
# Copyright 2010-2025 Google LLC
# Licensed under the Apache License, Version 2.0 (the "License");
# you may not use this file except in compliance with the License.
# You may obtain a copy of the License at
#
# http://www.apache.org/licenses/LICENSE-2.0
#
# Unless required by applicable law or agreed to in writing, software
# distributed under the License is distributed on an "AS IS" BASIS,
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
# See the License for the specific language governing permissions and
# limitations under the License.
"""Code sample to demonstrate Boolean variable and literals."""
@@ -28,25 +42,27 @@ from ortools.sat.python import cp_model
def literal_sample_sat():
model = cp_model.CpModel()
x = model.new_bool_var("x")
not_x = ~x
print(x)
print(not_x)
model = cp_model.CpModel()
x = model.new_bool_var('x')
not_x = ~x
print(x)
print(not_x)
literal_sample_sat()
```
### C++ code
```cpp
// Snippet from ortools/sat/samples/literal_sample_sat.cc
#include <stdlib.h>
#include "absl/base/log_severity.h"
#include "absl/log/globals.h"
#include "ortools/base/init_google.h"
#include "ortools/base/logging.h"
#include "absl/base/log_severity.h"
#include "absl/log/globals.h"
#include "ortools/sat/cp_model.h"
namespace operations_research {
@@ -69,17 +85,19 @@ int main(int argc, char* argv[]) {
operations_research::sat::LiteralSampleSat();
return EXIT_SUCCESS;
}
```
### Java code
```java
// Snippet from ortools/sat/samples/LiteralSampleSat.java
package com.google.ortools.sat.samples;
import com.google.ortools.Loader;
import com.google.ortools.sat.BoolVar;
import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.Literal;
import com.google.ortools.Loader;
/** Code sample to demonstrate Boolean variable and literals. */
public class LiteralSampleSat {
@@ -91,11 +109,15 @@ public class LiteralSampleSat {
System.out.println(notX);
}
}
```
### C\# code
```cs
```csharp
// Snippet from ortools/sat/samples/LiteralSampleSat.cs
using System;
using Google.OrTools.Sat;
@@ -108,11 +130,14 @@ public class LiteralSampleSat
ILiteral not_x = x.Not();
}
}
```
### Go code
```cs
```go
// Snippet from ortools/sat/samples/literal_sample_sat.go
// The literal_sample_sat command is a simple example of literals.
package main
@@ -133,6 +158,7 @@ func literalSampleSat() {
func main() {
literalSampleSat()
}
```
## Boolean constraints
@@ -150,6 +176,7 @@ constraints. For instance, we can add a constraint Or(x, not(y)).
### Python code
```python
# Snippet from ortools/sat/samples/bool_or_sample_sat.py
#!/usr/bin/env python3
"""Code sample to demonstrates a simple Boolean constraint."""
@@ -158,29 +185,33 @@ from ortools.sat.python import cp_model
def bool_or_sample_sat():
model = cp_model.CpModel()
model = cp_model.CpModel()
x = model.new_bool_var("x")
y = model.new_bool_var("y")
x = model.new_bool_var('x')
y = model.new_bool_var('y')
model.add_bool_or([x, y.negated()])
# The [] is not mandatory.
# ~y is equivalent to y.negated()
model.add_bool_or(x, ~y)
model.add_bool_or([x, y.negated()])
# The [] is not mandatory.
# ~y is equivalent to y.negated()
model.add_bool_or(x, ~y)
bool_or_sample_sat()
```
### C++ code
```cpp
// Snippet from ortools/sat/samples/bool_or_sample_sat.cc
#include <stdlib.h>
#include "ortools/base/init_google.h"
#include "absl/base/log_severity.h"
#include "absl/log/globals.h"
#include "absl/types/span.h"
#include "ortools/base/init_google.h"
#include "ortools/sat/cp_model.h"
namespace operations_research {
@@ -205,11 +236,15 @@ int main(int argc, char* argv[]) {
operations_research::sat::BoolOrSampleSat();
return EXIT_SUCCESS;
}
```
### Java code
```java
// Snippet from ortools/sat/samples/BoolOrSampleSat.java
package com.google.ortools.sat.samples;
import com.google.ortools.Loader;
@@ -227,11 +262,15 @@ public class BoolOrSampleSat {
model.addBoolOr(new Literal[] {x, y.not()});
}
}
```
### C\# code
```cs
```csharp
// Snippet from ortools/sat/samples/BoolOrSampleSat.cs
using System;
using Google.OrTools.Sat;
@@ -247,11 +286,15 @@ public class BoolOrSampleSat
model.AddBoolOr(new ILiteral[] { x, y.Not() });
}
}
```
### Go code
```cs
```go
// Snippet from ortools/sat/samples/bool_or_sample_sat.go
// The bool_or_sample_sat command is simple example of the BoolOr constraint.
package main
@@ -271,6 +314,7 @@ func boolOrSampleSat() {
func main() {
boolOrSampleSat()
}
```
## Reified constraints
@@ -278,12 +322,14 @@ func main() {
The CP-SAT solver supports *half-reified* constraints, also called
*implications*, which are of the form:
x implies constraint
```
x implies constraint
```
where the constraint must hold if `x` is true.
Please note that this is not an equivalence relation. The constraint can still
be true if `x` is false.
Note that this is not an equivalence relation. The constraint can still be true
if `x` is false.
So we can write b => And(x, not y). That is, if b is true, then x is true and y
is false. Note that in this particular example, there are multiple ways to
@@ -293,6 +339,7 @@ then is written as Or(not b, x) and Or(not b, not y).
### Python code
```python
# Snippet from ortools/sat/samples/reified_sample_sat.py
#!/usr/bin/env python3
"""Simple model with a reified constraint."""
@@ -300,37 +347,42 @@ from ortools.sat.python import cp_model
def reified_sample_sat():
"""Showcase creating a reified constraint."""
model = cp_model.CpModel()
"""Showcase creating a reified constraint."""
model = cp_model.CpModel()
x = model.new_bool_var("x")
y = model.new_bool_var("y")
b = model.new_bool_var("b")
x = model.new_bool_var('x')
y = model.new_bool_var('y')
b = model.new_bool_var('b')
# First version using a half-reified bool and.
model.add_bool_and(x, ~y).only_enforce_if(b)
# First version using a half-reified bool and.
model.add_bool_and(x, ~y).only_enforce_if(b)
# Second version using implications.
model.add_implication(b, x)
model.add_implication(b, ~y)
# Second version using implications.
model.add_implication(b, x)
model.add_implication(b, ~y)
# Third version using bool or.
model.add_bool_or(~b, x)
model.add_bool_or(~b, ~y)
# Third version using bool or.
model.add_bool_or(~b, x)
model.add_bool_or(~b, ~y)
reified_sample_sat()
```
### C++ code
```cpp
// Snippet from ortools/sat/samples/reified_sample_sat.cc
#include <stdlib.h>
#include "ortools/base/init_google.h"
#include "absl/base/log_severity.h"
#include "absl/log/globals.h"
#include "absl/types/span.h"
#include "ortools/base/init_google.h"
#include "ortools/sat/cp_model.h"
namespace operations_research {
@@ -364,11 +416,15 @@ int main(int argc, char* argv[]) {
operations_research::sat::ReifiedSampleSat();
return EXIT_SUCCESS;
}
```
### Java code
```java
// Snippet from ortools/sat/samples/ReifiedSampleSat.java
package com.google.ortools.sat.samples;
import com.google.ortools.Loader;
@@ -407,11 +463,15 @@ public class ReifiedSampleSat {
model.addBoolOr(new Literal[] {b.not(), y.not()});
}
}
```
### C\# code
```cs
```csharp
// Snippet from ortools/sat/samples/ReifiedSampleSat.cs
using System;
using Google.OrTools.Sat;
@@ -437,11 +497,15 @@ public class ReifiedSampleSat
model.AddBoolOr(new ILiteral[] { b.Not(), y.Not() });
}
}
```
### Go code
```cs
```go
// Snippet from ortools/sat/samples/reified_sample_sat.go
// The reified_sample_sat command is a simple example of implication constraints.
package main
@@ -471,29 +535,37 @@ func reifiedSampleSat() {
func main() {
reifiedSampleSat()
}
```
## Product of two Boolean Variables
A useful construct is the product `p` of two Boolean variables `x` and `y`.
p == x * y
```
p == x * y
```
This is equivalent to the logical relation
p <=> x and y
```
p <=> x and y
```
This is encoded using one bool_or constraint and two implications. The following
code samples output this truth table:
x = 0 y = 0 p = 0
x = 1 y = 0 p = 0
x = 0 y = 1 p = 0
x = 1 y = 1 p = 1
```
x = 0 y = 0 p = 0
x = 1 y = 0 p = 0
x = 0 y = 1 p = 0
x = 1 y = 1 p = 1
```
### Python code
```python
# Snippet from ortools/sat/samples/boolean_product_sample_sat.py
#!/usr/bin/env python3
"""Code sample that encodes the product of two Boolean variables."""
@@ -502,35 +574,39 @@ from ortools.sat.python import cp_model
def boolean_product_sample_sat():
"""Encoding of the product of two Boolean variables.
"""Encoding of the product of two Boolean variables.
p == x * y, which is the same as p <=> x and y
"""
model = cp_model.CpModel()
x = model.new_bool_var("x")
y = model.new_bool_var("y")
p = model.new_bool_var("p")
p == x * y, which is the same as p <=> x and y
"""
model = cp_model.CpModel()
x = model.new_bool_var('x')
y = model.new_bool_var('y')
p = model.new_bool_var('p')
# x and y implies p, rewrite as not(x and y) or p.
model.add_bool_or(~x, ~y, p)
# x and y implies p, rewrite as not(x and y) or p.
model.add_bool_or(~x, ~y, p)
# p implies x and y, expanded into two implications.
model.add_implication(p, x)
model.add_implication(p, y)
# p implies x and y, expanded into two implications.
model.add_implication(p, x)
model.add_implication(p, y)
# Create a solver and solve.
solver = cp_model.CpSolver()
solution_printer = cp_model.VarArraySolutionPrinter([x, y, p])
solver.parameters.enumerate_all_solutions = True
solver.solve(model, solution_printer)
# Create a solver and solve.
solver = cp_model.CpSolver()
solution_printer = cp_model.VarArraySolutionPrinter([x, y, p])
solver.parameters.enumerate_all_solutions = True
solver.solve(model, solution_printer)
boolean_product_sample_sat()
```
### Go code
```cs
```go
// Snippet from ortools/sat/samples/boolean_product_sample_sat.go
// The boolean_product_sample_sat command is a simple example of the product of two literals.
package main
@@ -538,9 +614,10 @@ import (
"fmt"
log "github.com/golang/glog"
"github.com/google/or-tools/ortools/sat/go/cpmodel"
sppb "github.com/google/or-tools/ortools/sat/proto/satparameters"
"google.golang.org/protobuf/proto"
"github.com/google/or-tools/ortools/sat/go/cpmodel"
sppb "github.com/google/or-tools/ortools/sat/proto/satparameters"
)
func booleanProductSample() error {
@@ -564,7 +641,7 @@ func booleanProductSample() error {
}
// Set `fill_additional_solutions_in_response` and `enumerate_all_solutions` to true so
// the solver returns all solutions found.
params := &sppb.SatParameters{
params := &sppb.SatParameters{
FillAdditionalSolutionsInResponse: proto.Bool(true),
EnumerateAllSolutions: proto.Bool(true),
SolutionPoolSize: proto.Int32(4),

648
ortools/sat/docs/integer_arithmetic.md
View File

File diff suppressed because it is too large Load Diff

141
ortools/sat/docs/model.md
View File

@@ -77,39 +77,37 @@ Some remarks:
### Python code
```python
#!/usr/bin/env python3
"""Code sample that solves a model using solution hinting."""
# Snippet from ortools/sat/samples/solution_hinting_sample_sat.py
from ortools.sat.python import cp_model
def solution_hinting_sample_sat():
"""Showcases solution hinting."""
# Creates the model.
model = cp_model.CpModel()
"""Showcases solution hinting."""
# Creates the model.
model = cp_model.CpModel()
# Creates the variables.
num_vals = 3
x = model.new_int_var(0, num_vals - 1, "x")
y = model.new_int_var(0, num_vals - 1, "y")
z = model.new_int_var(0, num_vals - 1, "z")
# Creates the variables.
num_vals = 3
x = model.new_int_var(0, num_vals - 1, 'x')
y = model.new_int_var(0, num_vals - 1, 'y')
z = model.new_int_var(0, num_vals - 1, 'z')
# Creates the constraints.
model.add(x != y)
# Creates the constraints.
model.add(x != y)
model.maximize(x + 2 * y + 3 * z)
model.maximize(x + 2 * y + 3 * z)
# Solution hinting: x <- 1, y <- 2
model.add_hint(x, 1)
model.add_hint(y, 2)
# Solution hinting: x <- 1, y <- 2
model.add_hint(x, 1)
model.add_hint(y, 2)
# Creates a solver and solves.
solver = cp_model.CpSolver()
solution_printer = cp_model.VarArrayAndObjectiveSolutionPrinter([x, y, z])
status = solver.solve(model, solution_printer)
# Creates a solver and solves.
solver = cp_model.CpSolver()
solution_printer = cp_model.VarArrayAndObjectiveSolutionPrinter([x, y, z])
status = solver.solve(model, solution_printer)
print(f"Status = {solver.status_name(status)}")
print(f"Number of solutions found: {solution_printer.solution_count}")
print(f'Status = {solver.status_name(status)}')
print(f'Number of solutions found: {solution_printer.solution_count}')
solution_hinting_sample_sat()
@@ -118,12 +116,13 @@ solution_hinting_sample_sat()
### C++ code
```cpp
// Snippet from ortools/sat/samples/solution_hinting_sample_sat.cc
#include <stdlib.h>
#include "absl/base/log_severity.h"
#include "absl/log/globals.h"
#include "ortools/base/init_google.h"
#include "ortools/base/logging.h"
#include "absl/base/log_severity.h"
#include "absl/log/globals.h"
#include "ortools/sat/cp_model.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_solver.h"
@@ -179,13 +178,14 @@ int main(int argc, char* argv[]) {
### Java code
```java
// Snippet from ortools/sat/samples/SolutionHintingSampleSat.java
package com.google.ortools.sat.samples;
import com.google.ortools.Loader;
import com.google.ortools.sat.CpSolverStatus;
import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.CpSolver;
import com.google.ortools.sat.CpSolverSolutionCallback;
import com.google.ortools.sat.CpSolverStatus;
import com.google.ortools.sat.IntVar;
import com.google.ortools.sat.LinearExpr;
@@ -242,7 +242,8 @@ public class SolutionHintingSampleSat {
### C\# code
```cs
```csharp
// Snippet from ortools/sat/samples/SolutionHintingSampleSat.cs
using System;
using Google.OrTools.Sat;
@@ -307,7 +308,7 @@ public class SolutionHintingSampleSat
### Go code
```cs
```go
// The solution_hinting_sample_sat command is an example of setting solution hints on the model.
package main
@@ -316,6 +317,7 @@ import (
log "github.com/golang/glog"
"github.com/google/or-tools/ortools/sat/go/cpmodel"
cmpb "github.com/google/or-tools/ortools/sat/proto/cpmodel"
)
@@ -360,6 +362,7 @@ func main() {
log.Exitf("solutionHintingSampleSat returned with error: %v", err)
}
}
```
## Model copy
@@ -375,58 +378,60 @@ The deep copy python mechanism relies on the
[`copy` Python Standard Library](https://docs.python.org/3/library/copy.html).
```python
#!/usr/bin/env python3
"""Showcases deep copying of a model."""
# Snippet from ortools/sat/samples/clone_model_sample_sat.py
import copy
from ortools.sat.python import cp_model
def clone_model_sample_sat():
"""Showcases cloning a model."""
# Creates the model.
model = cp_model.CpModel()
"""Showcases cloning a model."""
# Creates the model.
model = cp_model.CpModel()
# Creates the variables.
num_vals = 3
x = model.new_int_var(0, num_vals - 1, "x")
y = model.new_int_var(0, num_vals - 1, "y")
z = model.new_int_var(0, num_vals - 1, "z")
# Creates the variables.
num_vals = 3
x = model.new_int_var(0, num_vals - 1, 'x')
y = model.new_int_var(0, num_vals - 1, 'y')
z = model.new_int_var(0, num_vals - 1, 'z')
# Creates the constraints.
model.add(x != y)
# Creates the constraints.
model.add(x != y)
model.maximize(x + 2 * y + 3 * z)
model.maximize(x + 2 * y + 3 * z)
# Creates a solver and solves.
solver = cp_model.CpSolver()
status = solver.solve(model)
# Creates a solver and solves.
solver = cp_model.CpSolver()
status = solver.solve(model)
if status == cp_model.OPTIMAL:
print("Optimal value of the original model: {}".format(solver.objective_value))
if status == cp_model.OPTIMAL:
print(
'Optimal value of the original model: {}'.format(solver.objective_value)
)
# Creates a dictionary holding the model and the variables you want to use.
to_clone = {
"model": model,
"x": x,
"y": y,
"z": z,
}
# Creates a dictionary holding the model and the variables you want to use.
to_clone = {
'model': model,
'x': x,
'y': y,
'z': z,
}
# Deep copy the dictionary.
clone = copy.deepcopy(to_clone)
# Deep copy the dictionary.
clone = copy.deepcopy(to_clone)
# Retrieve the cloned model and variables.
cloned_model: cp_model.CpModel = clone["model"]
cloned_x = clone["x"]
cloned_y = clone["y"]
cloned_model.add(cloned_x + cloned_y <= 1)
# Retrieve the cloned model and variables.
cloned_model: cp_model.CpModel = clone['model']
cloned_x = clone['x']
cloned_y = clone['y']
cloned_model.add(cloned_x + cloned_y <= 1)
status = solver.solve(cloned_model)
status = solver.solve(cloned_model)
if status == cp_model.OPTIMAL:
print("Optimal value of the modified model: {}".format(solver.objective_value))
if status == cp_model.OPTIMAL:
print(
'Optimal value of the modified model: {}'.format(solver.objective_value)
)
clone_model_sample_sat()
@@ -435,12 +440,13 @@ clone_model_sample_sat()
### C++ code
```cpp
// Snippet from ortools/sat/samples/clone_model_sample_sat.cc
#include <stdlib.h>
#include "absl/base/log_severity.h"
#include "absl/log/globals.h"
#include "ortools/base/init_google.h"
#include "ortools/base/logging.h"
#include "absl/base/log_severity.h"
#include "absl/log/globals.h"
#include "ortools/sat/cp_model.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_solver.h"
@@ -492,12 +498,13 @@ int main(int argc, char* argv[]) {
### Java code
```java
// Snippet from ortools/sat/samples/CloneModelSampleSat.java
package com.google.ortools.sat.samples;
import com.google.ortools.Loader;
import com.google.ortools.sat.CpSolverStatus;
import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.CpSolver;
import com.google.ortools.sat.CpSolverStatus;
import com.google.ortools.sat.IntVar;
import com.google.ortools.sat.LinearExpr;

7
ortools/sat/integer_base.cc
View File

@@ -119,7 +119,12 @@ bool LinearExpression2::IsCanonicalized() const {
return false;
}
}
if (vars[0] >= vars[1]) return false;
if (vars[0] >= vars[1]) {
if (vars[0] == kNoIntegerVariable && vars[1] == kNoIntegerVariable) {
return true;
}
return false;
}
if (vars[0] == kNoIntegerVariable) return true;

4
ortools/sat/integer_base.h
View File

@@ -358,7 +358,9 @@ H AbslHashValue(H h, const AffineExpression& e) {
// A linear expression with at most two variables (coeffs can be zero).
// And some utility to canonicalize them.
struct LinearExpression2 {
// Construct a zero expression.
LinearExpression2() = default;
LinearExpression2(IntegerVariable v1, IntegerVariable v2, IntegerValue c1,
IntegerValue c2) {
vars[0] = v1;
@@ -428,7 +430,7 @@ struct LinearExpression2 {
}
IntegerValue coeffs[2];
IntegerVariable vars[2];
IntegerVariable vars[2] = {kNoIntegerVariable, kNoIntegerVariable};
template <typename Sink>
friend void AbslStringify(Sink& sink, const LinearExpression2& expr) {

4
ortools/sat/integer_base_test.cc
View File

@@ -15,6 +15,7 @@
#include <utility>
#include "absl/log/check.h"
#include "gtest/gtest.h"
namespace operations_research::sat {
@@ -22,6 +23,7 @@ namespace {
TEST(CanonicalizeAffinePrecedenceTest, Basic) {
LinearExpression2 expr;
CHECK(expr.IsCanonicalized()) << expr;
expr.vars[0] = IntegerVariable(0);
expr.vars[1] = IntegerVariable(2);
expr.coeffs[0] = IntegerValue(4);
@@ -30,6 +32,7 @@ TEST(CanonicalizeAffinePrecedenceTest, Basic) {
IntegerValue lb(0);
IntegerValue ub(11);
expr.CanonicalizeAndUpdateBounds(lb, ub);
CHECK(expr.IsCanonicalized());
EXPECT_EQ(expr.vars[0], IntegerVariable(0));
EXPECT_EQ(expr.vars[1], IntegerVariable(2));
@@ -47,6 +50,7 @@ TEST(CanonicalizeAffinePrecedenceTest, OneSingleVariable) {
expr.coeffs[1] = IntegerValue(2);
expr.SimpleCanonicalization();
CHECK(expr.IsCanonicalized());
EXPECT_EQ(expr.vars[0], kNoIntegerVariable);
EXPECT_EQ(expr.vars[1], IntegerVariable(0));

10
ortools/sat/intervals.cc
View File

@@ -183,12 +183,12 @@ IntervalsRepository::GetOrCreateDisjunctivePrecedenceLiteralIfNonTrivial(
if (enforcement_literals.empty()) {
const auto [expr_a_before_b, ub_a_before_b] =
EncodeDifferenceLowerThan(a.end, b.start, 0);
reified_precedences_->AddReifiedBoundIfNonTrivial(
reified_precedences_->AddBoundEncodingIfNonTrivial(
a_before_b, expr_a_before_b, ub_a_before_b);
const auto [expr_b_before_a, ub_b_before_a] =
EncodeDifferenceLowerThan(b.end, a.start, 0);
reified_precedences_->AddReifiedBoundIfNonTrivial(
reified_precedences_->AddBoundEncodingIfNonTrivial(
a_before_b.Negated(), expr_b_before_a, ub_b_before_a);
}
@@ -218,7 +218,7 @@ IntervalsRepository::GetOrCreateDisjunctivePrecedenceLiteralIfNonTrivial(
bool IntervalsRepository::CreatePrecedenceLiteralIfNonTrivial(
AffineExpression x, AffineExpression y) {
const auto [expr, ub] = EncodeDifferenceLowerThan(x, y, 0);
const LiteralIndex index = reified_precedences_->GetReifiedBound(expr, ub);
const LiteralIndex index = reified_precedences_->GetEncodedBound(expr, ub);
if (index != kNoLiteralIndex) return false;
// We want l => x <= y and not(l) => x > y <=> y + 1 <= x
@@ -231,7 +231,7 @@ bool IntervalsRepository::CreatePrecedenceLiteralIfNonTrivial(
// Create a new literal.
const BooleanVariable boolean_var = sat_solver_->NewBooleanVariable();
const Literal x_before_y = Literal(boolean_var, true);
reified_precedences_->AddReifiedBoundIfNonTrivial(x_before_y, expr, ub);
reified_precedences_->AddBoundEncodingIfNonTrivial(x_before_y, expr, ub);
AffineExpression y_plus_one = y;
y_plus_one.constant += 1;
@@ -243,7 +243,7 @@ bool IntervalsRepository::CreatePrecedenceLiteralIfNonTrivial(
LiteralIndex IntervalsRepository::GetPrecedenceLiteral(
AffineExpression x, AffineExpression y) const {
const auto [expr, ub] = EncodeDifferenceLowerThan(x, y, 0);
return reified_precedences_->GetReifiedBound(expr, ub);
return reified_precedences_->GetEncodedBound(expr, ub);
}
Literal IntervalsRepository::GetOrCreatePrecedenceLiteral(AffineExpression x,

52
ortools/sat/precedences.cc
View File

@@ -1093,7 +1093,8 @@ int GreaterThanAtLeastOneOfDetector::AddGreaterThanAtLeastOneOfConstraints(
ReifiedLinear2Bounds::ReifiedLinear2Bounds(Model* model)
: integer_encoder_(model->GetOrCreate<IntegerEncoder>()),
best_root_level_bounds_(model->GetOrCreate<RootLevelLinear2Bounds>()) {
best_root_level_bounds_(model->GetOrCreate<RootLevelLinear2Bounds>()),
lin2_indices_(model->GetOrCreate<Linear2Indices>()) {
int index = 0;
model->GetOrCreate<LevelZeroCallbackHelper>()->callbacks.push_back(
[index = index, trail = model->GetOrCreate<Trail>(), this]() mutable {
@@ -1108,14 +1109,16 @@ ReifiedLinear2Bounds::ReifiedLinear2Bounds(Model* model)
if (relevant_true_literals.empty()) return true;
// Linear scan.
for (const auto [l, expr, ub] : all_reified_relations_) {
for (const auto [l, expr_index, ub] : all_reified_relations_) {
if (relevant_true_literals.contains(l)) {
best_root_level_bounds_->AddUpperBound(expr, ub);
VLOG(2) << "New fixed precedence: " << expr << " <= " << ub
best_root_level_bounds_->AddUpperBound(expr_index, ub);
VLOG(2) << "New fixed precedence: "
<< lin2_indices_->GetExpression(expr_index) << " <= " << ub
<< " (was reified by " << l << ")";
} else if (relevant_true_literals.contains(l.Negated())) {
best_root_level_bounds_->AddLowerBound(expr, ub + 1);
VLOG(2) << "New fixed precedence: " << expr << " > " << ub
best_root_level_bounds_->AddLowerBound(expr_index, ub + 1);
VLOG(2) << "New fixed precedence: "
<< lin2_indices_->GetExpression(expr_index) << " > " << ub
<< " (was reified by not(" << l << "))";
}
}
@@ -1138,20 +1141,35 @@ RelationStatus ReifiedLinear2Bounds::GetLevelZeroPrecedenceStatus(
ub);
}
void ReifiedLinear2Bounds::AddReifiedBoundIfNonTrivial(Literal l,
LinearExpression2 expr,
IntegerValue ub) {
void ReifiedLinear2Bounds::AddBoundEncodingIfNonTrivial(Literal l,
LinearExpression2 expr,
IntegerValue ub) {
DCHECK(expr.IsCanonicalized());
DCHECK_EQ(expr.DivideByGcd(), 1);
const RelationStatus status =
best_root_level_bounds_->GetLevelZeroStatus(expr, kMinIntegerValue, ub);
if (status != RelationStatus::IS_UNKNOWN) return;
relation_to_lit_.insert({{expr, ub}, l});
if (expr.vars[0] == kNoIntegerVariable) {
// We checked for IS_UNKNOWN above, which is not possible for constant
// linear2.
DCHECK_NE(expr.vars[1], kNoIntegerVariable);
DCHECK_EQ(expr.coeffs[1], 1);
integer_encoder_->AssociateToIntegerLiteral(
l, IntegerLiteral::LowerOrEqual(expr.vars[1], ub));
return;
}
const LinearExpression2Index expr_index = lin2_indices_->AddOrGet(expr);
relation_to_lit_.insert({{expr_index, ub}, l});
variable_appearing_in_reified_relations_.insert(l.Variable());
all_reified_relations_.push_back({l, expr, ub});
all_reified_relations_.push_back({l, expr_index, ub});
}
LiteralIndex ReifiedLinear2Bounds::GetReifiedBound(LinearExpression2 expr,
LiteralIndex ReifiedLinear2Bounds::GetEncodedBound(LinearExpression2 expr,
IntegerValue ub) {
DCHECK(expr.IsCanonicalized());
DCHECK_EQ(expr.DivideByGcd(), 1);
const RelationStatus status =
best_root_level_bounds_->GetLevelZeroStatus(expr, kMinIntegerValue, ub);
if (status == RelationStatus::IS_TRUE) {
@@ -1160,8 +1178,16 @@ LiteralIndex ReifiedLinear2Bounds::GetReifiedBound(LinearExpression2 expr,
if (status == RelationStatus::IS_FALSE) {
return integer_encoder_->GetFalseLiteral().Index();
}
if (expr.vars[0] == kNoIntegerVariable) {
DCHECK_NE(expr.vars[1], kNoIntegerVariable);
DCHECK_EQ(expr.coeffs[1], 1);
return integer_encoder_->GetAssociatedLiteral(
IntegerLiteral::LowerOrEqual(expr.vars[1], ub));
}
const auto it = relation_to_lit_.find({expr, ub});
const LinearExpression2Index expr_index = lin2_indices_->GetIndex(expr);
if (expr_index == kNoLinearExpression2Index) return kNoLiteralIndex;
const auto it = relation_to_lit_.find({expr_index, ub});
if (it == relation_to_lit_.end()) return kNoLiteralIndex;
return it->second;
}

17
ortools/sat/precedences.h
View File

@@ -188,6 +188,10 @@ class RootLevelLinear2Bounds {
return AddUpperBound(expr, -lb);
}
bool AddLowerBound(LinearExpression2Index index, IntegerValue lb) {
return AddUpperBound(NegationOf(index), -lb);
}
// All modifications go through this function.
bool AddUpperBound(LinearExpression2Index index, IntegerValue ub);
@@ -615,21 +619,24 @@ class ReifiedLinear2Bounds {
AffineExpression b) const;
// Register the fact that l <=> ( expr <= ub ).
// `expr` must already be canonicalized and gcd-reduced.
// These are considered equivalence relation.
void AddReifiedBoundIfNonTrivial(Literal l, LinearExpression2 expr,
IntegerValue ub);
void AddBoundEncodingIfNonTrivial(Literal l, LinearExpression2 expr,
IntegerValue ub);
// Returns kNoLiteralIndex if we don't have a literal <=> ( expr <= ub ), or
// returns that literal if we have one. Note that we will return the
// true/false literal if the status is known at level zero.
LiteralIndex GetReifiedBound(LinearExpression2 expr, IntegerValue ub);
// `expr` must be canonicalized and gcd-reduced.
LiteralIndex GetEncodedBound(LinearExpression2 expr, IntegerValue ub);
private:
IntegerEncoder* integer_encoder_;
RootLevelLinear2Bounds* best_root_level_bounds_;
Linear2Indices* lin2_indices_;
// This stores relations l <=> (linear2 <= rhs).
absl::flat_hash_map<std::pair<LinearExpression2, IntegerValue>, Literal>
absl::flat_hash_map<std::pair<LinearExpression2Index, IntegerValue>, Literal>
relation_to_lit_;
// This is used to detect relations that become fixed at level zero and
@@ -637,7 +644,7 @@ class ReifiedLinear2Bounds {
// we fix variable, a linear scan shouldn't be too bad and is relatively
// compact memory wise.
absl::flat_hash_set<BooleanVariable> variable_appearing_in_reified_relations_;
std::vector<std::tuple<Literal, LinearExpression2, IntegerValue>>
std::vector<std::tuple<Literal, LinearExpression2Index, IntegerValue>>
all_reified_relations_;
};

21
ortools/sat/python/cp_model_helper_test.py
View File

@@ -356,6 +356,27 @@ class CpModelHelperTest(absltest.TestCase):
self.assertFalse(e12.is_integer())
self.assertEqual(str(e12), "(3.1 * (x + 2))")
def test_large_lin_expr(self):
model = cmh.CpModelProto()
all_records = range(4)
decision_var = []
for r in all_records:
decision_var.append(
[
cmh.IntVar(model).with_name(f"x{r}0"),
cmh.IntVar(model).with_name(f"x{r}1"),
cmh.IntVar(model).with_name(f"x{r}2"),
]
)
expr = sum(
(decision_var[r][1] + decision_var[r][2]) * 2
+ (decision_var[r][0] + decision_var[r][2]) * 3
+ (decision_var[r][0] + decision_var[r][1]) * 4
for r in all_records
)
print(expr, expr == 2)
class CpModelBuilderTest(absltest.TestCase):