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

add new code samoke; update internals

Browse Source
This commit is contained in:
Laurent Perron
2019-08-23 16:45:52 +02:00
parent 4b9f11ba2a
commit a64e947cdb
8 changed files with 556 additions and 151 deletions
Download Patch File Download Diff File Expand all files Collapse all files

269
ortools/sat/cp_model_loader.cc
View File

@@ -56,6 +56,36 @@ std::vector<int64> ValuesFromProto(const Values& values) {
return std::vector<int64>(values.begin(), values.end());
}
bool ComputeLinearBounds(const LinearConstraintProto& proto,
CpModelMapping* mapping, IntegerTrail* integer_trail,
int64* sum_min, int64* sum_max) {
*sum_min = 0;
*sum_max = 0;
for (int i = 0; i < proto.vars_size(); ++i) {
const int var = proto.vars(i);
const int64 coeff = proto.coeffs(i);
const IntegerVariable sat_var = mapping->Integer(var);
const int64 lb = integer_trail->LowerBound(sat_var).value();
const int64 ub = integer_trail->UpperBound(sat_var).value();
if (lb == ub) {
return false;
}
if (coeff >= 0) {
(*sum_min) += coeff * lb;
(*sum_max) += coeff * ub;
} else {
(*sum_min) += coeff * ub;
(*sum_max) += coeff * lb;
}
}
return true;
}
// We check that it is strictly inside bounds, because
// b => sum(ai * xi) == ub(ai * xi) or lb(ai * xi)
// can be implemented without the actual sum. Therefore, there would be no need
// to fully encode in that case.
bool IsEqCstInsideBounds(const LinearConstraintProto& proto,
CpModelMapping* mapping, IntegerTrail* integer_trail) {
if (proto.domain_size() != 2 || proto.domain(0) != proto.domain(1)) {
@@ -64,55 +94,38 @@ bool IsEqCstInsideBounds(const LinearConstraintProto& proto,
int64 sum_min = 0;
int64 sum_max = 0;
for (int i = 0; i < proto.vars_size(); ++i) {
const int var = proto.vars(i);
const int64 coeff = proto.coeffs(i);
const IntegerVariable sat_var = mapping->Integer(var);
const int64 lb = integer_trail->LowerBound(sat_var).value();
const int64 ub = integer_trail->UpperBound(sat_var).value();
if (coeff >= 0) {
sum_min += coeff * lb;
sum_max += coeff * ub;
} else {
sum_min += coeff * ub;
sum_max += coeff * lb;
}
if (!ComputeLinearBounds(proto, mapping, integer_trail, &sum_min, &sum_max)) {
return false;
}
const int64 value = proto.domain(0);
return value > sum_min && value < sum_max;
}
// We check that it is strictly inside bounds, because
// b => sum(ai * xi) < ub(ai * xi) or > lb(ai * xi)
// can be implemented without the actual sum. Therefore, there would be no need
// to fully encode in that case.
bool IsNEqCstInsideBounds(const LinearConstraintProto& proto,
CpModelMapping* mapping, IntegerTrail* integer_trail,
int64* single_value) {
int64 sum_min = 0;
int64 sum_max = 0;
for (int i = 0; i < proto.vars_size(); ++i) {
const int var = proto.vars(i);
const int64 coeff = proto.coeffs(i);
const IntegerVariable sat_var = mapping->Integer(var);
const int64 lb = integer_trail->LowerBound(sat_var).value();
const int64 ub = integer_trail->UpperBound(sat_var).value();
if (coeff >= 0) {
sum_min += coeff * lb;
sum_max += coeff * ub;
} else {
sum_min += coeff * ub;
sum_max += coeff * lb;
}
if (!ComputeLinearBounds(proto, mapping, integer_trail, &sum_min, &sum_max)) {
return false;
}
if (proto.domain_size() == 4 && proto.domain(0) <= sum_min &&
proto.domain(1) + 2 == proto.domain(2) && proto.domain(3) >= sum_max) {
const Domain complement =
Domain(sum_min, sum_max)
.IntersectionWith(ReadDomainFromProto(proto).Complement());
const int64 value = complement.Min();
if (complement.Size() == 1 && value > sum_min && value < sum_max) {
if (single_value != nullptr) {
*single_value = proto.domain(1) + 1;
*single_value = value;
}
return true;
}
return false;
}
@@ -276,29 +289,30 @@ void CpModelMapping::CreateVariables(const CpModelProto& model_proto,
<< ", int_var = " << int_var_proto.DebugString()
<< ", bool_var = " << bool_var_proto.DebugString();
encoder->AssociateToIntegerEqualValue(lit, var, IntegerValue(vmin));
encoder->AssociateToIntegerEqualValue(lit.Negated(), var,
IntegerValue(vmax));
encoder->AssociateToIntegerLiteral(
lit.Negated(),
IntegerLiteral::GreaterOrEqual(var, IntegerValue(vmax)));
encoder->AssociateToIntegerLiteral(
lit, IntegerLiteral::LowerOrEqual(var, IntegerValue(vmin)));
// encoder->AssociateToIntegerEqualValue(lit.Negated(), var,
// IntegerValue(vmax));
// encoder->AssociateToIntegerLiteral(
// lit.Negated(),
// IntegerLiteral::GreaterOrEqual(var, IntegerValue(vmax)));
// encoder->AssociateToIntegerLiteral(
// lit, IntegerLiteral::LowerOrEqual(var, IntegerValue(vmin)));
} else {
CHECK_EQ(vmax - vmin, -coeff);
CHECK_EQ(vmin, rhs) << ct.DebugString()
<< ", int_var = " << int_var_proto.DebugString()
<< ", bool_var = " << bool_var_proto.DebugString();
encoder->AssociateToIntegerEqualValue(lit, var, IntegerValue(vmax));
encoder->AssociateToIntegerEqualValue(lit.Negated(), var,
IntegerValue(vmin));
encoder->AssociateToIntegerLiteral(
lit, IntegerLiteral::GreaterOrEqual(var, IntegerValue(vmax)));
encoder->AssociateToIntegerLiteral(
lit.Negated(), IntegerLiteral::LowerOrEqual(var, IntegerValue(vmin)));
// encoder->AssociateToIntegerEqualValue(lit.Negated(), var,
// IntegerValue(vmin));
// encoder->AssociateToIntegerLiteral(
// lit, IntegerLiteral::GreaterOrEqual(var, IntegerValue(vmax)));
// encoder->AssociateToIntegerLiteral(
// lit.Negated(), IntegerLiteral::LowerOrEqual(var,
// IntegerValue(vmin)));
}
// This is needed so that IsFullyEncoded() returns true.
m->GetOrCreate<IntegerEncoder>()->FullyEncodeVariable(integers_[int_var]);
encoder->FullyEncodeVariable(integers_[int_var]);
num_encoded_from_affine++;
already_loaded_ct_.insert(&ct);
}
@@ -332,7 +346,6 @@ void CpModelMapping::CreateVariables(const CpModelProto& model_proto,
already_loaded_ct_.insert(&ct);
}
}
// The logic assumes that the linear constraints have been presolved, so that
// equality with a domain bound have been converted to <= or >= and so that we
// never have any trivial inequalities.
@@ -428,6 +441,7 @@ void CpModelMapping::ExtractEncoding(const CpModelProto& model_proto,
if (!inter.IsEmpty() && inter.Min() == inter.Max()) {
var_to_equalities[var].push_back(
{&ct, enforcement_literal, inter.Min(), true});
variables_to_encoded_values_[var].insert(inter.Min());
}
}
{
@@ -436,6 +450,7 @@ void CpModelMapping::ExtractEncoding(const CpModelProto& model_proto,
if (!inter.IsEmpty() && inter.Min() == inter.Max()) {
var_to_equalities[var].push_back(
{&ct, enforcement_literal, inter.Min(), false});
variables_to_encoded_values_[var].insert(inter.Min());
}
}
}
@@ -687,6 +702,7 @@ class FullEncodingFixedPointComputer {
void FullyEncode(int v) {
v = PositiveRef(v);
VLOG(3) << "Fully encode " << v;
const IntegerVariable variable = mapping_->Integer(v);
if (v == kNoIntegerVariable) return;
if (!model_->Get(IsFixed(variable))) {
@@ -695,15 +711,6 @@ class FullEncodingFixedPointComputer {
AddVariableToPropagationQueue(v);
}
const int64 DomainSize(int v) const {
const IntegerVariableProto& proto = model_proto_.variables(v);
int64 result = 0;
for (int i = 0; i < proto.domain_size(); i += 2) {
result += proto.domain(i + 1) - proto.domain(i) + 1;
}
return result;
}
bool ProcessConstraint(ConstraintIndex ct_index);
bool ProcessElement(ConstraintIndex ct_index);
bool ProcessTable(ConstraintIndex ct_index);
@@ -726,8 +733,8 @@ class FullEncodingFixedPointComputer {
gtl::ITIVector<ConstraintIndex, bool> constraint_is_finished_;
gtl::ITIVector<ConstraintIndex, bool> constraint_is_registered_;
absl::flat_hash_map<int, absl::flat_hash_set<int64>> is_eq_cst_;
absl::flat_hash_map<int, absl::flat_hash_set<int>> is_eq_var_;
absl::flat_hash_map<int, absl::flat_hash_set<int>>
variables_to_equal_or_diff_variables_;
};
// We only add to the propagation queue variable that are fully encoded.
@@ -742,21 +749,22 @@ void FullEncodingFixedPointComputer::ComputeFixedPoint() {
ProcessConstraint(ct_index);
}
// is_eq_cst and is_eq_var are filled with target variables. Let's scan those.
std::map<int, int64> to_process;
for (const auto& var_values : is_eq_cst_) {
to_process[var_values.first] += var_values.second.size();
}
for (const auto& var_vars : is_eq_var_) {
to_process[var_vars.first] += var_vars.second.size();
std::vector<int> variable_usages(model_proto_.variables_size());
for (int i = 0; i < variable_usages.size(); ++i) {
variable_usages[i] = mapping_->NumEncodedValues(i);
if (gtl::ContainsKey(variables_to_equal_or_diff_variables_, i)) {
variable_usages[i] += variables_to_equal_or_diff_variables_[i].size();
}
}
int num_var_encoded_from_linear_accesses = 0;
for (const auto& var_size : to_process) {
const int var = var_size.first;
for (int var = 0; var < variable_usages.size(); ++var) {
if (variable_usages[var] == 0) continue;
if (IsFullyEncoded(var)) continue;
const int64 num_constraints = var_size.second;
const int64 domain_size = DomainSize(var);
const int64 num_constraints = variable_usages[var];
const int64 domain_size =
ReadDomainFromProto(model_proto_.variables(var)).Size();
if (num_constraints >= domain_size / 2) {
VLOG(3) << model_proto_.variables(var).ShortDebugString()
<< " is encoded with " << num_constraints
@@ -814,44 +822,36 @@ bool FullEncodingFixedPointComputer::ProcessElement(ConstraintIndex ct_index) {
const ConstraintProto& ct = model_proto_.constraints(ct_index.value());
// Index must always be full encoded.
VLOG(3) << "Element " << ct.DebugString() << " fully encode index "
<< ct.element().index();
FullyEncode(ct.element().index());
// TODO(user): Implement ProcessEnforcedEquality() and
// LoadEnforcedEquality() that decides what to do.
// b => left == right
// - If one var has a much smaller domain that the over one, no need to
// fully encode the other one
// - If both vars are small (add a parameter to control the size limit),
// fully encode both and add AC encoding
// - Use it for both linear and element constraints
// If target is a constant or fully encoded, variables must be fully encoded.
const int target = ct.element().target();
if (IsFullyEncoded(target)) {
for (const int v : ct.element().vars()) FullyEncode(v);
}
// // If target is a constant or fully encoded, variables must be fully
// encoded. const int target = ct.element().target(); if
// (IsFullyEncoded(target)) {
// for (const int v : ct.element().vars()) FullyEncode(v);
// }
// If all non-target variables are fully encoded, target must be too.
bool all_variables_are_fully_encoded = true;
for (const int v : ct.element().vars()) {
if (v == target) continue;
if (!IsFullyEncoded(v)) {
all_variables_are_fully_encoded = false;
break;
}
}
if (all_variables_are_fully_encoded) {
if (!IsFullyEncoded(target)) FullyEncode(target);
return true;
}
// // If all non-target variables are fully encoded, target must be too.
// bool all_variables_are_fully_encoded = true;
// for (const int v : ct.element().vars()) {
// if (v == target) continue;
// if (!IsFullyEncoded(v)) {
// all_variables_are_fully_encoded = false;
// break;
// }
// }
// if (all_variables_are_fully_encoded) {
// if (!IsFullyEncoded(target)) FullyEncode(target);
// return true;
// }
// // If some variables are not fully encoded, register on those.
// if (constraint_is_registered_[ct_index]) {
// for (const int v : ct.element().vars()) Register(ct_index, v);
// Register(ct_index, target);
// }
// return false;
return true;
// If some variables are not fully encoded, register on those.
if (constraint_is_registered_[ct_index]) {
for (const int v : ct.element().vars()) Register(ct_index, v);
Register(ct_index, target);
}
return false;
}
bool FullEncodingFixedPointComputer::ProcessTable(ConstraintIndex ct_index) {
@@ -878,6 +878,7 @@ bool FullEncodingFixedPointComputer::ProcessAutomaton(
bool FullEncodingFixedPointComputer::ProcessInverse(ConstraintIndex ct_index) {
const ConstraintProto& ct = model_proto_.constraints(ct_index.value());
VLOG(3) << "Process inverse " << ct.DebugString();
for (const int variable : ct.inverse().f_direct()) {
FullyEncode(variable);
}
@@ -893,27 +894,20 @@ bool FullEncodingFixedPointComputer::ProcessLinear(ConstraintIndex ct_index) {
return true;
}
if (ct.name() == "MAPPING") return true;
int64 value = ct.linear().domain(0);
if (!IsEqCstInsideBounds(ct.linear(), mapping_, integer_trail_) &&
!IsNEqCstInsideBounds(ct.linear(), mapping_, integer_trail_, &value)) {
return true;
}
if (ct.linear().vars_size() == 1 && ct.enforcement_literal_size() == 1) {
const int var = ct.linear().vars(0);
if (!IsFullyEncoded(var)) {
is_eq_cst_[var].insert(value);
}
} else if (ct.linear().vars_size() == 2) {
if (ct.linear().vars_size() == 2) {
const int var0 = ct.linear().vars(0);
const int var1 = ct.linear().vars(1);
if (!IsFullyEncoded(var0)) {
is_eq_var_[var0].insert(var1);
variables_to_equal_or_diff_variables_[var0].insert(var1);
}
if (!IsFullyEncoded(var1)) {
is_eq_var_[var1].insert(var0);
variables_to_equal_or_diff_variables_[var1].insert(var0);
}
}
return true;
@@ -1027,9 +1021,14 @@ void LoadEquivalenceNeqAC(const std::vector<Literal> enforcement_literal,
const IntegerValue target_value = rhs - value_literal.value * coeff2;
if (gtl::ContainsKey(term1_value_to_literal, target_value)) {
const Literal target_literal = term1_value_to_literal[target_value];
m->Add(EnforcedClause(
enforcement_literal,
{value_literal.literal.Negated(), target_literal.Negated()}));
if (enforcement_literal.empty()) {
m->Add(ClauseConstraint(
{value_literal.literal.Negated(), target_literal.Negated()}));
} else {
m->Add(EnforcedClause(
enforcement_literal,
{value_literal.literal.Negated(), target_literal.Negated()}));
}
}
}
}
@@ -1056,7 +1055,10 @@ void LoadLinearConstraint(const ConstraintProto& ct, Model* m) {
IsEqCstInsideBounds(ct.linear(), mapping, integer_trail) &&
encoder->VariableIsFullyEncoded(vars[0]) &&
encoder->VariableIsFullyEncoded(vars[1]) && max_domain_size < 64) {
VLOG(3) << "Load AC version of " << ct.DebugString();
VLOG(3) << "Load AC version of " << ct.DebugString() << ", var0 domain = "
<< integer_trail->InitialVariableDomain(vars[0])
<< ", var1 domain = "
<< integer_trail->InitialVariableDomain(vars[1]);
return LoadEquivalenceAC(mapping->Literals(ct.enforcement_literal()),
IntegerValue(coeffs[0]), vars[0],
IntegerValue(coeffs[1]), vars[1],
@@ -1067,7 +1069,10 @@ void LoadLinearConstraint(const ConstraintProto& ct, Model* m) {
&single_value) &&
encoder->VariableIsFullyEncoded(vars[0]) &&
encoder->VariableIsFullyEncoded(vars[1]) && max_domain_size < 64) {
VLOG(3) << "Load NAC version of " << ct.DebugString();
VLOG(3) << "Load NAC version of " << ct.DebugString() << ", var0 domain = "
<< integer_trail->InitialVariableDomain(vars[0])
<< ", var1 domain = "
<< integer_trail->InitialVariableDomain(vars[1]);
return LoadEquivalenceNeqAC(mapping->Literals(ct.enforcement_literal()),
IntegerValue(coeffs[0]), vars[0],
IntegerValue(coeffs[1]), vars[1],
@@ -1484,23 +1489,10 @@ void LoadBooleanElement(const ConstraintProto& ct, Model* m) {
void LoadElementConstraint(const ConstraintProto& ct, Model* m) {
auto* mapping = m->GetOrCreate<CpModelMapping>();
auto* integer_trail = m->GetOrCreate<IntegerTrail>();
const IntegerVariable index = mapping->Integer(ct.element().index());
const IntegerVariable target = mapping->Integer(ct.element().target());
const int64 index_min =
std::max<int64>(0, integer_trail->LowerBound(index).value());
const int64 index_max = std::min<int64>(
integer_trail->UpperBound(index).value(), ct.element().vars_size() - 1);
const int64 target_min = integer_trail->LowerBound(target).value();
const int64 target_max = integer_trail->UpperBound(target).value();
VLOG(3) << "Element index has range " << index_min << ".." << index_max;
VLOG(3) << "Element target has range " << target_min << ".." << target_max;
bool boolean_array = true;
for (int i = index_min; i <= index_max; ++i) {
const int ref = ct.element().vars(i);
for (const int ref : ct.element().vars()) {
if (!mapping->IsBoolean(ref)) {
boolean_array = false;
break;
@@ -1515,11 +1507,11 @@ void LoadElementConstraint(const ConstraintProto& ct, Model* m) {
// TODO(user): Move this to presolve. Leads to a larger discussion on
// adding full encoding to model during presolve.
if (boolean_array) {
VLOG(3) << "Load Boolean Element " << ct.DebugString();
LoadBooleanElement(ct, m);
return;
}
const IntegerVariable target = mapping->Integer(ct.element().target());
const std::vector<IntegerVariable> vars =
mapping->Integers(ct.element().vars());
@@ -1544,7 +1536,6 @@ void LoadElementConstraint(const ConstraintProto& ct, Model* m) {
// Special case when target is fixed.
if (m->Get(IsFixed(target))) {
VLOG(3) << "Load Element Constraint Bounds " << ct.DebugString();
return LoadElementConstraintBounds(ct, m);
}
@@ -1553,9 +1544,7 @@ void LoadElementConstraint(const ConstraintProto& ct, Model* m) {
int num_AC_variables = 0;
const int num_vars = ct.element().vars().size();
for (int i = index_min; i <= index_max; ++i) {
const int v = ct.element().vars(i);
for (const int v : ct.element().vars()) {
IntegerVariable variable = mapping->Integer(v);
const bool is_full =
m->Get(IsFixed(variable)) || encoder->VariableIsFullyEncoded(variable);
@@ -1564,17 +1553,13 @@ void LoadElementConstraint(const ConstraintProto& ct, Model* m) {
const SatParameters& params = *m->GetOrCreate<SatParameters>();
if (params.boolean_encoding_level() > 0 &&
(target_is_AC || num_AC_variables >= num_vars - 1) &&
(target_max - target_min + 1 <= 16)) {
(target_is_AC || num_AC_variables >= num_vars - 1)) {
if (params.boolean_encoding_level() > 1) {
VLOG(3) << "Load Element AC " << ct.DebugString();
LoadElementConstraintAC(ct, m);
} else {
VLOG(3) << "Load Element Half AC " << ct.DebugString();
LoadElementConstraintHalfAC(ct, m);
}
} else {
VLOG(3) << "Load Element Bounds " << ct.DebugString();
LoadElementConstraintBounds(ct, m);
}
}

10
ortools/sat/cp_model_loader.h
View File

@@ -160,6 +160,13 @@ class CpModelMapping {
return result;
}
int NumEncodedValues(int var) {
if (gtl::ContainsKey(variables_to_encoded_values_, var)) {
return variables_to_encoded_values_[var].size();
}
return 0;
}
private:
// Note that only the variables used by at least one constraint will be
// created, the other will have a kNo[Integer,Interval,Boolean]VariableValue.
@@ -177,6 +184,9 @@ class CpModelMapping {
// ExtractEncoding().
absl::flat_hash_set<const ConstraintProto*> already_loaded_ct_;
absl::flat_hash_set<const ConstraintProto*> is_half_encoding_ct_;
absl::flat_hash_map<int, absl::flat_hash_set<int64>>
variables_to_encoded_values_;
};
// Inspects the model and use some heuristic to decide which variable, if any,

1
ortools/sat/cp_model_presolve.cc
View File

@@ -4287,7 +4287,6 @@ void CpModelPresolver::RemoveUnusedEquivalentVariables() {
}
ConstraintProto* ct = proto->add_constraints();
ct->set_name("MAPPING");
auto* arg = ct->mutable_linear();
arg->add_vars(var);
arg->add_coeffs(1);

5
ortools/sat/linear_programming_constraint.cc
View File

@@ -2158,9 +2158,8 @@ LinearProgrammingConstraint::HeuristicLPPseudoCostBinary(Model* model) {
std::function<LiteralIndex()>
LinearProgrammingConstraint::LPReducedCostAverageBranching() {
if (!compute_reduced_cost_averages_) {
compute_reduced_cost_averages_ = true;
const int num_vars = integer_variables_.size();
const int num_vars = integer_variables_.size();
if (sum_cost_down_.size() < num_vars) {
VLOG(1) << " LPReducedCostAverageBranching has #variables: " << num_vars;
sum_cost_down_.resize(num_vars, 0.0);
num_cost_down_.resize(num_vars, 0);

138
ortools/sat/samples/MultipleKnapsackSat.java Normal file
View File

@@ -0,0 +1,138 @@
// 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.
// [START program]
// [START import]
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;
// [END import]
/** Sample showing how to solve a multiple knapsack problem. */
public class MultipleKnapsackSat {
static {
System.loadLibrary("jniortools");
}
// [START data]
static class DataModel {
int[] items = new int[] {48, 30, 42, 36, 36, 48, 42, 42, 36, 24, 30, 30, 42, 36, 36};
int[] values = new int[] {10, 30, 25, 50, 35, 30, 15, 40, 30, 35, 45, 10, 20, 30, 25};
int[] binCapacities = new int[] {100, 100, 100, 100, 100};
int numItems = items.length;
int numBins = 5;
}
// [END data]
// [START solution_printer]
static void printSolution(
DataModel data, CpSolver solver, IntVar[][] x, IntVar[] load, IntVar[] value) {
System.out.printf("Optimal objective value: %f%n", solver.objectiveValue());
System.out.println();
long packedWeight = 0;
long packedValue = 0;
for (int b = 0; b < data.numBins; ++b) {
System.out.println("Bin " + b);
for (int i = 0; i < data.numItems; ++i) {
if (solver.value(x[i][b]) > 0) {
System.out.println(
"Item " + i + " - Weight: " + data.items[i] + " Value: " + data.values[i]);
}
}
System.out.println("Packed bin weight: " + solver.value(load[b]));
packedWeight = packedWeight + solver.value(load[b]);
System.out.println("Packed bin value: " + solver.value(value[b]) + "\n");
packedValue = packedValue + solver.value(value[b]);
}
System.out.println("Total packed weight: " + packedWeight);
System.out.println("Total packed value: " + packedValue);
}
public static void main(String[] args) {
// Instantiate the data problem.
// [START data]
final DataModel data = new DataModel();
// [END data]
int totalValue = 0;
for (int i = 0; i < data.numItems; ++i) {
totalValue = totalValue + data.values[i];
}
// [START model]
CpModel model = new CpModel();
// [END model]
// [START variables]
IntVar[][] x = new IntVar[data.numItems][data.numBins];
for (int i = 0; i < data.numItems; ++i) {
for (int b = 0; b < data.numBins; ++b) {
x[i][b] = model.newIntVar(0, 1, "x_" + i + "_" + b);
}
}
// Main variables.
// Load and value variables.
IntVar[] load = new IntVar[data.numBins];
IntVar[] value = new IntVar[data.numBins];
for (int b = 0; b < data.numBins; ++b) {
load[b] = model.newIntVar(0, data.binCapacities[b], "load_" + b);
value[b] = model.newIntVar(0, totalValue, "value_" + b);
}
// Links load and value with x.
int[] sizes = new int[data.numItems];
for (int i = 0; i < data.numItems; ++i) {
sizes[i] = data.items[i];
}
for (int b = 0; b < data.numBins; ++b) {
IntVar[] vars = new IntVar[data.numItems];
for (int i = 0; i < data.numItems; ++i) {
vars[i] = x[i][b];
}
model.addEquality(LinearExpr.scalProd(vars, data.items), load[b]);
model.addEquality(LinearExpr.scalProd(vars, data.values), value[b]);
}
// [END variables]
// [START constraints]
// Each item can be in at most one bin.
// Place all items.
for (int i = 0; i < data.numItems; ++i) {
IntVar[] vars = new IntVar[data.numBins];
for (int b = 0; b < data.numBins; ++b) {
vars[b] = x[i][b];
}
model.addLessOrEqual(LinearExpr.sum(vars), 1);
}
// [END constraints]
// Maximize sum of load.
// [START objective]
model.maximize(LinearExpr.sum(value));
// [END objective]
// [START solve]
CpSolver solver = new CpSolver();
CpSolverStatus status = solver.solve(model);
// [END solve]
// [START print_solution]
System.out.println("Solve status: " + status);
if (status == CpSolverStatus.OPTIMAL) {
printSolution(data, solver, x, load, value);
}
// [END print_solution]
}
private MultipleKnapsackSat() {}
}

148
ortools/sat/samples/multiple_knapsack_sat.cc Normal file
View File

@@ -0,0 +1,148 @@
// 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.
// [START program]
// [START import]
#include "ortools/sat/cp_model.h"
// [END import]
namespace operations_research {
namespace sat {
// [START data_model]
struct DataModel {
const std::vector<int> weights = {{
48,
30,
42,
36,
36,
48,
42,
42,
36,
24,
30,
30,
42,
36,
36,
}};
const std::vector<int> values = {
{10, 30, 25, 50, 35, 30, 15, 40, 30, 35, 45, 10, 20, 30, 25}};
const int num_items = weights.size();
const int total_value = accumulate(values.begin(), values.end(), 0);
const std::vector<int> kBinCapacities = {{100, 100, 100, 100, 100}};
const int kNumBins = 5;
};
// [END data_model]
// [START solution_printer]
void PrintSolution(const DataModel data,
const std::vector<std::vector<IntVar>> x,
const std::vector<IntVar> load,
const std::vector<IntVar> value,
const CpSolverResponse response) {
for (int b = 0; b < data.kNumBins; ++b) {
LOG(INFO) << "Bin " << b;
LOG(INFO);
for (int i = 0; i < data.num_items; ++i) {
if (SolutionIntegerValue(response, x[i][b]) > 0) {
LOG(INFO) << "Item " << i << " - Weight: " << data.weights[i]
<< " Value: " << data.values[i];
}
}
LOG(INFO) << "Packed bin weight: "
<< SolutionIntegerValue(response, load[b]);
LOG(INFO) << "Packed bin value: "
<< SolutionIntegerValue(response, value[b]);
LOG(INFO);
}
LOG(INFO) << "Total packed weight: "
<< SolutionIntegerValue(response, LinearExpr::Sum(load));
LOG(INFO) << "Total packed value: "
<< SolutionIntegerValue(response, LinearExpr::Sum(value));
}
// [END solution_printer]
void MultipleKnapsackSat() {
// [START data]
DataModel data;
// [END data]
// [START model]
CpModelBuilder cp_model;
// [END model]
// [START variables]
// Main variables.
std::vector<std::vector<IntVar>> x(data.num_items);
for (int i = 0; i < data.num_items; ++i) {
for (int b = 0; b < data.kNumBins; ++b) {
x[i].push_back(cp_model.NewIntVar({0, 1}));
}
}
// Load variables.
std::vector<IntVar> load(data.kNumBins);
std::vector<IntVar> value(data.kNumBins);
for (int b = 0; b < data.kNumBins; ++b) {
load[b] = cp_model.NewIntVar({0, data.kBinCapacities[b]});
value[b] = cp_model.NewIntVar({0, data.total_value});
}
// Links load and x.
for (int b = 0; b < data.kNumBins; ++b) {
LinearExpr weightsExpr;
LinearExpr valuesExpr;
for (int i = 0; i < data.num_items; ++i) {
weightsExpr.AddTerm(x[i][b], data.weights[i]);
valuesExpr.AddTerm(x[i][b], data.values[i]);
}
cp_model.AddEquality(weightsExpr, load[b]);
cp_model.AddEquality(valuesExpr, value[b]);
}
// [END variables]
// [START constraints]
// Each item can be in at most one bin.
for (int i = 0; i < data.num_items; ++i) {
LinearExpr expr;
for (int b = 0; b < data.kNumBins; ++b) {
expr.AddTerm(x[i][b], 1);
}
cp_model.AddLessOrEqual(expr, 1);
}
// [END constraints]
// Maximize sum of load.
// [START objective]
cp_model.Maximize(LinearExpr::Sum(value));
// [END objective]
// [START solve]
const CpSolverResponse response = Solve(cp_model.Build());
// [END solve]
// [START print_solution]
PrintSolution(data, x, load, value, response);
// [END print_solution]
}
} // namespace sat
} // namespace operations_research
int main() {
operations_research::sat::MultipleKnapsackSat();
return EXIT_SUCCESS;
}
// [END program]

129
ortools/sat/samples/multiple_knapsack_sat.py Normal file
View File

@@ -0,0 +1,129 @@
# 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.
# [START program]
"""Solves a multiple knapsack problem using the CP-SAT solver."""
# [START import]
from __future__ import absolute_import
from __future__ import division
from __future__ import print_function
from ortools.sat.python import cp_model
# [END import]
# [START data_model]
def create_data_model():
"""Create the data for the example."""
data = {}
weights = [48, 30, 42, 36, 36, 48, 42, 42, 36, 24, 30, 30, 42, 36, 36]
values = [10, 30, 25, 50, 35, 30, 15, 40, 30, 35, 45, 10, 20, 30, 25]
data['num_items'] = len(weights)
data['all_items'] = range(data['num_items'])
data['weights'] = weights
data['values'] = values
data['bin_capacities'] = [100, 100, 100, 100, 100]
data['num_bins'] = len(data['bin_capacities'])
data['all_bins'] = range(data['num_bins'])
return data
# [END data_model]
# [START solution_printer]
def print_solutions(data, solver, x):
"""Display the solution."""
total_weight = 0
total_value = 0
for b in data['all_bins']:
print('Bin', b, '\n')
bin_weight = 0
bin_value = 0
for idx, val in enumerate(data['weights']):
if solver.Value(x[(idx, b)]) > 0:
print('Item', idx, '- Weight:', val, ' Value:',
data['values'][idx])
bin_weight += val
bin_value += data['values'][idx]
print('Packed bin weight:', bin_weight)
print('Packed bin value:', bin_value, '\n')
total_weight += bin_weight
total_value += bin_value
print('Total packed weight:', total_weight)
print('Total packed value:', total_value)
# [END solution_printer]
def main():
# [START data]
data = create_data_model()
# [END data]
# [START model]
model = cp_model.CpModel()
# [END model]
# Main variables.
# [START variables]
x = {}
for idx in data['all_items']:
for b in data['all_bins']:
x[(idx, b)] = model.NewIntVar(0, 1, 'x_%i_%i' % (idx, b))
max_value = sum(data['values'])
# value[b] is the value of bin b when packed.
value = [
model.NewIntVar(0, max_value, 'value_%i' % b) for b in data['all_bins']
]
for b in data['all_bins']:
model.Add(value[b] == sum(
x[(i, b)] * data['values'][i] for i in data['all_items']))
# [END variables]
# [START constraints]
# Each item can be in at most one bin.
for idx in data['all_items']:
model.Add(sum(x[idx, b] for b in data['all_bins']) <= 1)
# The amount packed in each bin cannot exceed its capacity.
for b in data['all_bins']:
model.Add(
sum(x[(i, b)] * data['weights'][i]
for i in data['all_items']) <= data['bin_capacities'][b])
# [END constraints]
# [START objective]
# Maximize total value of packed items.
model.Maximize(sum(value))
# [END objective]
# [START solver]
solver = cp_model.CpSolver()
# [END solver]
# [START solve]
status = solver.Solve(model)
# [END solve]
# [START print_solution]
if status == cp_model.OPTIMAL:
print_solutions(data, solver, x)
# [END solutions_printer]
if __name__ == '__main__':
main()
# [END program]

7
ortools/sat/synchronization.cc
View File

@@ -398,12 +398,9 @@ void SharedResponseManager::SetStatsFromModelInternal(Model* model) {
bool SharedResponseManager::ProblemIsSolved() const {
absl::MutexLock mutex_lock(&mutex_);
// TODO(user): Currently this work because we do not allow enumerate all
// solution in multithread.
if (!model_proto_.has_objective() &&
((best_response_.status() == CpSolverStatus::FEASIBLE &&
!enumerate_all_solutions_) ||
best_response_.status() == CpSolverStatus::OPTIMAL)) {
best_response_.status() == CpSolverStatus::FEASIBLE &&
!enumerate_all_solutions_) {
return true;
}