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

improve CP-SAT diffn; add 2 more examples to CP-SAT cookbook; internal cleanup and improvements

Browse Source
This commit is contained in:
Laurent Perron
2019-03-25 11:26:14 +01:00
parent 0b4cd18625
commit e81e12ec45
23 changed files with 1715 additions and 86 deletions
Download Patch File Download Diff File Expand all files Collapse all files

18
makefiles/Makefile.gen.mk
View File

@@ -166,7 +166,8 @@ objs/util/cached_log.$O: ortools/util/cached_log.cc \
objs/util/file_util.$O: ortools/util/file_util.cc ortools/util/file_util.h \
ortools/base/file.h ortools/base/integral_types.h ortools/base/logging.h \
ortools/base/macros.h ortools/base/status.h ortools/base/recordio.h | $(OBJ_DIR)/util
ortools/base/macros.h ortools/base/status.h ortools/base/recordio.h \
ortools/base/statusor.h | $(OBJ_DIR)/util
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Sutil$Sfile_util.cc $(OBJ_OUT)$(OBJ_DIR)$Sutil$Sfile_util.$O
objs/util/fp_utils.$O: ortools/util/fp_utils.cc ortools/util/fp_utils.h \
@@ -480,7 +481,7 @@ objs/lp_data/model_reader.$O: ortools/lp_data/model_reader.cc \
ortools/util/fp_utils.h ortools/base/file.h ortools/base/status.h \
ortools/lp_data/mps_reader.h ortools/base/commandlineflags.h \
ortools/base/map_util.h ortools/lp_data/proto_utils.h \
ortools/util/file_util.h ortools/base/recordio.h | $(OBJ_DIR)/lp_data
ortools/util/file_util.h ortools/base/recordio.h ortools/base/statusor.h | $(OBJ_DIR)/lp_data
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Slp_data$Smodel_reader.cc $(OBJ_OUT)$(OBJ_DIR)$Slp_data$Smodel_reader.$O
objs/lp_data/mps_reader.$O: ortools/lp_data/mps_reader.cc \
@@ -666,7 +667,8 @@ objs/glop/lp_solver.$O: ortools/glop/lp_solver.cc ortools/glop/lp_solver.h \
ortools/lp_data/matrix_scaler.h ortools/lp_data/proto_utils.h \
ortools/gen/ortools/linear_solver/linear_solver.pb.h \
ortools/gen/ortools/util/optional_boolean.pb.h ortools/util/file_util.h \
ortools/base/file.h ortools/base/status.h ortools/base/recordio.h | $(OBJ_DIR)/glop
ortools/base/file.h ortools/base/status.h ortools/base/recordio.h \
ortools/base/statusor.h | $(OBJ_DIR)/glop
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Sglop$Slp_solver.cc $(OBJ_OUT)$(OBJ_DIR)$Sglop$Slp_solver.$O
objs/glop/lu_factorization.$O: ortools/glop/lu_factorization.cc \
@@ -1548,7 +1550,7 @@ objs/sat/diffn.$O: ortools/sat/diffn.cc ortools/sat/diffn.h \
ortools/sat/intervals.h ortools/sat/cp_constraints.h \
ortools/sat/integer_expr.h ortools/sat/precedences.h \
ortools/sat/theta_tree.h ortools/base/iterator_adaptors.h \
ortools/util/sort.h | $(OBJ_DIR)/sat
ortools/sat/cumulative.h ortools/util/sort.h | $(OBJ_DIR)/sat
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Ssat$Sdiffn.cc $(OBJ_OUT)$(OBJ_DIR)$Ssat$Sdiffn.$O
objs/sat/disjunctive.$O: ortools/sat/disjunctive.cc \
@@ -3340,13 +3342,13 @@ objs/constraint_solver/routing_parameters.$O: \
$(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Sconstraint_solver$Srouting_parameters.cc $(OBJ_OUT)$(OBJ_DIR)$Sconstraint_solver$Srouting_parameters.$O
objs/constraint_solver/routing_search.$O: \
ortools/constraint_solver/routing_search.cc ortools/base/small_map.h \
ortools/constraint_solver/routing_search.cc ortools/base/map_util.h \
ortools/base/logging.h ortools/base/integral_types.h \
ortools/base/macros.h ortools/base/small_map.h \
ortools/base/small_ordered_set.h ortools/base/stl_util.h \
ortools/base/integral_types.h ortools/base/macros.h \
ortools/constraint_solver/constraint_solveri.h \
ortools/base/commandlineflags.h ortools/base/hash.h \
ortools/base/basictypes.h ortools/base/logging.h ortools/base/map_util.h \
ortools/base/sysinfo.h ortools/base/timer.h \
ortools/base/basictypes.h ortools/base/sysinfo.h ortools/base/timer.h \
ortools/constraint_solver/constraint_solver.h ortools/base/random.h \
ortools/gen/ortools/constraint_solver/solver_parameters.pb.h \
ortools/util/piecewise_linear_function.h \

1
ortools/sat/BUILD
View File

@@ -944,6 +944,7 @@ cc_library(
srcs = ["diffn.cc"],
hdrs = ["diffn.h"],
deps = [
":cumulative",
":disjunctive",
":integer",
":intervals",

44
ortools/sat/cp_model_loader.cc
View File

@@ -753,50 +753,6 @@ void LoadNoOverlap2dConstraint(const ConstraintProto& ct, Model* m) {
const std::vector<IntervalVariable> y_intervals =
mapping->Intervals(ct.no_overlap_2d().y_intervals());
m->Add(StrictNonOverlappingRectangles(x_intervals, y_intervals));
// Add a cumulative relaxation. That is, on one direction, you do not enforce
// the rectangle aspect, allowing slices to move freely.
auto add_cumulative = [m](const std::vector<IntervalVariable>& x,
const std::vector<IntervalVariable>& y) {
IntervalsRepository* const repository =
m->GetOrCreate<IntervalsRepository>();
std::vector<IntegerVariable> starts;
std::vector<IntegerVariable> sizes;
std::vector<IntegerVariable> ends;
int64 min_starts = kint64max;
int64 max_ends = kint64min;
for (const IntervalVariable& interval : y) {
starts.push_back(repository->StartVar(interval));
IntegerVariable s_var = repository->SizeVar(interval);
if (s_var == kNoIntegerVariable) {
s_var = m->Add(
ConstantIntegerVariable(repository->MinSize(interval).value()));
}
sizes.push_back(s_var);
ends.push_back(repository->EndVar(interval));
min_starts = std::min(min_starts, m->Get(LowerBound(starts.back())));
max_ends = std::max(max_ends, m->Get(UpperBound(ends.back())));
}
const IntegerVariable min_start_var =
m->Add(NewIntegerVariable(min_starts, max_ends));
m->Add(IsEqualToMinOf(min_start_var, starts));
const IntegerVariable max_end_var =
m->Add(NewIntegerVariable(min_starts, max_ends));
m->Add(IsEqualToMaxOf(max_end_var, ends));
const IntegerVariable capacity =
m->Add(NewIntegerVariable(0, CapSub(max_ends, min_starts)));
const std::vector<int64> coeffs = {-1, -1, 1};
m->Add(WeightedSumGreaterOrEqual({capacity, min_start_var, max_end_var},
coeffs, 0));
m->Add(Cumulative(x, sizes, capacity));
};
add_cumulative(x_intervals, y_intervals);
add_cumulative(y_intervals, x_intervals);
}
void LoadCumulativeConstraint(const ConstraintProto& ct, Model* m) {

126
ortools/sat/diffn.cc
View File

@@ -19,6 +19,7 @@
#include "absl/strings/str_join.h"
#include "ortools/base/iterator_adaptors.h"
#include "ortools/base/map_util.h"
#include "ortools/sat/cumulative.h"
#include "ortools/sat/disjunctive.h"
#include "ortools/sat/intervals.h"
#include "ortools/sat/sat_solver.h"
@@ -28,6 +29,47 @@
namespace operations_research {
namespace sat {
void AddCumulativeRelaxation(const std::vector<IntervalVariable>& x,
const std::vector<IntervalVariable>& y,
Model* model) {
IntervalsRepository* const repository =
model->GetOrCreate<IntervalsRepository>();
std::vector<IntegerVariable> starts;
std::vector<IntegerVariable> sizes;
std::vector<IntegerVariable> ends;
int64 min_starts = kint64max;
int64 max_ends = kint64min;
for (const IntervalVariable& interval : y) {
starts.push_back(repository->StartVar(interval));
IntegerVariable s_var = repository->SizeVar(interval);
if (s_var == kNoIntegerVariable) {
s_var = model->Add(
ConstantIntegerVariable(repository->MinSize(interval).value()));
}
sizes.push_back(s_var);
ends.push_back(repository->EndVar(interval));
min_starts = std::min(min_starts, model->Get(LowerBound(starts.back())));
max_ends = std::max(max_ends, model->Get(UpperBound(ends.back())));
}
const IntegerVariable min_start_var =
model->Add(NewIntegerVariable(min_starts, max_ends));
model->Add(IsEqualToMinOf(min_start_var, starts));
const IntegerVariable max_end_var =
model->Add(NewIntegerVariable(min_starts, max_ends));
model->Add(IsEqualToMaxOf(max_end_var, ends));
const IntegerVariable capacity =
model->Add(NewIntegerVariable(0, CapSub(max_ends, min_starts)));
const std::vector<int64> coeffs = {-1, -1, 1};
model->Add(WeightedSumGreaterOrEqual({capacity, min_start_var, max_end_var},
coeffs, 0));
model->Add(Cumulative(x, sizes, capacity));
}
#define RETURN_IF_FALSE(f) \
if (!(f)) return false;
@@ -79,6 +121,37 @@ IntegerValue NonOverlappingRectanglesBasePropagator::FindCanonicalValue(
return candidate;
}
std::vector<std::vector<int>>
NonOverlappingRectanglesBasePropagator::SplitDisjointBoxes(
std::vector<int> boxes, SchedulingConstraintHelper* x_dim) {
std::vector<std::vector<int>> result(1);
std::sort(boxes.begin(), boxes.end(), [x_dim](int a, int b) {
return x_dim->StartMin(a) < x_dim->StartMin(b);
});
result.back().push_back(boxes[0]);
IntegerValue current_max_end = x_dim->EndMax(boxes[0]);
for (int b = 1; b < boxes.size(); ++b) {
const int box = boxes[b];
if (x_dim->StartMin(box) < current_max_end) {
// Merge.
result.back().push_back(box);
current_max_end = std::max(current_max_end, x_dim->EndMax(box));
} else {
if (result.back().size() == 1) {
// Overwrite
result.back().clear();
} else {
result.push_back(std::vector<int>());
}
result.back().push_back(box);
current_max_end = x_dim->EndMax(box);
}
}
return result;
}
bool NonOverlappingRectanglesBasePropagator::
FindBoxesThatMustOverlapAHorizontalLineAndPropagate(
SchedulingConstraintHelper* x_dim, SchedulingConstraintHelper* y_dim,
@@ -97,7 +170,7 @@ bool NonOverlappingRectanglesBasePropagator::
std::vector<int> active_boxes;
for (int box = 0; box < num_boxes_; ++box) {
if (cached_areas_[box] == 0) continue;
if (cached_areas_[box] == 0 && !strict_) continue;
const IntegerValue start_max = y_dim->StartMax(box);
const IntegerValue end_min = y_dim->EndMin(box);
if (start_max < end_min) {
@@ -145,8 +218,19 @@ bool NonOverlappingRectanglesBasePropagator::
event_to_overlapping_boxes.erase(event);
}
std::set<std::vector<int>> reduced_overlapping_boxes;
for (const auto& it : event_to_overlapping_boxes) {
const std::vector<int>& boxes = it.second;
std::vector<std::vector<int>> disjoint_boxes =
SplitDisjointBoxes(it.second, x_dim);
for (std::vector<int>& sub_boxes : disjoint_boxes) {
if (sub_boxes.size() > 1) {
std::sort(sub_boxes.begin(), sub_boxes.end());
reduced_overlapping_boxes.insert(sub_boxes);
}
}
}
for (const std::vector<int>& boxes : reduced_overlapping_boxes) {
// Collect the common overlapping coordinates of all boxes.
IntegerValue lb(kint64min);
IntegerValue ub(kint64max);
@@ -189,9 +273,26 @@ NonOverlappingRectanglesEnergyPropagator::
bool NonOverlappingRectanglesEnergyPropagator::Propagate() {
FillCachedAreas();
std::vector<int> all_boxes;
for (int box = 0; box < num_boxes_; ++box) {
if (cached_areas_[box] == 0) continue;
RETURN_IF_FALSE(FailWhenEnergyIsTooLarge(box));
all_boxes.push_back(box);
}
if (all_boxes.empty()) return true;
const std::vector<std::vector<int>> x_split =
SplitDisjointBoxes(all_boxes, &x_);
for (const std::vector<int>& x_boxes : x_split) {
if (x_boxes.size() <= 1) continue;
const std::vector<std::vector<int>> y_split =
SplitDisjointBoxes(x_boxes, &y_);
for (const std::vector<int>& y_boxes : y_split) {
if (y_boxes.size() <= 1) continue;
for (const int box : y_boxes) {
RETURN_IF_FALSE(FailWhenEnergyIsTooLarge(box, y_boxes));
}
}
}
return true;
@@ -205,20 +306,21 @@ void NonOverlappingRectanglesEnergyPropagator::RegisterWith(
watcher->SetPropagatorPriority(id, 2);
}
void NonOverlappingRectanglesEnergyPropagator::SortNeighbors(int box) {
void NonOverlappingRectanglesEnergyPropagator::SortNeighbors(
int box, const std::vector<int>& local_boxes) {
auto max_span = [](IntegerValue min_a, IntegerValue max_a, IntegerValue min_b,
IntegerValue max_b) {
return std::max(max_a, max_b) - std::min(min_a, min_b) + 1;
};
cached_distance_to_bounding_box_.resize(num_boxes_);
cached_distance_to_bounding_box_.assign(num_boxes_, IntegerValue(0));
neighbors_.clear();
const IntegerValue box_x_min = x_.StartMin(box);
const IntegerValue box_x_max = x_.EndMax(box);
const IntegerValue box_y_min = y_.StartMin(box);
const IntegerValue box_y_max = y_.EndMax(box);
for (int other_box = 0; other_box < num_boxes_; ++other_box) {
for (const int other_box : local_boxes) {
if (other_box == box) continue;
if (cached_areas_[other_box] == 0) continue;
@@ -239,10 +341,10 @@ void NonOverlappingRectanglesEnergyPropagator::SortNeighbors(int box) {
}
bool NonOverlappingRectanglesEnergyPropagator::FailWhenEnergyIsTooLarge(
int box) {
int box, const std::vector<int>& local_boxes) {
// Note that we only consider the smallest dimension of each boxes here.
SortNeighbors(box);
SortNeighbors(box, local_boxes);
IntegerValue area_min_x = x_.StartMin(box);
IntegerValue area_max_x = x_.EndMax(box);
IntegerValue area_min_y = y_.StartMin(box);
@@ -268,14 +370,6 @@ bool NonOverlappingRectanglesEnergyPropagator::FailWhenEnergyIsTooLarge(
const int other_box = neighbors_[i];
CHECK_GT(cached_areas_[other_box], 0);
if (x_.StartMin(other_box) >= area_max_x ||
x_.EndMax(other_box) <= area_min_x ||
y_.StartMin(other_box) >= area_max_y ||
y_.EndMax(other_box) <= area_min_y) {
// Strictly disjoint from the current bounding box. Let's stop here.
return true;
}
// Update Bounding box.
area_min_x = std::min(area_min_x, x_.StartMin(other_box));
area_max_x = std::max(area_max_x, x_.EndMax(other_box));

19
ortools/sat/diffn.h
View File

@@ -47,6 +47,8 @@ class NonOverlappingRectanglesBasePropagator : public PropagatorInterface {
bool FindBoxesThatMustOverlapAHorizontalLineAndPropagate(
SchedulingConstraintHelper* x_dim, SchedulingConstraintHelper* y_dim,
std::function<bool(const std::vector<int>& boxes)> inner_propagate);
std::vector<std::vector<int>> SplitDisjointBoxes(
std::vector<int> boxes, SchedulingConstraintHelper* x_dim);
const int num_boxes_;
SchedulingConstraintHelper x_;
@@ -76,8 +78,8 @@ class NonOverlappingRectanglesEnergyPropagator
void RegisterWith(GenericLiteralWatcher* watcher);
private:
void SortNeighbors(int box);
bool FailWhenEnergyIsTooLarge(int box);
void SortNeighbors(int box, const std::vector<int>& local_boxes);
bool FailWhenEnergyIsTooLarge(int box, const std::vector<int>& local_boxes);
std::vector<int> neighbors_;
std::vector<IntegerValue> cached_distance_to_bounding_box_;
@@ -145,6 +147,12 @@ class NonOverlappingRectanglesSlowPropagator
DISALLOW_COPY_AND_ASSIGN(NonOverlappingRectanglesSlowPropagator);
};
// Add a cumulative relaxation. That is, on one direction, it does not enforce
// the rectangle aspect, allowing vertical slices to move freely.
void AddCumulativeRelaxation(const std::vector<IntervalVariable>& x,
const std::vector<IntervalVariable>& y,
Model* model);
// Enforces that the boxes with corners in (x, y), (x + dx, y), (x, y + dy)
// and (x + dx, y + dy) do not overlap.
// If one box has a zero dimension, then it can be placed anywhere.
@@ -169,7 +177,11 @@ inline std::function<void(Model*)> NonOverlappingRectangles(
new NonOverlappingRectanglesSlowPropagator(
x, y, false, model, model->GetOrCreate<IntegerTrail>());
slow_constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
model->TakeOwnership(slow_constraint);
AddCumulativeRelaxation(x, y, model);
AddCumulativeRelaxation(y, x, model);
};
}
@@ -198,6 +210,9 @@ inline std::function<void(Model*)> StrictNonOverlappingRectangles(
x, y, true, model, model->GetOrCreate<IntegerTrail>());
slow_constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
model->TakeOwnership(slow_constraint);
AddCumulativeRelaxation(x, y, model);
AddCumulativeRelaxation(y, x, model);
};
}

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

@@ -12,17 +12,34 @@ The CP-SAT solver can express integer variables and constraints.
## Integer variables
Integer variables are discrete variables ranging over 64 bit signed integer
values. When creating them, a domain must be given. The format of this domain is
a flattened list of disjoint intervals.
Integer variables can take on 64 bit signed integer values. When creating them,
a domain must be given. The format of this domain is not uniform across languages.
- To represent a interval from 0 to 10, just pass a domain [0, 10].
- To represent a single value (5), create a domain [5, 5].
- From these, it is easy to represent an enumerated list of values [-5, -4,
-3, 1, 3, 4, 5, 6] is encoded as [-5, -3, 1, 1, 3, 6].
In Java, Python, and C#:
- To represent a interval from 0 to 10, just pass the two bounds (0, 10) as in
`NewIntVar(0, 10, "x")`. A single value will be represented by twice the
value as in [5, 5].
- To create a fixed variable (constant), use the `NewConstant()` API.
- To represent an enumerated list of values, for example {-5, -4, -3, 1, 3, 4,
5, 6}, you need to rewrite it as a list of intervals [-5, -3] U [1] U [3,
6], then flatten the list into a single list of integers. This gives `[-5,
-3, 1, 1, 3, 6]` in python, or `new long[] {-5, -3, 1, 1, 3, 6}` in Java or
C#.
- To exclude a single value, use int64min and int64max values as in [int64min,
4, 6, int64max].
In C++, domains use the Domain class.
- To represent a interval from 0 to 10, just pass a domain `{0, 10}` or
`Domain(0, 10)` as in `NewIntVar({0, 10})`.
- To represent a single value (5), create a domain `{5, 5}` or `Domain(5)`.
- To create a fixed variable (constant), use the `NewConstant()` API.
- To represent an enumerated list of values, for instance {-5, -4, -3, 1, 3,
4, 5, 6}, you can use `Domain::FromValues({-5, -4, -3, 1, 3, 4, 5, 6})` or
`Domain::FromIntervals({{-5, -3}, {1, 1}, {3, 6}})`.
- To exclude a single value, use `Domain(5).Complement()`.
## Linear constraints
In **C++** and **Java**, the model supports linear constraints as in:
@@ -31,18 +48,21 @@ In **C++** and **Java**, the model supports linear constraints as in:
as well as domain constraints as in:
sum(ai * xi) in domain
sum(ai * xi) in domain
Where domain uses the same encoding as integer variables.
where domain uses the same encoding as integer variables. These are available
through specific methods of the cp_model like `cp_model.AddEquality(x, 3)` in
C++, `cp_model.addGreaterThan(x, 10)` in java.
**Python** and **C\#** CP-SAT APIs support general linear arithmetic (+, *, -,
==, >=, >, <, <=, !=).
==, >=, >, <, <=, !=). You need to use the Add method of the cp_model as in
`cp_model.Add(x != 3)`.
## Rabbits and Pheasants examples
Let's solve a simple children's puzzle: the Rabbits and Pheasants problem.
WIn a field of rabbits and pheasants, there are 20 heads and 56 legs. How many
In a field of rabbits and pheasants, there are 20 heads and 56 legs. How many
rabbits and pheasants are there?
### Python code
@@ -188,3 +208,742 @@ public class RabbitsAndPheasantsSat
}
}
```
## Earliness-Tardiness cost function.
Let's encode a useful convex piecewise linear function that often appears in
scheduling. You want to encourage a delivery to happen during a time window. If
you deliver early, you pay a linear penalty on waiting time. If you deliver
late, you pay a linear penalty on the delay.
Because the function is convex, you can define all affine functions, and take
the max of them to define the piecewise linear function.
The following samples output:
x=0 expr=40
x=1 expr=32
x=2 expr=24
x=3 expr=16
x=4 expr=8
x=5 expr=0
x=6 expr=0
x=7 expr=0
x=8 expr=0
x=9 expr=0
x=10 expr=0
x=11 expr=0
x=12 expr=0
x=13 expr=0
x=14 expr=0
x=15 expr=0
x=16 expr=12
x=17 expr=24
x=18 expr=36
x=19 expr=48
x=20 expr=60
### Python code
```python
"""Encodes an convex piecewise linear function."""
from __future__ import absolute_import
from __future__ import division
from __future__ import print_function
from ortools.sat.python import cp_model
class VarArraySolutionPrinter(cp_model.CpSolverSolutionCallback):
"""Print intermediate solutions."""
def __init__(self, variables):
cp_model.CpSolverSolutionCallback.__init__(self)
self.__variables = variables
self.__solution_count = 0
def on_solution_callback(self):
self.__solution_count += 1
for v in self.__variables:
print('%s=%i' % (v, self.Value(v)), end=' ')
print()
def solution_count(self):
return self.__solution_count
def earliness_tardiness_cost_sample_sat():
"""Encode the piecewise linear expression."""
earliness_date = 5 # ed.
earliness_cost = 8
lateness_date = 15 # ld.
lateness_cost = 12
# Model.
model = cp_model.CpModel()
# Declare our primary variable.
x = model.NewIntVar(0, 20, 'x')
# Create the expression variable and implement the piecewise linear function.
#
# \ /
# \______/
# ed ld
#
large_constant = 1000
expr = model.NewIntVar(0, large_constant, 'expr')
# First segment.
s1 = model.NewIntVar(-large_constant, large_constant, 's1')
model.Add(s1 == earliness_cost * (earliness_date - x))
# Second segment.
s2 = 0
# Third segment.
s3 = model.NewIntVar(-large_constant, large_constant, 's3')
model.Add(s3 == lateness_cost * (x - lateness_date))
# Link together expr and x through s1, s2, and s3.
model.AddMaxEquality(expr, [s1, s2, s3])
# Search for x values in increasing order.
model.AddDecisionStrategy([x], cp_model.CHOOSE_FIRST,
cp_model.SELECT_MIN_VALUE)
# Create a solver and solve with a fixed search.
solver = cp_model.CpSolver()
# Force the solver to follow the decision strategy exactly.
solver.parameters.search_branching = cp_model.FIXED_SEARCH
# Search and print out all solutions.
solution_printer = VarArraySolutionPrinter([x, expr])
solver.SearchForAllSolutions(model, solution_printer)
earliness_tardiness_cost_sample_sat()
```
### C++ code
```cpp
#include "ortools/sat/cp_model.h"
#include "ortools/sat/model.h"
#include "ortools/sat/sat_parameters.pb.h"
namespace operations_research {
namespace sat {
void EarlinessTardinessCostSampleSat() {
const int64 kEarlinessDate = 5;
const int64 kEarlinessCost = 8;
const int64 kLatenessDate = 15;
const int64 kLatenessCost = 12;
// Create the CP-SAT model.
CpModelBuilder cp_model;
// Declare our primary variable.
const IntVar x = cp_model.NewIntVar({0, 20});
// Create the expression variable and implement the piecewise linear function.
//
// \ /
// \______/
// ed ld
//
const int64 kLargeConstant = 1000;
const IntVar expr = cp_model.NewIntVar({0, kLargeConstant});
// First segment.
const IntVar s1 = cp_model.NewIntVar({-kLargeConstant, kLargeConstant});
cp_model.AddEquality(s1, LinearExpr::ScalProd({x}, {-kEarlinessCost})
.AddConstant(kEarlinessCost * kEarlinessDate));
// Second segment.
const IntVar s2 = cp_model.NewConstant(0);
// Third segment.
const IntVar s3 = cp_model.NewIntVar({-kLargeConstant, kLargeConstant});
cp_model.AddEquality(s3, LinearExpr::ScalProd({x}, {kLatenessCost})
.AddConstant(-kLatenessCost * kLatenessDate));
// Link together expr and x through s1, s2, and s3.
cp_model.AddMaxEquality(expr, {s1, s2, s3});
// Search for x values in increasing order.
cp_model.AddDecisionStrategy({x}, DecisionStrategyProto::CHOOSE_FIRST,
DecisionStrategyProto::SELECT_MIN_VALUE);
// Create a solver and solve with a fixed search.
Model model;
SatParameters parameters;
parameters.set_search_branching(SatParameters::FIXED_SEARCH);
parameters.set_enumerate_all_solutions(true);
model.Add(NewSatParameters(parameters));
model.Add(NewFeasibleSolutionObserver([&](const CpSolverResponse& r) {
LOG(INFO) << "x=" << SolutionIntegerValue(r, x) << " expr"
<< SolutionIntegerValue(r, expr);
}));
SolveWithModel(cp_model, &model);
}
} // namespace sat
} // namespace operations_research
int main() {
operations_research::sat::EarlinessTardinessCostSampleSat();
return EXIT_SUCCESS;
}
```
### Java code
```java
import com.google.ortools.sat.DecisionStrategyProto;
import com.google.ortools.sat.SatParameters;
import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.CpSolver;
import com.google.ortools.sat.CpSolverSolutionCallback;
import com.google.ortools.sat.IntVar;
/** Encode the piecewise linear expression. */
public class EarlinessTardinessCostSampleSat {
static { System.loadLibrary("jniortools"); }
public static void main(String[] args) throws Exception {
long earlinessDate = 5;
long earlinessCost = 8;
long latenessDate = 15;
long latenessCost = 12;
// Create the CP-SAT model.
CpModel model = new CpModel();
// Declare our primary variable.
IntVar x = model.newIntVar(0, 20, "x");
// Create the expression variable and implement the piecewise linear function.
//
// \ /
// \______/
// ed ld
//
long largeConstant = 1000;
IntVar expr = model.newIntVar(0, largeConstant, "expr");
// First segment: s1 == earlinessCost * (earlinessDate - x).
IntVar s1 = model.newIntVar(-largeConstant, largeConstant, "s1");
model.addScalProdEqual(
new IntVar[] {s1, x}, new long[] {1, earlinessCost}, earlinessCost * earlinessDate);
// Second segment.
IntVar s2 = model.newConstant(0);
// Third segment: s3 == latenessCost * (x - latenessDate).
IntVar s3 = model.newIntVar(-largeConstant, largeConstant, "s3");
model.addScalProdEqual(
new IntVar[] {s3, x}, new long[] {1, -latenessCost}, -latenessCost * latenessDate);
// Link together expr and x through s1, s2, and s3.
model.addMaxEquality(expr, new IntVar[] {s1, s2, s3});
// Search for x values in increasing order.
model.addDecisionStrategy(
new IntVar[] {x},
DecisionStrategyProto.VariableSelectionStrategy.CHOOSE_FIRST,
DecisionStrategyProto.DomainReductionStrategy.SELECT_MIN_VALUE);
// Create the solver.
CpSolver solver = new CpSolver();
// Force the solver to follow the decision strategy exactly.
solver.getParameters().setSearchBranching(SatParameters.SearchBranching.FIXED_SEARCH);
// Solve the problem with the printer callback.
solver.searchAllSolutions(
model,
new CpSolverSolutionCallback() {
public CpSolverSolutionCallback init(IntVar[] variables) {
variableArray = variables;
return this;
}
@Override
public void onSolutionCallback() {
for (IntVar v : variableArray) {
System.out.printf("%s=%d ", v.getName(), value(v));
}
System.out.println();
}
private IntVar[] variableArray;
}.init(new IntVar[] {x, expr}));
}
}
```
### C\# code
```cs
using System;
using Google.OrTools.Sat;
public class VarArraySolutionPrinter : CpSolverSolutionCallback
{
public VarArraySolutionPrinter(IntVar[] variables)
{
variables_ = variables;
}
public override void OnSolutionCallback()
{
{
foreach (IntVar v in variables_)
{
Console.Write(String.Format("{0}={1} ", v.ShortString(), Value(v)));
}
Console.WriteLine();
}
}
private IntVar[] variables_;
}
public class EarlinessTardinessCostSampleSat
{
static void Main()
{
long earliness_date = 5;
long earliness_cost = 8;
long lateness_date = 15;
long lateness_cost = 12;
// Create the CP-SAT model.
CpModel model = new CpModel();
// Declare our primary variable.
IntVar x = model.NewIntVar(0, 20, "x");
// Create the expression variable and implement the piecewise linear
// function.
//
// \ /
// \______/
// ed ld
//
long large_constant = 1000;
IntVar expr = model.NewIntVar(0, large_constant, "expr");
// First segment.
IntVar s1 = model.NewIntVar(-large_constant, large_constant, "s1");
model.Add(s1 == earliness_cost * (earliness_date - x));
// Second segment.
IntVar s2 = model.NewConstant(0);
// Third segment.
IntVar s3 = model.NewIntVar(-large_constant, large_constant, "s3");
model.Add(s3 == lateness_cost * (x - lateness_date));
// Link together expr and x through s1, s2, and s3.
model.AddMaxEquality(expr, new IntVar[] {s1, s2, s3});
// Search for x values in increasing order.
model.AddDecisionStrategy(
new IntVar[] {x},
DecisionStrategyProto.Types.VariableSelectionStrategy.ChooseFirst,
DecisionStrategyProto.Types.DomainReductionStrategy.SelectMinValue);
// Create the solver.
CpSolver solver = new CpSolver();
// Force solver to follow the decision strategy exactly.
solver.StringParameters = "search_branching:FIXED_SEARCH";
VarArraySolutionPrinter cb =
new VarArraySolutionPrinter(new IntVar[] {x, expr});
solver.SearchAllSolutions(model, cb);
}
}
```
## Step function.
Let's encode a step function. We will use one Boolean variable per step value,
and filter the admissible domain of the input variable with this variable.
The following samples output:
x=0 expr=2
x=1 expr=2
x=3 expr=2
x=4 expr=2
x=5 expr=0
x=6 expr=0
x=7 expr=3
x=8 expr=0
x=9 expr=0
x=10 expr=0
x=11 expr=2
x=12 expr=2
x=13 expr=2
x=14 expr=2
x=15 expr=2
x=16 expr=2
x=17 expr=2
x=18 expr=2
x=19 expr=2
x=20 expr=2
### Python code
```python
"""Implements a step function."""
from __future__ import absolute_import
from __future__ import division
from __future__ import print_function
from ortools.sat.python import cp_model
class VarArraySolutionPrinter(cp_model.CpSolverSolutionCallback):
"""Print intermediate solutions."""
def __init__(self, variables):
cp_model.CpSolverSolutionCallback.__init__(self)
self.__variables = variables
self.__solution_count = 0
def on_solution_callback(self):
self.__solution_count += 1
for v in self.__variables:
print('%s=%i' % (v, self.Value(v)), end=' ')
print()
def solution_count(self):
return self.__solution_count
def step_function_sample_sat():
"""Encode the step function."""
# Model.
model = cp_model.CpModel()
# Declare our primary variable.
x = model.NewIntVar(0, 20, 'x')
# Create the expression variable and implement the step function
# Note it is not defined for x == 2.
#
# - 3
# -- -- --------- 2
# 1
# -- --- 0
# 0==================20
#
expr = model.NewIntVar(0, 3, 'expr')
# expr == 0 on [5, 6] U [8, 10]
b0 = model.NewBoolVar('b0')
model.AddLinearConstraintWithBounds([(x, 1)], [5, 6, 8, 10]).OnlyEnforceIf(b0)
model.Add(expr == 0).OnlyEnforceIf(b0)
# expr == 2 on [0, 1] U [3, 4] U [11, 20]
b2 = model.NewBoolVar('b2')
model.AddLinearConstraintWithBounds([(x, 1)],
[0, 1, 3, 4, 11, 20]).OnlyEnforceIf(b2)
model.Add(expr == 2).OnlyEnforceIf(b2)
# expr == 3 when x == 7
b3 = model.NewBoolVar('b3')
model.Add(x == 7).OnlyEnforceIf(b3)
model.Add(expr == 3).OnlyEnforceIf(b3)
# At least one bi is true. (we could use a sum == 1).
model.AddBoolOr([b0, b2, b3])
# Search for x values in increasing order.
model.AddDecisionStrategy([x], cp_model.CHOOSE_FIRST,
cp_model.SELECT_MIN_VALUE)
# Create a solver and solve with a fixed search.
solver = cp_model.CpSolver()
# Force the solver to follow the decision strategy exactly.
solver.parameters.search_branching = cp_model.FIXED_SEARCH
# Search and print out all solutions.
solution_printer = VarArraySolutionPrinter([x, expr])
solver.SearchForAllSolutions(model, solution_printer)
step_function_sample_sat()
```
### C++ code
```cpp
#include "ortools/sat/cp_model.h"
#include "ortools/sat/model.h"
#include "ortools/sat/sat_parameters.pb.h"
namespace operations_research {
namespace sat {
void StepFunctionSampleSat() {
// Create the CP-SAT model.
CpModelBuilder cp_model;
// Declare our primary variable.
const IntVar x = cp_model.NewIntVar({0, 20});
// Create the expression variable and implement the step function
// Note it is not defined for var == 2.
//
// - 3
// -- -- --------- 2
// 1
// -- --- 0
// 0 ================ 20
//
IntVar expr = cp_model.NewIntVar({0, 3});
// expr == 0 on [5, 6] U [8, 10]
BoolVar b0 = cp_model.NewBoolVar();
cp_model.AddLinearConstraint(x, Domain::FromValues({5, 6, 8, 9, 10}))
.OnlyEnforceIf(b0);
cp_model.AddEquality(expr, 0).OnlyEnforceIf(b0);
// expr == 2 on [0, 1] U [3, 4] U [11, 20]
BoolVar b2 = cp_model.NewBoolVar();
cp_model
.AddLinearConstraint(x, Domain::FromIntervals({{0, 1}, {3, 4}, {11, 20}}))
.OnlyEnforceIf(b2);
cp_model.AddEquality(expr, 2).OnlyEnforceIf(b2);
// expr == 3 when x = 7
BoolVar b3 = cp_model.NewBoolVar();
cp_model.AddEquality(x, 7).OnlyEnforceIf(b3);
cp_model.AddEquality(expr, 3).OnlyEnforceIf(b3);
// At least one bi is true. (we could use a sum == 1).
cp_model.AddBoolOr({b0, b2, b3});
// Search for x values in increasing order.
cp_model.AddDecisionStrategy({x}, DecisionStrategyProto::CHOOSE_FIRST,
DecisionStrategyProto::SELECT_MIN_VALUE);
// Create a solver and solve with a fixed search.
Model model;
SatParameters parameters;
parameters.set_search_branching(SatParameters::FIXED_SEARCH);
parameters.set_enumerate_all_solutions(true);
model.Add(NewSatParameters(parameters));
model.Add(NewFeasibleSolutionObserver([&](const CpSolverResponse& r) {
LOG(INFO) << "x=" << SolutionIntegerValue(r, x) << " expr"
<< SolutionIntegerValue(r, expr);
}));
SolveWithModel(cp_model, &model);
}
} // namespace sat
} // namespace operations_research
int main() {
operations_research::sat::StepFunctionSampleSat();
return EXIT_SUCCESS;
}
```
### Java code
```java
import com.google.ortools.sat.DecisionStrategyProto;
import com.google.ortools.sat.SatParameters;
import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.CpSolver;
import com.google.ortools.sat.CpSolverSolutionCallback;
import com.google.ortools.sat.IntVar;
import com.google.ortools.sat.Literal;
/** Link integer constraints together. */
public class StepFunctionSampleSat {
static { System.loadLibrary("jniortools"); }
public static void main(String[] args) throws Exception {
// Create the CP-SAT model.
CpModel model = new CpModel();
// Declare our primary variable.
IntVar x = model.newIntVar(0, 20, "x");
// Create the expression variable and implement the step function
// Note it is not defined for var == 2.
//
// - 3
// -- -- --------- 2
// 1
// -- --- 0
// 0 ================ 20
//
IntVar expr = model.newIntVar(0, 3, "expr");
// expr == 0 on [5, 6] U [8, 10]
Literal b0 = model.newBoolVar("b0");
model.addLinearSumWithBounds(new IntVar[] {x}, new long[] {5, 6, 8, 10}).onlyEnforceIf(b0);
model.addEquality(expr, 0).onlyEnforceIf(b0);
// expr == 2 on [0, 1] U [3, 4] U [11, 20]
Literal b2 = model.newBoolVar("b2");
model
.addLinearSumWithBounds(new IntVar[] {x}, new long[] {0, 1, 3, 4, 11, 20})
.onlyEnforceIf(b2);
model.addEquality(expr, 2).onlyEnforceIf(b2);
// expr == 3 when x = 7
Literal b3 = model.newBoolVar("b3");
model.addEquality(x, 7).onlyEnforceIf(b3);
model.addEquality(expr, 3).onlyEnforceIf(b3);
// At least one bi is true. (we could use a sum == 1).
model.addBoolOr(new Literal[] {b0, b2, b3});
// Search for x values in increasing order.
model.addDecisionStrategy(
new IntVar[] {x},
DecisionStrategyProto.VariableSelectionStrategy.CHOOSE_FIRST,
DecisionStrategyProto.DomainReductionStrategy.SELECT_MIN_VALUE);
// Create the solver.
CpSolver solver = new CpSolver();
// Force the solver to follow the decision strategy exactly.
solver.getParameters().setSearchBranching(SatParameters.SearchBranching.FIXED_SEARCH);
// Solve the problem with the printer callback.
solver.searchAllSolutions(
model,
new CpSolverSolutionCallback() {
public CpSolverSolutionCallback init(IntVar[] variables) {
variableArray = variables;
return this;
}
@Override
public void onSolutionCallback() {
for (IntVar v : variableArray) {
System.out.printf("%s=%d ", v.getName(), value(v));
}
System.out.println();
}
private IntVar[] variableArray;
}.init(new IntVar[] {x, expr}));
}
}
```
### C\# code
```cs
using System;
using Google.OrTools.Sat;
public class VarArraySolutionPrinter : CpSolverSolutionCallback
{
public VarArraySolutionPrinter(IntVar[] variables)
{
variables_ = variables;
}
public override void OnSolutionCallback()
{
{
foreach (IntVar v in variables_)
{
Console.Write(String.Format("{0}={1} ", v.ShortString(), Value(v)));
}
Console.WriteLine();
}
}
private IntVar[] variables_;
}
public class StepFunctionSampleSat
{
static void Main()
{
// Create the CP-SAT model.
CpModel model = new CpModel();
// Declare our primary variable.
IntVar x = model.NewIntVar(0, 20, "x");
// Create the expression variable and implement the step function
// Note it is not defined for var == 2.
//
// - 3
// -- -- --------- 2
// 1
// -- --- 0
// 0 20
//
IntVar expr = model.NewIntVar(0, 3, "expr");
// expr == 0 on [5, 6] U [8, 10]
ILiteral b0 = model.NewBoolVar("b0");
model.AddLinearConstraintWithBounds(
new IntVar[] {x},
new long[] {1},
new long[] {5, 6, 8, 10}).OnlyEnforceIf(b0);
model.Add(expr == 0).OnlyEnforceIf(b0);
// expr == 2 on [0, 1] U [3, 4] U [11, 20]
ILiteral b2 = model.NewBoolVar("b2");
model.AddLinearConstraintWithBounds(
new IntVar[] {x},
new long[] {1},
new long[] {0, 1, 3, 4, 11, 20}).OnlyEnforceIf(b2);
model.Add(expr == 2).OnlyEnforceIf(b2);
// expr == 3 when x == 7
ILiteral b3 = model.NewBoolVar("b3");
model.Add(x == 7).OnlyEnforceIf(b3);
model.Add(expr == 3).OnlyEnforceIf(b3);
// At least one bi is true. (we could use a sum == 1).
model.AddBoolOr(new ILiteral[] {b0, b2, b3});
// Search for x values in increasing order.
model.AddDecisionStrategy(
new IntVar[] {x},
DecisionStrategyProto.Types.VariableSelectionStrategy.ChooseFirst,
DecisionStrategyProto.Types.DomainReductionStrategy.SelectMinValue);
// Create the solver.
CpSolver solver = new CpSolver();
// Force solver to follow the decision strategy exactly.
solver.StringParameters = "search_branching:FIXED_SEARCH";
VarArraySolutionPrinter cb =
new VarArraySolutionPrinter(new IntVar[] {x, expr});
solver.SearchAllSolutions(model, cb);
}
}
```

14
ortools/sat/integer.cc
View File

@@ -1563,7 +1563,17 @@ void GenericLiteralWatcher::UpdateCallingNeeds(Trail* trail) {
}
bool GenericLiteralWatcher::Propagate(Trail* trail) {
// Only once per call to Propagate(), if we are at level zero, we might want
// to call propagators even if the bounds didn't change.
const int level = trail->CurrentDecisionLevel();
if (level == 0) {
for (const int id : propagator_ids_to_call_at_level_zero_) {
if (in_queue_[id]) continue;
in_queue_[id] = true;
queue_by_priority_[id_to_priority_[id]].push_back(id);
}
}
UpdateCallingNeeds(trail);
// Note that the priority may be set to -1 inside the loop in order to restart
@@ -1727,6 +1737,10 @@ void GenericLiteralWatcher::NotifyThatPropagatorMayNotReachFixedPointInOnePass(
id_to_idempotence_[id] = false;
}
void GenericLiteralWatcher::AlwaysCallAtLevelZero(int id) {
propagator_ids_to_call_at_level_zero_.push_back(id);
}
void GenericLiteralWatcher::RegisterReversibleClass(int id,
ReversibleInterface* rev) {
id_to_reversible_classes_[id].push_back(rev);

9
ortools/sat/integer.h
View File

@@ -996,6 +996,12 @@ class GenericLiteralWatcher : public SatPropagator {
// called again if they change one of their own watched variables.
void NotifyThatPropagatorMayNotReachFixedPointInOnePass(int id);
// Whether we call a propagator even if its watched variables didn't change.
// This is only used when we are back to level zero. This was introduced for
// the LP propagator where we might need to continue an interrupted solve or
// add extra cuts at level zero.
void AlwaysCallAtLevelZero(int id);
// Watches the corresponding quantity. The propagator with given id will be
// called if it changes. Note that WatchLiteral() only trigger when the
// literal becomes true.
@@ -1082,6 +1088,9 @@ class GenericLiteralWatcher : public SatPropagator {
std::vector<int> id_to_priority_;
std::vector<int> id_to_idempotence_;
// Special propagators that needs to always be called at level zero.
std::vector<int> propagator_ids_to_call_at_level_zero_;
std::vector<std::function<void(const std::vector<IntegerVariable>&)>>
level_zero_modified_variable_callback_;

1
ortools/sat/linear_programming_constraint.cc
View File

@@ -212,6 +212,7 @@ void LinearProgrammingConstraint::RegisterWith(Model* model) {
watcher->WatchUpperBound(objective_cp_, watcher_id);
}
watcher->SetPropagatorPriority(watcher_id, 2);
watcher->AlwaysCallAtLevelZero(watcher_id);
if (integer_variables_.size() >= 20) { // Do not use on small subparts.
auto* container = model->GetOrCreate<SearchHeuristicsVector>();

6
ortools/sat/python/cp_model.py
View File

@@ -1513,11 +1513,11 @@ class CpSolverSolutionCallback(pywrapsat.SolutionCallback):
"""
if not self.HasResponse():
raise RuntimeError('Solve() has not be called.')
if isinstance(lit, IntVar) or isinstance(lit, _NotBooleanVariable):
if isinstance(lit, numbers.Integral):
return bool(lit)
elif isinstance(lit, IntVar) or isinstance(lit, _NotBooleanVariable):
index = lit.Index()
return self.SolutionBooleanValue(index)
elif isinstance(lit, numbers.Integral):
return bool(lit)
else:
raise TypeError(
'Cannot interpret %s as a boolean expression.' % lit)

1
ortools/sat/python/sat.i
View File

@@ -93,3 +93,4 @@ PY_PROTO_TYPEMAP(ortools.sat.sat_parameters_pb2,
%include "ortools/sat/swig_helper.h"
%unignoreall

93
ortools/sat/samples/EarlinessTardinessCostSampleSat.cs Normal file
View File

@@ -0,0 +1,93 @@
// Copyright 2010-2018 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.
using System;
using Google.OrTools.Sat;
public class VarArraySolutionPrinter : CpSolverSolutionCallback
{
public VarArraySolutionPrinter(IntVar[] variables)
{
variables_ = variables;
}
public override void OnSolutionCallback()
{
{
foreach (IntVar v in variables_)
{
Console.Write(String.Format("{0}={1} ", v.ShortString(), Value(v)));
}
Console.WriteLine();
}
}
private IntVar[] variables_;
}
public class EarlinessTardinessCostSampleSat
{
static void Main()
{
long earliness_date = 5;
long earliness_cost = 8;
long lateness_date = 15;
long lateness_cost = 12;
// Create the CP-SAT model.
CpModel model = new CpModel();
// Declare our primary variable.
IntVar x = model.NewIntVar(0, 20, "x");
// Create the expression variable and implement the piecewise linear
// function.
//
// \ /
// \______/
// ed ld
//
long large_constant = 1000;
IntVar expr = model.NewIntVar(0, large_constant, "expr");
// First segment.
IntVar s1 = model.NewIntVar(-large_constant, large_constant, "s1");
model.Add(s1 == earliness_cost * (earliness_date - x));
// Second segment.
IntVar s2 = model.NewConstant(0);
// Third segment.
IntVar s3 = model.NewIntVar(-large_constant, large_constant, "s3");
model.Add(s3 == lateness_cost * (x - lateness_date));
// Link together expr and x through s1, s2, and s3.
model.AddMaxEquality(expr, new IntVar[] {s1, s2, s3});
// Search for x values in increasing order.
model.AddDecisionStrategy(
new IntVar[] {x},
DecisionStrategyProto.Types.VariableSelectionStrategy.ChooseFirst,
DecisionStrategyProto.Types.DomainReductionStrategy.SelectMinValue);
// Create the solver.
CpSolver solver = new CpSolver();
// Force solver to follow the decision strategy exactly.
solver.StringParameters = "search_branching:FIXED_SEARCH";
VarArraySolutionPrinter cb =
new VarArraySolutionPrinter(new IntVar[] {x, expr});
solver.SearchAllSolutions(model, cb);
}
}

20
ortools/sat/samples/EarlinessTardinessCostSampleSat.csproj Normal file
View File

@@ -0,0 +1,20 @@
<Project Sdk="Microsoft.NET.Sdk">
<PropertyGroup>
<OutputType>Exe</OutputType>
<LangVersion>7.2</LangVersion>
<TargetFramework>netcoreapp2.1</TargetFramework>
<EnableDefaultItems>false</EnableDefaultItems>
<RestoreSources>../../../packages;$(RestoreSources);https://api.nuget.org/v3/index.json</RestoreSources>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugType>full</DebugType>
<Optimize>true</Optimize>
<GenerateTailCalls>true</GenerateTailCalls>
</PropertyGroup>
<ItemGroup>
<Compile Include="EarlinessTardinessCostSampleSat.cs" />
<PackageReference Include="Google.OrTools" Version="7.0.*" />
</ItemGroup>
</Project>

93
ortools/sat/samples/EarlinessTardinessCostSampleSat.java Normal file
View File

@@ -0,0 +1,93 @@
// Copyright 2010-2018 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.
import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.CpSolver;
import com.google.ortools.sat.CpSolverSolutionCallback;
import com.google.ortools.sat.DecisionStrategyProto;
import com.google.ortools.sat.IntVar;
import com.google.ortools.sat.SatParameters;
/** Encode the piecewise linear expression. */
public class EarlinessTardinessCostSampleSat {
static {
System.loadLibrary("jniortools");
}
public static void main(String[] args) throws Exception {
long earlinessDate = 5;
long earlinessCost = 8;
long latenessDate = 15;
long latenessCost = 12;
// Create the CP-SAT model.
CpModel model = new CpModel();
// Declare our primary variable.
IntVar x = model.newIntVar(0, 20, "x");
// Create the expression variable and implement the piecewise linear function.
//
// \ /
// \______/
// ed ld
//
long largeConstant = 1000;
IntVar expr = model.newIntVar(0, largeConstant, "expr");
// First segment: s1 == earlinessCost * (earlinessDate - x).
IntVar s1 = model.newIntVar(-largeConstant, largeConstant, "s1");
model.addScalProdEqual(
new IntVar[] {s1, x}, new long[] {1, earlinessCost}, earlinessCost* earlinessDate);
// Second segment.
IntVar s2 = model.newConstant(0);
// Third segment: s3 == latenessCost * (x - latenessDate).
IntVar s3 = model.newIntVar(-largeConstant, largeConstant, "s3");
model.addScalProdEqual(
new IntVar[] {s3, x}, new long[] {1, -latenessCost}, -latenessCost* latenessDate);
// Link together expr and x through s1, s2, and s3.
model.addMaxEquality(expr, new IntVar[] {s1, s2, s3});
// Search for x values in increasing order.
model.addDecisionStrategy(new IntVar[] {x},
DecisionStrategyProto.VariableSelectionStrategy.CHOOSE_FIRST,
DecisionStrategyProto.DomainReductionStrategy.SELECT_MIN_VALUE);
// Create the solver.
CpSolver solver = new CpSolver();
// Force the solver to follow the decision strategy exactly.
solver.getParameters().setSearchBranching(SatParameters.SearchBranching.FIXED_SEARCH);
// Solve the problem with the printer callback.
solver.searchAllSolutions(model, new CpSolverSolutionCallback() {
public CpSolverSolutionCallback init(IntVar[] variables) {
variableArray = variables;
return this;
}
@Override
public void onSolutionCallback() {
for (IntVar v : variableArray) {
System.out.printf("%s=%d ", v.getName(), value(v));
}
System.out.println();
}
private IntVar[] variableArray;
}.init(new IntVar[] {x, expr}));
}
}

100
ortools/sat/samples/StepFunctionSampleSat.cs Normal file
View File

@@ -0,0 +1,100 @@
// Copyright 2010-2018 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.
using System;
using Google.OrTools.Sat;
public class VarArraySolutionPrinter : CpSolverSolutionCallback
{
public VarArraySolutionPrinter(IntVar[] variables)
{
variables_ = variables;
}
public override void OnSolutionCallback()
{
{
foreach (IntVar v in variables_)
{
Console.Write(String.Format("{0}={1} ", v.ShortString(), Value(v)));
}
Console.WriteLine();
}
}
private IntVar[] variables_;
}
public class StepFunctionSampleSat
{
static void Main()
{
// Create the CP-SAT model.
CpModel model = new CpModel();
// Declare our primary variable.
IntVar x = model.NewIntVar(0, 20, "x");
// Create the expression variable and implement the step function
// Note it is not defined for var == 2.
//
// - 3
// -- -- --------- 2
// 1
// -- --- 0
// 0 20
//
IntVar expr = model.NewIntVar(0, 3, "expr");
// expr == 0 on [5, 6] U [8, 10]
ILiteral b0 = model.NewBoolVar("b0");
model.AddLinearConstraintWithBounds(
new IntVar[] {x},
new long[] {1},
new long[] {5, 6, 8, 10}).OnlyEnforceIf(b0);
model.Add(expr == 0).OnlyEnforceIf(b0);
// expr == 2 on [0, 1] U [3, 4] U [11, 20]
ILiteral b2 = model.NewBoolVar("b2");
model.AddLinearConstraintWithBounds(
new IntVar[] {x},
new long[] {1},
new long[] {0, 1, 3, 4, 11, 20}).OnlyEnforceIf(b2);
model.Add(expr == 2).OnlyEnforceIf(b2);
// expr == 3 when x == 7
ILiteral b3 = model.NewBoolVar("b3");
model.Add(x == 7).OnlyEnforceIf(b3);
model.Add(expr == 3).OnlyEnforceIf(b3);
// At least one bi is true. (we could use a sum == 1).
model.AddBoolOr(new ILiteral[] {b0, b2, b3});
// Search for x values in increasing order.
model.AddDecisionStrategy(
new IntVar[] {x},
DecisionStrategyProto.Types.VariableSelectionStrategy.ChooseFirst,
DecisionStrategyProto.Types.DomainReductionStrategy.SelectMinValue);
// Create the solver.
CpSolver solver = new CpSolver();
// Force solver to follow the decision strategy exactly.
solver.StringParameters = "search_branching:FIXED_SEARCH";
VarArraySolutionPrinter cb =
new VarArraySolutionPrinter(new IntVar[] {x, expr});
solver.SearchAllSolutions(model, cb);
}
}

20
ortools/sat/samples/StepFunctionSampleSat.csproj Normal file
View File

@@ -0,0 +1,20 @@
<Project Sdk="Microsoft.NET.Sdk">
<PropertyGroup>
<OutputType>Exe</OutputType>
<LangVersion>7.2</LangVersion>
<TargetFramework>netcoreapp2.1</TargetFramework>
<EnableDefaultItems>false</EnableDefaultItems>
<RestoreSources>../../../packages;$(RestoreSources);https://api.nuget.org/v3/index.json</RestoreSources>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugType>full</DebugType>
<Optimize>true</Optimize>
<GenerateTailCalls>true</GenerateTailCalls>
</PropertyGroup>
<ItemGroup>
<Compile Include="StepFunctionSampleSat.cs" />
<PackageReference Include="Google.OrTools" Version="7.0.*" />
</ItemGroup>
</Project>

95
ortools/sat/samples/StepFunctionSampleSat.java Normal file
View File

@@ -0,0 +1,95 @@
// Copyright 2010-2018 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.
import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.CpSolver;
import com.google.ortools.sat.CpSolverSolutionCallback;
import com.google.ortools.sat.DecisionStrategyProto;
import com.google.ortools.sat.IntVar;
import com.google.ortools.sat.Literal;
import com.google.ortools.sat.SatParameters;
/** Link integer constraints together. */
public class StepFunctionSampleSat {
static {
System.loadLibrary("jniortools");
}
public static void main(String[] args) throws Exception {
// Create the CP-SAT model.
CpModel model = new CpModel();
// Declare our primary variable.
IntVar x = model.newIntVar(0, 20, "x");
// Create the expression variable and implement the step function
// Note it is not defined for var == 2.
//
// - 3
// -- -- --------- 2
// 1
// -- --- 0
// 0 ================ 20
//
IntVar expr = model.newIntVar(0, 3, "expr");
// expr == 0 on [5, 6] U [8, 10]
Literal b0 = model.newBoolVar("b0");
model.addLinearSumWithBounds(new IntVar[] {x}, new long[] {5, 6, 8, 10}).onlyEnforceIf(b0);
model.addEquality(expr, 0).onlyEnforceIf(b0);
// expr == 2 on [0, 1] U [3, 4] U [11, 20]
Literal b2 = model.newBoolVar("b2");
model.addLinearSumWithBounds(new IntVar[] {x}, new long[] {0, 1, 3, 4, 11, 20})
.onlyEnforceIf(b2);
model.addEquality(expr, 2).onlyEnforceIf(b2);
// expr == 3 when x = 7
Literal b3 = model.newBoolVar("b3");
model.addEquality(x, 7).onlyEnforceIf(b3);
model.addEquality(expr, 3).onlyEnforceIf(b3);
// At least one bi is true. (we could use a sum == 1).
model.addBoolOr(new Literal[] {b0, b2, b3});
// Search for x values in increasing order.
model.addDecisionStrategy(new IntVar[] {x},
DecisionStrategyProto.VariableSelectionStrategy.CHOOSE_FIRST,
DecisionStrategyProto.DomainReductionStrategy.SELECT_MIN_VALUE);
// Create the solver.
CpSolver solver = new CpSolver();
// Force the solver to follow the decision strategy exactly.
solver.getParameters().setSearchBranching(SatParameters.SearchBranching.FIXED_SEARCH);
// Solve the problem with the printer callback.
solver.searchAllSolutions(model, new CpSolverSolutionCallback() {
public CpSolverSolutionCallback init(IntVar[] variables) {
variableArray = variables;
return this;
}
@Override
public void onSolutionCallback() {
for (IntVar v : variableArray) {
System.out.printf("%s=%d ", v.getName(), value(v));
}
System.out.println();
}
private IntVar[] variableArray;
}.init(new IntVar[] {x, expr}));
}
}

82
ortools/sat/samples/earliness_tardiness_cost_sample_sat.cc Normal file
View File

@@ -0,0 +1,82 @@
// Copyright 2010-2018 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.
#include "ortools/sat/cp_model.h"
#include "ortools/sat/model.h"
#include "ortools/sat/sat_parameters.pb.h"
namespace operations_research {
namespace sat {
void EarlinessTardinessCostSampleSat() {
const int64 kEarlinessDate = 5;
const int64 kEarlinessCost = 8;
const int64 kLatenessDate = 15;
const int64 kLatenessCost = 12;
// Create the CP-SAT model.
CpModelBuilder cp_model;
// Declare our primary variable.
const IntVar x = cp_model.NewIntVar({0, 20});
// Create the expression variable and implement the piecewise linear function.
//
// \ /
// \______/
// ed ld
//
const int64 kLargeConstant = 1000;
const IntVar expr = cp_model.NewIntVar({0, kLargeConstant});
// First segment.
const IntVar s1 = cp_model.NewIntVar({-kLargeConstant, kLargeConstant});
cp_model.AddEquality(s1, LinearExpr::ScalProd({x}, {-kEarlinessCost})
.AddConstant(kEarlinessCost * kEarlinessDate));
// Second segment.
const IntVar s2 = cp_model.NewConstant(0);
// Third segment.
const IntVar s3 = cp_model.NewIntVar({-kLargeConstant, kLargeConstant});
cp_model.AddEquality(s3, LinearExpr::ScalProd({x}, {kLatenessCost})
.AddConstant(-kLatenessCost * kLatenessDate));
// Link together expr and x through s1, s2, and s3.
cp_model.AddMaxEquality(expr, {s1, s2, s3});
// Search for x values in increasing order.
cp_model.AddDecisionStrategy({x}, DecisionStrategyProto::CHOOSE_FIRST,
DecisionStrategyProto::SELECT_MIN_VALUE);
// Create a solver and solve with a fixed search.
Model model;
SatParameters parameters;
parameters.set_search_branching(SatParameters::FIXED_SEARCH);
parameters.set_enumerate_all_solutions(true);
model.Add(NewSatParameters(parameters));
model.Add(NewFeasibleSolutionObserver([&](const CpSolverResponse& r) {
LOG(INFO) << "x=" << SolutionIntegerValue(r, x) << " expr"
<< SolutionIntegerValue(r, expr);
}));
SolveWithModel(cp_model, &model);
}
} // namespace sat
} // namespace operations_research
int main() {
operations_research::sat::EarlinessTardinessCostSampleSat();
return EXIT_SUCCESS;
}

92
ortools/sat/samples/earliness_tardiness_cost_sample_sat.py Normal file
View File

@@ -0,0 +1,92 @@
# Copyright 2010-2018 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.
"""Encodes an convex piecewise linear function."""
from __future__ import absolute_import
from __future__ import division
from __future__ import print_function
from ortools.sat.python import cp_model
class VarArraySolutionPrinter(cp_model.CpSolverSolutionCallback):
"""Print intermediate solutions."""
def __init__(self, variables):
cp_model.CpSolverSolutionCallback.__init__(self)
self.__variables = variables
self.__solution_count = 0
def on_solution_callback(self):
self.__solution_count += 1
for v in self.__variables:
print('%s=%i' % (v, self.Value(v)), end=' ')
print()
def solution_count(self):
return self.__solution_count
def earliness_tardiness_cost_sample_sat():
"""Encode the piecewise linear expression."""
earliness_date = 5 # ed.
earliness_cost = 8
lateness_date = 15 # ld.
lateness_cost = 12
# Model.
model = cp_model.CpModel()
# Declare our primary variable.
x = model.NewIntVar(0, 20, 'x')
# Create the expression variable and implement the piecewise linear function.
#
# \ /
# \______/
# ed ld
#
large_constant = 1000
expr = model.NewIntVar(0, large_constant, 'expr')
# First segment.
s1 = model.NewIntVar(-large_constant, large_constant, 's1')
model.Add(s1 == earliness_cost * (earliness_date - x))
# Second segment.
s2 = 0
# Third segment.
s3 = model.NewIntVar(-large_constant, large_constant, 's3')
model.Add(s3 == lateness_cost * (x - lateness_date))
# Link together expr and x through s1, s2, and s3.
model.AddMaxEquality(expr, [s1, s2, s3])
# Search for x values in increasing order.
model.AddDecisionStrategy([x], cp_model.CHOOSE_FIRST,
cp_model.SELECT_MIN_VALUE)
# Create a solver and solve with a fixed search.
solver = cp_model.CpSolver()
# Force the solver to follow the decision strategy exactly.
solver.parameters.search_branching = cp_model.FIXED_SEARCH
# Search and print out all solutions.
solution_printer = VarArraySolutionPrinter([x, expr])
solver.SearchForAllSolutions(model, solution_printer)
earliness_tardiness_cost_sample_sat()

1
ortools/sat/samples/nurses_sat.py
View File

@@ -115,6 +115,7 @@ def main():
# Creates the solver and solve.
# [START solve]
solver = cp_model.CpSolver()
solver.parameters.linearization_level = 0
# Display the first five solutions.
a_few_solutions = range(5)
solution_printer = NursesPartialSolutionPrinter(

85
ortools/sat/samples/step_function_sample_sat.cc Normal file
View File

@@ -0,0 +1,85 @@
// Copyright 2010-2018 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.
#include "ortools/sat/cp_model.h"
#include "ortools/sat/model.h"
#include "ortools/sat/sat_parameters.pb.h"
namespace operations_research {
namespace sat {
void StepFunctionSampleSat() {
// Create the CP-SAT model.
CpModelBuilder cp_model;
// Declare our primary variable.
const IntVar x = cp_model.NewIntVar({0, 20});
// Create the expression variable and implement the step function
// Note it is not defined for var == 2.
//
// - 3
// -- -- --------- 2
// 1
// -- --- 0
// 0 ================ 20
//
IntVar expr = cp_model.NewIntVar({0, 3});
// expr == 0 on [5, 6] U [8, 10]
BoolVar b0 = cp_model.NewBoolVar();
cp_model.AddLinearConstraint(x, Domain::FromValues({5, 6, 8, 9, 10}))
.OnlyEnforceIf(b0);
cp_model.AddEquality(expr, 0).OnlyEnforceIf(b0);
// expr == 2 on [0, 1] U [3, 4] U [11, 20]
BoolVar b2 = cp_model.NewBoolVar();
cp_model
.AddLinearConstraint(x, Domain::FromIntervals({{0, 1}, {3, 4}, {11, 20}}))
.OnlyEnforceIf(b2);
cp_model.AddEquality(expr, 2).OnlyEnforceIf(b2);
// expr == 3 when x = 7
BoolVar b3 = cp_model.NewBoolVar();
cp_model.AddEquality(x, 7).OnlyEnforceIf(b3);
cp_model.AddEquality(expr, 3).OnlyEnforceIf(b3);
// At least one bi is true. (we could use a sum == 1).
cp_model.AddBoolOr({b0, b2, b3});
// Search for x values in increasing order.
cp_model.AddDecisionStrategy({x}, DecisionStrategyProto::CHOOSE_FIRST,
DecisionStrategyProto::SELECT_MIN_VALUE);
// Create a solver and solve with a fixed search.
Model model;
SatParameters parameters;
parameters.set_search_branching(SatParameters::FIXED_SEARCH);
parameters.set_enumerate_all_solutions(true);
model.Add(NewSatParameters(parameters));
model.Add(NewFeasibleSolutionObserver([&](const CpSolverResponse& r) {
LOG(INFO) << "x=" << SolutionIntegerValue(r, x) << " expr"
<< SolutionIntegerValue(r, expr);
}));
SolveWithModel(cp_model, &model);
}
} // namespace sat
} // namespace operations_research
int main() {
operations_research::sat::StepFunctionSampleSat();
return EXIT_SUCCESS;
}

96
ortools/sat/samples/step_function_sample_sat.py Normal file
View File

@@ -0,0 +1,96 @@
# Copyright 2010-2018 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.
"""Implements a step function."""
from __future__ import absolute_import
from __future__ import division
from __future__ import print_function
from ortools.sat.python import cp_model
class VarArraySolutionPrinter(cp_model.CpSolverSolutionCallback):
"""Print intermediate solutions."""
def __init__(self, variables):
cp_model.CpSolverSolutionCallback.__init__(self)
self.__variables = variables
self.__solution_count = 0
def on_solution_callback(self):
self.__solution_count += 1
for v in self.__variables:
print('%s=%i' % (v, self.Value(v)), end=' ')
print()
def solution_count(self):
return self.__solution_count
def step_function_sample_sat():
"""Encode the step function."""
# Model.
model = cp_model.CpModel()
# Declare our primary variable.
x = model.NewIntVar(0, 20, 'x')
# Create the expression variable and implement the step function
# Note it is not defined for x == 2.
#
# - 3
# -- -- --------- 2
# 1
# -- --- 0
# 0==================20
#
expr = model.NewIntVar(0, 3, 'expr')
# expr == 0 on [5, 6] U [8, 10]
b0 = model.NewBoolVar('b0')
model.AddLinearConstraintWithBounds([(x, 1)],
[5, 6, 8, 10]).OnlyEnforceIf(b0)
model.Add(expr == 0).OnlyEnforceIf(b0)
# expr == 2 on [0, 1] U [3, 4] U [11, 20]
b2 = model.NewBoolVar('b2')
model.AddLinearConstraintWithBounds([(x, 1)],
[0, 1, 3, 4, 11, 20]).OnlyEnforceIf(b2)
model.Add(expr == 2).OnlyEnforceIf(b2)
# expr == 3 when x == 7
b3 = model.NewBoolVar('b3')
model.Add(x == 7).OnlyEnforceIf(b3)
model.Add(expr == 3).OnlyEnforceIf(b3)
# At least one bi is true. (we could use a sum == 1).
model.AddBoolOr([b0, b2, b3])
# Search for x values in increasing order.
model.AddDecisionStrategy([x], cp_model.CHOOSE_FIRST,
cp_model.SELECT_MIN_VALUE)
# Create a solver and solve with a fixed search.
solver = cp_model.CpSolver()
# Force the solver to follow the decision strategy exactly.
solver.parameters.search_branching = cp_model.FIXED_SEARCH
# Search and print out all solutions.
solution_printer = VarArraySolutionPrinter([x, expr])
solver.SearchForAllSolutions(model, solution_printer)
step_function_sample_sat()

4
ortools/sat/swig_helper.h
View File

@@ -79,12 +79,12 @@ class SolutionCallback {
std::atomic<bool>* stopped() const { return &stopped_; }
bool HasResponse() const { return has_response_; }
operations_research::sat::CpSolverResponse Response() const {
return response_;
}
bool HasResponse() const { return has_response_; }
private:
mutable CpSolverResponse response_;
mutable bool has_response_ = false;