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

change CP-SAT C++ Api to call Build() on the model before solving; use log_search_progress parameters to display all log; enable this parameter in non C++ language; call InitGoogleLogging() automatically in non C++ languages

Browse Source
This commit is contained in:
Laurent Perron
2019-04-05 14:58:33 +02:00
parent d1d1c01df4
commit 17b9b597a1
40 changed files with 197 additions and 129 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
examples/cpp/costas_array_sat.cc
View File

@@ -116,7 +116,7 @@ void CostasHard(const int dim) {
if (!FLAGS_params.empty()) {
model.Add(NewSatParameters(FLAGS_params));
}
const CpSolverResponse response = SolveWithModel(cp_model, &model);
const CpSolverResponse response = SolveWithModel(cp_model.Build(), &model);
if (response.status() == CpSolverStatus::FEASIBLE) {
std::vector<int64> costas_matrix;
@@ -183,7 +183,7 @@ void CostasBool(const int dim) {
if (!FLAGS_params.empty()) {
model.Add(NewSatParameters(FLAGS_params));
}
const CpSolverResponse response = SolveWithModel(cp_model, &model);
const CpSolverResponse response = SolveWithModel(cp_model.Build(), &model);
if (response.status() == CpSolverStatus::FEASIBLE) {
std::vector<int64> costas_matrix;
@@ -265,7 +265,7 @@ void CostasBoolSoft(const int dim) {
if (!FLAGS_params.empty()) {
model.Add(NewSatParameters(FLAGS_params));
}
const CpSolverResponse response = SolveWithModel(cp_model, &model);
const CpSolverResponse response = SolveWithModel(cp_model.Build(), &model);
if (response.status() == CpSolverStatus::OPTIMAL) {
std::vector<int64> costas_matrix;

2
examples/cpp/golomb_sat.cc
View File

@@ -92,7 +92,7 @@ void GolombRuler(int size) {
<< FLAGS_params;
}
model.Add(NewSatParameters(parameters));
const CpSolverResponse response = SolveWithModel(cp_model, &model);
const CpSolverResponse response = SolveWithModel(cp_model.Build(), &model);
if (response.status() == CpSolverStatus::OPTIMAL) {
const int64 result = SolutionIntegerValue(response, ticks.back());

2
examples/cpp/jobshop_sat.cc
View File

@@ -339,7 +339,7 @@ void Solve(const JsspInputProblem& problem) {
Model model;
model.Add(NewSatParameters(FLAGS_params));
const CpSolverResponse response = SolveWithModel(cp_model, &model);
const CpSolverResponse response = SolveWithModel(cp_model.Build(), &model);
LOG(INFO) << CpSolverResponseStats(response);
// Check cost, recompute it from scratch.

2
examples/cpp/magic_square_sat.cc
View File

@@ -72,7 +72,7 @@ void MagicSquare(int size) {
Model model;
model.Add(NewSatParameters(FLAGS_params));
const CpSolverResponse response = SolveWithModel(builder, &model);
const CpSolverResponse response = SolveWithModel(builder.Build(), &model);
if (response.status() == CpSolverStatus::FEASIBLE) {
for (int n = 0; n < size; ++n) {

27
examples/cpp/multi_knapsack_sat.cc
View File

@@ -37,8 +37,8 @@ static const int kVolumeMin = 1156;
static const int kVolumeMax = 1600;
// data for a single bin problem
static const int kItemsValues[] = {1008, 2087, 5522, 5250, 5720, 4998, 275, 3145, 12580, 382};
static const int kItemsWeights[] = {1008, 2087, 5522, 5250, 5720, 4998, 275, 3145, 12580, 382};
static const int kItemsWeights[] = {1008, 2087, 5522, 5250, 5720,
4998, 275, 3145, 12580, 382};
static const int kItemsVolumes[] = {281, 307, 206, 111, 275, 79, 23, 65, 261, 40};
static const int kNumItems = 10;
@@ -61,21 +61,21 @@ void MultiKnapsackSat(int scaling, const std::string& params) {
}
// Fill up scaled values, weights, volumes;
std::vector<int64> values(num_items);
std::vector<int64> weights(num_items);
std::vector<int64> volumes(num_items);
for (int i = 0; i < num_items; ++i) {
const int index = i % kNumItems;
values[i] = kItemsValues[index];
weights[i] = kItemsWeights[index];
volumes[i] = kItemsVolumes[index];
}
// Constraints per bins.
std::vector<IntVar> bin_weights;
for (int b = 0; b < num_bins; ++b) {
builder.AddLinearConstraint(
LinearExpr::BooleanScalProd(items_in_bins[b], weights),
{kWeightMin, kWeightMax});
IntVar bin_weight = builder.NewIntVar({kWeightMin, kWeightMax});
bin_weights.push_back(bin_weight);
builder.AddEquality(
LinearExpr::BooleanScalProd(items_in_bins[b], weights), bin_weight);
builder.AddLinearConstraint(
LinearExpr::BooleanScalProd(items_in_bins[b], volumes),
{kVolumeMin, kVolumeMax});
@@ -90,16 +90,21 @@ void MultiKnapsackSat(int scaling, const std::string& params) {
builder.AddEquality(LinearExpr::BooleanSum(copies), selected_items[i]);
}
// Symmetry breaking. Weights are decreasing accross bins.
// for (int b = 0; b + 1 < num_bins; ++b) {
// builder.AddGreaterOrEqual(bin_weights[b], bin_weights[b + 1]);
// }
// Maximize value.
builder.Maximize(LinearExpr::BooleanScalProd(selected_items, values));
builder.Maximize(LinearExpr::Sum(bin_weights));
// And solve.
Model model;
if (!params.empty()) {
model.Add(NewSatParameters(params));
}
const CpSolverResponse response = SolveWithModel(builder, &model);
LOG(INFO) << CpSolverResponseStats(response);
const CpSolverResponse response = SolveWithModel(builder.Build(), &model);
LOG(INFO) << CpSolverResponseStats(response);
}
} // namespace sat
@@ -109,4 +114,4 @@ int main(int argc, char **argv) {
gflags::ParseCommandLineFlags(&argc, &argv, true);
operations_research::sat::MultiKnapsackSat(FLAGS_size, FLAGS_params);
return EXIT_SUCCESS;
}
}

4
examples/cpp/network_routing_sat.cc
View File

@@ -398,7 +398,7 @@ class NetworkRoutingSolver {
parameters.set_enumerate_all_solutions(true);
model.Add(NewSatParameters(parameters));
SolveWithModel(cp_model, &model);
SolveWithModel(cp_model.Build(), &model);
}
// This method will fill the all_paths_ data structure. all_paths
@@ -643,7 +643,7 @@ class NetworkRoutingSolver {
}
num_solutions++;
}));
const CpSolverResponse response = SolveWithModel(cp_model, &model);
const CpSolverResponse response = SolveWithModel(cp_model.Build(), &model);
return response.objective_value();
}

2
examples/cpp/shift_minimization_sat.cc
View File

@@ -294,7 +294,7 @@ void LoadAndSolve(const std::string& file_name) {
Model model;
model.Add(NewSatParameters(FLAGS_params));
const CpSolverResponse response = SolveWithModel(cp_model, &model);
const CpSolverResponse response = SolveWithModel(cp_model.Build(), &model);
LOG(INFO) << CpSolverResponseStats(response);
}
} // namespace sat

2
examples/cpp/slitherlink_sat.cc
View File

@@ -217,7 +217,7 @@ void SlitherLink(const std::vector<std::vector<int>> &data) {
builder.AddEquality(vertical_arcs[2 * right_arc + 1], 0);
}
const CpSolverResponse response = Solve(builder);
const CpSolverResponse response = Solve(builder.Build());
std::vector<std::vector<bool>> h_arcs(num_rows + 1);
for (int y = 0; y < num_rows + 1; ++y) {

4
examples/cpp/sports_scheduling_sat.cc
View File

@@ -164,7 +164,7 @@ void FirstModel(int num_teams) {
model.Add(NewSatParameters(FLAGS_params));
}
const CpSolverResponse response = SolveWithModel(builder, &model);
const CpSolverResponse response = SolveWithModel(builder.Build(), &model);
LOG(INFO) << CpSolverResponseStats(response);
if (response.status() == CpSolverStatus::OPTIMAL ||
@@ -309,7 +309,7 @@ void SecondModel(int num_teams) {
model.Add(NewSatParameters(FLAGS_params));
}
const CpSolverResponse response = SolveWithModel(builder, &model);
const CpSolverResponse response = SolveWithModel(builder.Build(), &model);
LOG(INFO) << CpSolverResponseStats(response);
}

2
examples/cpp/variable_intervals_sat.cc
View File

@@ -58,7 +58,7 @@ void Solve() {
}
}));
SolveWithModel(cp_model, &model);
SolveWithModel(cp_model.Build(), &model);
LOG(INFO) << "Number of solutions found: " << num_solutions;
}

2
examples/cpp/weighted_tardiness_sat.cc
View File

@@ -207,7 +207,7 @@ void Solve(const std::vector<int64>& durations,
}));
// Solve.
const CpSolverResponse response = SolveWithModel(cp_model, &model);
const CpSolverResponse response = SolveWithModel(cp_model.Build(), &model);
LOG(INFO) << CpSolverResponseStats(response);
}

1
examples/python/jobshop_ft06_sat.py
View File

@@ -85,6 +85,7 @@ def jobshop_ft06():
# Solve model.
solver = cp_model.CpSolver()
solver.parameters.log_search_progress = True
status = solver.Solve(model)
# Output solution.

16
examples/tests/cp_model_test.py
View File

@@ -559,6 +559,21 @@ class CpModelTest(object):
self.assertEqual(4, solution_counter.solution_count())
def testSequentialSolve(self):
print('testSequentialSolve')
model = cp_model.CpModel()
t = model.NewBoolVar('t')
a = model.NewBoolVar('a')
b = model.NewBoolVar('b')
model.AddBoolAnd([a, b]).OnlyEnforceIf(t)
model.Add(t == 1).OnlyEnforceIf([a, b])
solver = cp_model.CpSolver()
status1 = solver.Solve(model)
status2 = solver.Solve(model)
self.assertEqual(status1, status2)
if __name__ == '__main__':
cp_model_test = CpModelTest()
cp_model_test.testCreateIntegerVariable()
@@ -604,3 +619,4 @@ if __name__ == '__main__':
cp_model_test.testDisplayBounds()
cp_model_test.testIntegerExpressionErrors()
cp_model_test.testLinearizedBoolAndEqual()
cp_model_test.testSequentialSolve()

9
ortools/sat/BUILD
View File

@@ -41,11 +41,12 @@ cc_library(
hdrs = ["cp_model.h"],
visibility = ["//visibility:public"],
deps = [
":cp_model_cc_proto",
":cp_model_solver",
":cp_model_utils",
":model",
":sat_parameters_cc_proto",
"//ortools/base:map_util",
"//ortools/sat:cp_model_cc_proto",
"//ortools/sat:cp_model_solver",
"//ortools/sat:cp_model_utils",
"//ortools/sat:model",
"//ortools/util:sorted_interval_list",
"@com_google_absl//absl/container:flat_hash_map",
"@com_google_absl//absl/strings:str_format",

24
ortools/sat/cp_model.cc
View File

@@ -15,7 +15,9 @@
#include "absl/strings/str_format.h"
#include "ortools/base/map_util.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_solver.h"
#include "ortools/sat/cp_model_utils.h"
#include "ortools/sat/sat_parameters.pb.h"
namespace operations_research {
namespace sat {
@@ -724,13 +726,27 @@ void CpModelBuilder::AddDecisionStrategy(
proto->set_domain_reduction_strategy(domain_strategy);
}
CpSolverResponse Solve(CpModelBuilder cp_model) {
CpSolverResponse Solve(const CpModelProto& model_proto) {
Model model;
return SolveCpModel(cp_model.Proto(), &model);
return SolveCpModel(model_proto, &model);
}
CpSolverResponse SolveWithModel(CpModelBuilder cp_model, Model* model) {
return SolveCpModel(cp_model.Proto(), model);
CpSolverResponse SolveWithModel(const CpModelProto& model_proto, Model* model) {
return SolveCpModel(model_proto, model);
}
CpSolverResponse SolveWithParameters(const CpModelProto& model_proto,
const SatParameters& params) {
Model model;
model.Add(NewSatParameters(params));
return SolveCpModel(model_proto, &model);
}
CpSolverResponse SolveWithParameters(const CpModelProto& model_proto,
const std::string& params) {
Model model;
model.Add(NewSatParameters(params));
return SolveCpModel(model_proto, &model);
}
int64 SolutionIntegerValue(const CpSolverResponse& r, const LinearExpr& expr) {

17
ortools/sat/cp_model.h
View File

@@ -41,6 +41,7 @@
#include "ortools/sat/cp_model_solver.h"
#include "ortools/sat/cp_model_utils.h"
#include "ortools/sat/model.h"
#include "ortools/sat/sat_parameters.pb.h"
#include "ortools/util/sorted_interval_list.h"
namespace operations_research {
@@ -679,6 +680,8 @@ class CpModelBuilder {
// TODO(user) : add MapDomain?
const CpModelProto& Build() const { return Proto(); }
const CpModelProto& Proto() const { return cp_model_; }
CpModelProto* MutableProto() { return &cp_model_; }
@@ -705,11 +708,21 @@ class CpModelBuilder {
};
// Solves the current cp_model and returns an instance of CpSolverResponse.
CpSolverResponse Solve(CpModelBuilder cp_model);
CpSolverResponse Solve(const CpModelProto& model_proto);
// Solves the current cp_model within the given model, and returns an
// instance of CpSolverResponse.
CpSolverResponse SolveWithModel(CpModelBuilder cp_model, Model* model);
CpSolverResponse SolveWithModel(const CpModelProto& model_proto, Model* model);
// Solves the current cp_model with the give sat parameters, and returns an
// instance of CpSolverResponse.
CpSolverResponse SolveWithParameters(const CpModelProto& model_proto,
const SatParameters& params);
// Solves the current cp_model with the given sat parameters as std::string in
// JSon format, and returns an instance of CpSolverResponse.
CpSolverResponse SolveWithParameters(const CpModelProto& model_proto,
const std::string& params);
// Evaluates the value of an linear expression in a solver response.
int64 SolutionIntegerValue(const CpSolverResponse& r, const LinearExpr& expr);

74
ortools/sat/cp_model_solver.cc
View File

@@ -105,10 +105,22 @@ DEFINE_double(max_drat_time_in_seconds, std::numeric_limits<double>::infinity(),
DEFINE_bool(cp_model_check_intermediate_solutions, false,
"When true, all intermediate solutions found by the solver will be "
"checked. This can be expensive, therefore it is off by default.");
DECLARE_bool(log_prefix);
DECLARE_bool(logtostderr);
namespace operations_research {
namespace sat {
void FixFlagsAndEnvironmentForSwig() {
static bool initialized = false;
if (!initialized) {
google::InitGoogleLogging("swig_helper");
initialized = true;
}
FLAGS_logtostderr = true;
FLAGS_log_prefix = false;
}
namespace {
// =============================================================================
@@ -1216,12 +1228,15 @@ CpSolverResponse SolveCpModelInternal(
external_solution_observer,
SharedBoundsManager* shared_bounds_manager, WallTimer* wall_timer,
Model* model) {
const bool log_search =
model->GetOrCreate<SatParameters>()->log_search_progress() ||
VLOG_IS_ON(1);
const bool worker_is_in_parallel_search = model->Get<WorkerInfo>() != nullptr;
const bool is_lns = model->GetOrCreate<SatParameters>()->use_lns();
if (!worker_is_in_parallel_search && is_real_solve && !is_lns) {
VLOG(1) << absl::StrFormat("*** starting to load the model at %.2fs",
wall_timer->Get());
if (!worker_is_in_parallel_search && is_real_solve && !is_lns && log_search) {
LOG(INFO) << absl::StrFormat("*** starting to load the model at %.2fs",
wall_timer->Get());
}
// Initialize a default invalid response.
CpSolverResponse response;
@@ -1475,7 +1490,7 @@ CpSolverResponse SolveCpModelInternal(
// Watch improved objective best bounds in regular search, or core based
// search. It should be disabled for LNS.
RegisterObjectiveBestBoundExport(model_proto, VLOG_IS_ON(1), objective_var,
RegisterObjectiveBestBoundExport(model_proto, log_search, objective_var,
wall_timer, model);
}
@@ -1495,9 +1510,9 @@ CpSolverResponse SolveCpModelInternal(
model);
}
if (!worker_is_in_parallel_search && is_real_solve && !is_lns) {
VLOG(1) << absl::StrFormat("*** starting sequential search at %.2fs",
wall_timer->Get());
if (!worker_is_in_parallel_search && is_real_solve && !is_lns && log_search) {
LOG(INFO) << absl::StrFormat("*** starting sequential search at %.2fs",
wall_timer->Get());
}
// Load solution hint.
@@ -2248,6 +2263,9 @@ CpSolverResponse SolveCpModelParallel(
absl::Notification first_solution_found_or_search_finished;
const int num_search_workers = params.num_search_workers();
const bool log_search =
model->GetOrCreate<SatParameters>()->log_search_progress() ||
VLOG_IS_ON(1);
// Collect per-worker parameters and names.
std::vector<SatParameters> worker_parameters;
@@ -2259,8 +2277,7 @@ CpSolverResponse SolveCpModelParallel(
worker_names.push_back(worker_name);
worker_parameters.push_back(local_params);
}
VLOG(1) << absl::StrFormat(
LOG_IF(INFO, log_search) << absl::StrFormat(
"*** starting parallel search at %.2fs with %i workers: [ %s ]",
wall_timer->Get(), num_search_workers, absl::StrJoin(worker_names, ", "));
@@ -2274,7 +2291,8 @@ CpSolverResponse SolveCpModelParallel(
const SatParameters local_params = worker_parameters[worker_id];
pool.Schedule([&model_proto, stopped, local_params, &best_response,
&mutex, worker_name, worker_id, wall_timer]() {
&mutex, worker_name, worker_id, wall_timer,
log_search]() {
Model local_model;
local_model.Add(NewSatParameters(local_params));
local_model.GetOrCreate<TimeLimit>()->RegisterExternalBooleanAsLimit(
@@ -2295,8 +2313,8 @@ CpSolverResponse SolveCpModelParallel(
}
if (local_response.status() != CpSolverStatus::UNKNOWN) {
CHECK_EQ(local_response.status(), best_response.status());
VLOG(1) << absl::StrFormat("#1 %6.2fs %s", wall_timer->Get(),
worker_name);
LOG_IF(INFO, log_search) << absl::StrFormat(
"#1 %6.2fs %s", wall_timer->Get(), worker_name);
*stopped = true;
}
});
@@ -2373,7 +2391,8 @@ CpSolverResponse SolveCpModelParallel(
set_objective_best_bound, stopped, local_params, worker_id,
&mutex, &best_response, num_search_workers, random_seed,
wall_timer, &first_solution_found_or_search_finished,
&shared_bounds_manager, maximize, worker_name]() {
&shared_bounds_manager, maximize, worker_name,
log_search]() {
Model local_model;
local_model.Add(NewSatParameters(local_params));
local_model.GetOrCreate<TimeLimit>()->RegisterExternalBooleanAsLimit(
@@ -2415,11 +2434,11 @@ CpSolverResponse SolveCpModelParallel(
// called.
{
absl::MutexLock lock(&mutex);
VLOG(1) << "*** worker '" << worker_name
<< "' terminates with status "
<< ProtoEnumToString<CpSolverStatus>(thread_response.status())
<< " and an objective value of "
<< thread_response.objective_value();
LOG_IF(INFO, log_search)
<< "*** worker '" << worker_name << "' terminates with status "
<< ProtoEnumToString<CpSolverStatus>(thread_response.status())
<< " and an objective value of "
<< thread_response.objective_value();
MergeOptimizationSolution(thread_response, maximize, &best_response);
@@ -2485,6 +2504,7 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
// TODO(user): Support solution hint, but then the first TODO will make it
// automatic.
const SatParameters& params = *model->GetOrCreate<SatParameters>();
const bool log_search = params.log_search_progress() || VLOG_IS_ON(1);
if (!model_proto.has_objective() && !model_proto.has_solution_hint() &&
!params.enumerate_all_solutions() && !params.use_lns()) {
bool is_pure_sat = true;
@@ -2507,23 +2527,23 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
}
// Starts by expanding some constraints if needed.
VLOG(1) << absl::StrFormat("*** starting model expansion at %.2fs",
wall_timer.Get());
LOG_IF(INFO, log_search) << absl::StrFormat(
"*** starting model expansion at %.2fs", wall_timer.Get());
CpModelProto new_model = model_proto; // Copy.
PresolveOptions options;
options.log_info = VLOG_IS_ON(1);
options.log_info = log_search;
ExpandCpModel(&new_model, options);
// Presolve?
std::function<void(CpSolverResponse * response)> postprocess_solution;
if (params.cp_model_presolve()) {
VLOG(1) << absl::StrFormat("*** starting model presolve at %.2fs",
wall_timer.Get());
LOG_IF(INFO, log_search) << absl::StrFormat(
"*** starting model presolve at %.2fs", wall_timer.Get());
// Do the actual presolve.
CpModelProto mapping_proto;
std::vector<int> postsolve_mapping;
PresolveOptions options;
options.log_info = VLOG_IS_ON(1);
options.log_info = log_search;
options.parameters = *model->GetOrCreate<SatParameters>();
options.time_limit = model->GetOrCreate<TimeLimit>();
const bool ok = PresolveCpModel(options, &new_model, &mapping_proto,
@@ -2534,7 +2554,7 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
response.set_status(CpSolverStatus::MODEL_INVALID);
return response;
}
VLOG(1) << CpModelStats(new_model);
LOG_IF(INFO, log_search) << CpModelStats(new_model);
postprocess_solution = [&model_proto, mapping_proto, postsolve_mapping,
&wall_timer](CpSolverResponse* response) {
// Note that it is okay to use the initial model_proto in the postsolve
@@ -2562,8 +2582,8 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
int num_solutions = 0;
std::function<void(const CpSolverResponse&)> observer_function =
[&model_proto, &observers, &num_solutions, &wall_timer, &user_timer,
&postprocess_solution](const CpSolverResponse& response) {
if (VLOG_IS_ON(1)) {
&postprocess_solution, log_search](const CpSolverResponse& response) {
if (log_search) {
if (model_proto.has_objective()) {
const bool maximize =
model_proto.objective().scaling_factor() < 0.0;

3
ortools/sat/cp_model_solver.h
View File

@@ -72,6 +72,9 @@ std::function<SatParameters(Model*)> NewSatParameters(
std::function<SatParameters(Model*)> NewSatParameters(
const SatParameters& parameters);
// used by or-tools non C++ ports to bridge with the C++ layer.
void FixFlagsAndEnvironmentForSwig();
} // namespace sat
} // namespace operations_research

18
ortools/sat/cuts.cc
View File

@@ -410,7 +410,6 @@ CutGenerator CreateKnapsackCoverCutGenerator(
const std::vector<IntegerVariable>& vars, Model* model) {
CutGenerator result;
result.vars = vars;
result.type = "Knapsack";
IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
std::vector<LinearConstraint> knapsack_constraints;
@@ -422,14 +421,14 @@ CutGenerator CreateKnapsackCoverCutGenerator(
// TODO(user): do not add generator if there are no knapsack constraints.
result.generate_cuts = [knapsack_constraints, vars, model, integer_trail](
const gtl::ITIVector<IntegerVariable, double>&
lp_values) {
std::vector<LinearConstraint> cuts;
if (AllVarsTakeIntegerValue(vars, lp_values)) return cuts;
lp_values,
LinearConstraintManager* manager) {
if (AllVarsTakeIntegerValue(vars, lp_values)) return;
KnapsackSolverForCuts knapsack_solver(
"Knapsack on demand cover cut generator");
int64 skipped_constraints = 0;
int64 lifted_cuts = 0;
// Iterate through all knapsack constraints.
for (const LinearConstraint& constraint : knapsack_constraints) {
if (model->GetOrCreate<TimeLimit>()->LimitReached()) break;
@@ -530,24 +529,23 @@ CutGenerator CreateKnapsackCoverCutGenerator(
*integer_trail);
// Check if the constraint has only binary variables.
bool is_lifted = false;
if (ConstraintIsEligibleForLifting(cut, *integer_trail)) {
if (LiftKnapsackCut(constraint, lp_values,
cut_vars_original_coefficients, *integer_trail,
model->GetOrCreate<TimeLimit>(), &cut)) {
lifted_cuts++;
is_lifted = true;
}
}
CHECK(!SolutionSatisfiesConstraint(cut, lp_values));
cuts.push_back(cut);
manager->AddCut(cut, is_lifted ? "LiftedKnapsack" : "Knapsack",
lp_values);
}
}
if (skipped_constraints > 0) {
VLOG(2) << "Skipped constraints: " << skipped_constraints;
}
if (!cuts.empty()) VLOG(1) << "#KnapsackCuts: " << cuts.size();
if (lifted_cuts > 0) VLOG(1) << "#LiftedKnapsackCuts: " << lifted_cuts;
return cuts;
};
return result;

8
ortools/sat/cuts.h
View File

@@ -20,6 +20,7 @@
#include "ortools/base/int_type.h"
#include "ortools/sat/integer.h"
#include "ortools/sat/linear_constraint.h"
#include "ortools/sat/linear_constraint_manager.h"
#include "ortools/sat/model.h"
#include "ortools/util/time_limit.h"
@@ -33,12 +34,11 @@ namespace sat {
// CutGenerator should:
// - Only look at the lp_values positions that corresponds to its 'vars' or
// their negation.
// - Only return cuts in term of the same variables or their negation.
// - Only add cuts in term of the same variables or their negation.
struct CutGenerator {
std::string type;
std::vector<IntegerVariable> vars;
std::function<std::vector<LinearConstraint>(
const gtl::ITIVector<IntegerVariable, double>& lp_values)>
std::function<void(const gtl::ITIVector<IntegerVariable, double>& lp_values,
LinearConstraintManager* manager)>
generate_cuts;
};

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

@@ -90,7 +90,7 @@ void SimpleSatProgram() {
cp_model.AddNotEqual(x, y);
// Solving part.
const CpSolverResponse response = Solve(cp_model);
const CpSolverResponse response = Solve(cp_model.Build());
LOG(INFO) << CpSolverResponseStats(response);
if (response.status() == CpSolverStatus::FEASIBLE) {

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

@@ -144,7 +144,7 @@ void ChannelingSampleSat() {
<< " y=" << SolutionIntegerValue(r, y)
<< " b=" << SolutionBooleanValue(r, b);
}));
SolveWithModel(cp_model, &model);
SolveWithModel(cp_model.Build(), &model);
}
} // namespace sat
@@ -475,7 +475,7 @@ void BinpackingProblemSat() {
cp_model.Maximize(LinearExpr::BooleanSum(slacks));
// Solving part.
const CpSolverResponse response = Solve(cp_model);
const CpSolverResponse response = Solve(cp_model.Build());
LOG(INFO) << CpSolverResponseStats(response);
}

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

@@ -131,7 +131,7 @@ void RabbitsAndPheasantsSat() {
cp_model.AddEquality(LinearExpr::Sum({rabbits, pheasants}), 20);
cp_model.AddEquality(LinearExpr::ScalProd({rabbits, pheasants}, {4, 2}), 56);
const CpSolverResponse response = Solve(cp_model);
const CpSolverResponse response = Solve(cp_model.Build());
if (response.status() == CpSolverStatus::FEASIBLE) {
// Get the value of x in the solution.
@@ -401,7 +401,7 @@ void EarlinessTardinessCostSampleSat() {
LOG(INFO) << "x=" << SolutionIntegerValue(r, x) << " expr"
<< SolutionIntegerValue(r, expr);
}));
SolveWithModel(cp_model, &model);
SolveWithModel(cp_model.Build(), &model);
}
} // namespace sat
@@ -763,7 +763,7 @@ void StepFunctionSampleSat() {
LOG(INFO) << "x=" << SolutionIntegerValue(r, x) << " expr"
<< SolutionIntegerValue(r, expr);
}));
SolveWithModel(cp_model, &model);
SolveWithModel(cp_model.Build(), &model);
}
} // namespace sat

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

@@ -396,7 +396,7 @@ void NoOverlapSampleSat() {
// Solving part.
Model model;
const CpSolverResponse response = SolveWithModel(cp_model, &model);
const CpSolverResponse response = SolveWithModel(cp_model.Build(), &model);
LOG(INFO) << CpSolverResponseStats(response);
if (response.status() == CpSolverStatus::OPTIMAL) {
@@ -836,7 +836,7 @@ void RankingSampleSat() {
cp_model.Minimize(objective);
// Solving part.
const CpSolverResponse response = Solve(cp_model);
const CpSolverResponse response = Solve(cp_model.Build());
LOG(INFO) << CpSolverResponseStats(response);
if (response.status() == CpSolverStatus::OPTIMAL) {

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

@@ -81,7 +81,7 @@ void SolveWithTimeLimitSampleSat() {
model.Add(NewSatParameters(parameters));
// Solve.
const CpSolverResponse response = SolveWithModel(cp_model, &model);
const CpSolverResponse response = SolveWithModel(cp_model.Build(), &model);
LOG(INFO) << CpSolverResponseStats(response);
if (response.status() == CpSolverStatus::FEASIBLE) {
@@ -281,7 +281,7 @@ void SolveAndPrintIntermediateSolutionsSampleSat() {
num_solutions++;
}));
const CpSolverResponse response = SolveWithModel(cp_model, &model);
const CpSolverResponse response = SolveWithModel(cp_model.Build(), &model);
LOG(INFO) << "Number of solutions found: " << num_solutions;
}
@@ -533,7 +533,7 @@ void SearchAllSolutionsSampleSat() {
SatParameters parameters;
parameters.set_enumerate_all_solutions(true);
model.Add(NewSatParameters(parameters));
const CpSolverResponse response = SolveWithModel(cp_model, &model);
const CpSolverResponse response = SolveWithModel(cp_model.Build(), &model);
LOG(INFO) << "Number of solutions found: " << num_solutions;
}
@@ -787,7 +787,7 @@ void StopAfterNSolutionsSampleSat() {
LOG(INFO) << "Stop search after " << kSolutionLimit << " solutions.";
}
}));
const CpSolverResponse response = SolveWithModel(cp_model, &model);
const CpSolverResponse response = SolveWithModel(cp_model.Build(), &model);
LOG(INFO) << "Number of solutions found: " << num_solutions;
CHECK_EQ(num_solutions, kSolutionLimit);
}

46
ortools/sat/linear_programming_constraint.cc
View File

@@ -536,7 +536,7 @@ void LinearProgrammingConstraint::AddCutFromConstraints(
return;
}
VLOG(2) << " num_slack: " << num_slack;
VLOG(3) << " num_slack: " << num_slack;
cut = ConvertToLinearConstraint(dense_cut, cut_ub);
}
@@ -689,14 +689,7 @@ bool LinearProgrammingConstraint::Propagate() {
(trail_->CurrentDecisionLevel() == 0 ||
!sat_parameters_.only_add_cuts_at_level_zero())) {
for (const CutGenerator& generator : cut_generators_) {
// TODO(user): Change api so cuts can directly be added to the manager
// and we don't need this intermediate vector.
std::vector<LinearConstraint> cuts =
generator.generate_cuts(expanded_lp_solution_);
for (const LinearConstraint& cut : cuts) {
constraint_manager_.AddCut(cut, generator.type,
expanded_lp_solution_);
}
generator.generate_cuts(expanded_lp_solution_, &constraint_manager_);
}
}
@@ -1336,7 +1329,8 @@ void AddIncomingAndOutgoingCutsIfNeeded(
int num_nodes, const std::vector<int>& s, const std::vector<int>& tails,
const std::vector<int>& heads, const std::vector<IntegerVariable>& vars,
const std::vector<double>& var_lp_values, int64 rhs_lower_bound,
std::vector<LinearConstraint>* cuts) {
const gtl::ITIVector<IntegerVariable, double>& lp_values,
LinearConstraintManager* manager) {
LinearConstraint incoming;
LinearConstraint outgoing;
double sum_incoming = 0.0;
@@ -1426,10 +1420,10 @@ void AddIncomingAndOutgoingCutsIfNeeded(
}
if (sum_incoming < rhs_lower_bound - 1e-6) {
cuts->push_back(std::move(incoming));
manager->AddCut(incoming, "Circuit", lp_values);
}
if (sum_outgoing < rhs_lower_bound - 1e-6) {
cuts->push_back(std::move(outgoing));
manager->AddCut(outgoing, "Circuit", lp_values);
}
}
@@ -1443,10 +1437,10 @@ CutGenerator CreateStronglyConnectedGraphCutGenerator(
const std::vector<IntegerVariable>& vars) {
CutGenerator result;
result.vars = vars;
result.type = "StronglyConnectedGraph";
result.generate_cuts =
[num_nodes, tails, heads,
vars](const gtl::ITIVector<IntegerVariable, double>& lp_values) {
[num_nodes, tails, heads, vars](
const gtl::ITIVector<IntegerVariable, double>& lp_values,
LinearConstraintManager* manager) {
int num_arcs_in_lp_solution = 0;
std::vector<double> var_lp_values;
std::vector<std::vector<int>> graph(num_nodes);
@@ -1463,23 +1457,21 @@ CutGenerator CreateStronglyConnectedGraphCutGenerator(
graph[tails[i]].push_back(heads[i]);
}
}
std::vector<LinearConstraint> cuts;
std::vector<std::vector<int>> components;
FindStronglyConnectedComponents(num_nodes, graph, &components);
if (components.size() == 1) return cuts;
if (components.size() == 1) return;
VLOG(1) << "num_arcs_in_lp_solution:" << num_arcs_in_lp_solution
<< " sccs:" << components.size();
for (const std::vector<int>& component : components) {
if (component.size() == 1) continue;
AddIncomingAndOutgoingCutsIfNeeded(num_nodes, component, tails, heads,
vars, var_lp_values,
/*rhs_lower_bound=*/1, &cuts);
AddIncomingAndOutgoingCutsIfNeeded(
num_nodes, component, tails, heads, vars, var_lp_values,
/*rhs_lower_bound=*/1, lp_values, manager);
// In this case, the cuts for each component are the same.
if (components.size() == 2) break;
}
return cuts;
};
return result;
}
@@ -1496,10 +1488,10 @@ CutGenerator CreateCVRPCutGenerator(int num_nodes,
CutGenerator result;
result.vars = vars;
result.type = "CVRP";
result.generate_cuts =
[num_nodes, tails, heads, total_demands, demands, capacity,
vars](const gtl::ITIVector<IntegerVariable, double>& lp_values) {
[num_nodes, tails, heads, total_demands, demands, capacity, vars](
const gtl::ITIVector<IntegerVariable, double>& lp_values,
LinearConstraintManager* manager) {
int num_arcs_in_lp_solution = 0;
std::vector<double> var_lp_values;
std::vector<std::vector<int>> graph(num_nodes);
@@ -1510,10 +1502,9 @@ CutGenerator CreateCVRPCutGenerator(int num_nodes,
graph[tails[i]].push_back(heads[i]);
}
}
std::vector<LinearConstraint> cuts;
std::vector<std::vector<int>> components;
FindStronglyConnectedComponents(num_nodes, graph, &components);
if (components.size() == 1) return cuts;
if (components.size() == 1) return;
VLOG(1) << "num_arcs_in_lp_solution:" << num_arcs_in_lp_solution
<< " sccs:" << components.size();
@@ -1534,12 +1525,11 @@ CutGenerator CreateCVRPCutGenerator(int num_nodes,
AddIncomingAndOutgoingCutsIfNeeded(
num_nodes, component, tails, heads, vars, var_lp_values,
/*rhs_lower_bound=*/min_num_vehicles, &cuts);
/*rhs_lower_bound=*/min_num_vehicles, lp_values, manager);
// In this case, the cuts for each component are the same.
if (components.size() == 2) break;
}
return cuts;
};
return result;
}

2
ortools/sat/samples/binpacking_problem_sat.cc
View File

@@ -78,7 +78,7 @@ void BinpackingProblemSat() {
cp_model.Maximize(LinearExpr::BooleanSum(slacks));
// Solving part.
const CpSolverResponse response = Solve(cp_model);
const CpSolverResponse response = Solve(cp_model.Build());
LOG(INFO) << CpSolverResponseStats(response);
}

2
ortools/sat/samples/channeling_sample_sat.cc
View File

@@ -54,7 +54,7 @@ void ChannelingSampleSat() {
<< " y=" << SolutionIntegerValue(r, y)
<< " b=" << SolutionBooleanValue(r, b);
}));
SolveWithModel(cp_model, &model);
SolveWithModel(cp_model.Build(), &model);
}
} // namespace sat

2
ortools/sat/samples/cp_is_fun_sat.cc
View File

@@ -88,7 +88,7 @@ void CPIsFunSat() {
parameters.set_enumerate_all_solutions(true);
model.Add(NewSatParameters(parameters));
const CpSolverResponse response = SolveWithModel(cp_model, &model);
const CpSolverResponse response = SolveWithModel(cp_model.Build(), &model);
LOG(INFO) << "Number of solutions found: " << num_solutions;
// [END solve]
}

2
ortools/sat/samples/earliness_tardiness_cost_sample_sat.cc
View File

@@ -69,7 +69,7 @@ void EarlinessTardinessCostSampleSat() {
LOG(INFO) << "x=" << SolutionIntegerValue(r, x) << " expr"
<< SolutionIntegerValue(r, expr);
}));
SolveWithModel(cp_model, &model);
SolveWithModel(cp_model.Build(), &model);
}
} // namespace sat

2
ortools/sat/samples/no_overlap_sample_sat.cc
View File

@@ -67,7 +67,7 @@ void NoOverlapSampleSat() {
// Solving part.
Model model;
const CpSolverResponse response = SolveWithModel(cp_model, &model);
const CpSolverResponse response = SolveWithModel(cp_model.Build(), &model);
LOG(INFO) << CpSolverResponseStats(response);
if (response.status() == CpSolverStatus::OPTIMAL) {

2
ortools/sat/samples/rabbits_and_pheasants_sat.cc
View File

@@ -27,7 +27,7 @@ void RabbitsAndPheasantsSat() {
cp_model.AddEquality(LinearExpr::Sum({rabbits, pheasants}), 20);
cp_model.AddEquality(LinearExpr::ScalProd({rabbits, pheasants}, {4, 2}), 56);
const CpSolverResponse response = Solve(cp_model);
const CpSolverResponse response = Solve(cp_model.Build());
if (response.status() == CpSolverStatus::FEASIBLE) {
// Get the value of x in the solution.

2
ortools/sat/samples/ranking_sample_sat.cc
View File

@@ -124,7 +124,7 @@ void RankingSampleSat() {
cp_model.Minimize(objective);
// Solving part.
const CpSolverResponse response = Solve(cp_model);
const CpSolverResponse response = Solve(cp_model.Build());
LOG(INFO) << CpSolverResponseStats(response);
if (response.status() == CpSolverStatus::OPTIMAL) {

2
ortools/sat/samples/search_for_all_solutions_sample_sat.cc
View File

@@ -53,7 +53,7 @@ void SearchAllSolutionsSampleSat() {
SatParameters parameters;
parameters.set_enumerate_all_solutions(true);
model.Add(NewSatParameters(parameters));
const CpSolverResponse response = SolveWithModel(cp_model, &model);
const CpSolverResponse response = SolveWithModel(cp_model.Build(), &model);
// [END solve]
LOG(INFO) << "Number of solutions found: " << num_solutions;

2
ortools/sat/samples/simple_sat_program.cc
View File

@@ -35,7 +35,7 @@ void SimpleSatProgram() {
// Solving part.
// [START solve]
const CpSolverResponse response = Solve(cp_model);
const CpSolverResponse response = Solve(cp_model.Build());
LOG(INFO) << CpSolverResponseStats(response);
// [END solve]

2
ortools/sat/samples/solve_and_print_intermediate_solutions_sample_sat.cc
View File

@@ -52,7 +52,7 @@ void SolveAndPrintIntermediateSolutionsSampleSat() {
// [END print_solution]
// [START solve]
const CpSolverResponse response = SolveWithModel(cp_model, &model);
const CpSolverResponse response = SolveWithModel(cp_model.Build(), &model);
// [END solve]
LOG(INFO) << "Number of solutions found: " << num_solutions;

2
ortools/sat/samples/solve_with_time_limit_sample_sat.cc
View File

@@ -37,7 +37,7 @@ void SolveWithTimeLimitSampleSat() {
model.Add(NewSatParameters(parameters));
// Solve.
const CpSolverResponse response = SolveWithModel(cp_model, &model);
const CpSolverResponse response = SolveWithModel(cp_model.Build(), &model);
LOG(INFO) << CpSolverResponseStats(response);
if (response.status() == CpSolverStatus::FEASIBLE) {

2
ortools/sat/samples/step_function_sample_sat.cc
View File

@@ -71,7 +71,7 @@ void StepFunctionSampleSat() {
LOG(INFO) << "x=" << SolutionIntegerValue(r, x) << " expr"
<< SolutionIntegerValue(r, expr);
}));
SolveWithModel(cp_model, &model);
SolveWithModel(cp_model.Build(), &model);
}
} // namespace sat

2
ortools/sat/samples/stop_after_n_solutions_sample_sat.cc
View File

@@ -53,7 +53,7 @@ void StopAfterNSolutionsSampleSat() {
LOG(INFO) << "Stop search after " << kSolutionLimit << " solutions.";
}
}));
const CpSolverResponse response = SolveWithModel(cp_model, &model);
const CpSolverResponse response = SolveWithModel(cp_model.Build(), &model);
LOG(INFO) << "Number of solutions found: " << num_solutions;
CHECK_EQ(num_solutions, kSolutionLimit);
}

5
ortools/sat/swig_helper.h
View File

@@ -103,6 +103,7 @@ class SatHelper {
// C# protobufs do not support proto2.
static operations_research::sat::CpSolverResponse Solve(
const operations_research::sat::CpModelProto& model_proto) {
FixFlagsAndEnvironmentForSwig();
Model model;
std::atomic<bool> stopped(false);
model.GetOrCreate<TimeLimit>()->RegisterExternalBooleanAsLimit(&stopped);
@@ -115,6 +116,7 @@ class SatHelper {
static operations_research::sat::CpSolverResponse SolveWithParameters(
const operations_research::sat::CpModelProto& model_proto,
const operations_research::sat::SatParameters& parameters) {
FixFlagsAndEnvironmentForSwig();
Model model;
model.Add(NewSatParameters(parameters));
std::atomic<bool> stopped(false);
@@ -128,6 +130,7 @@ class SatHelper {
static operations_research::sat::CpSolverResponse SolveWithStringParameters(
const operations_research::sat::CpModelProto& model_proto,
const std::string& parameters) {
FixFlagsAndEnvironmentForSwig();
Model model;
model.Add(NewSatParameters(parameters));
std::atomic<bool> stopped(false);
@@ -143,6 +146,7 @@ class SatHelper {
const operations_research::sat::CpModelProto& model_proto,
const operations_research::sat::SatParameters& parameters,
const SolutionCallback& callback) {
FixFlagsAndEnvironmentForSwig();
Model model;
model.Add(NewSatParameters(parameters));
model.Add(NewFeasibleSolutionObserver(
@@ -159,6 +163,7 @@ class SatHelper {
SolveWithStringParametersAndSolutionCallback(
const operations_research::sat::CpModelProto& model_proto,
const std::string& parameters, const SolutionCallback& callback) {
FixFlagsAndEnvironmentForSwig();
Model model;
model.Add(NewSatParameters(parameters));
model.Add(NewFeasibleSolutionObserver(