27 #include "absl/random/random.h"
28 #include "absl/strings/str_cat.h"
29 #include "absl/strings/str_format.h"
37 #if !defined(__PORTABLE_PLATFORM__) && defined(USE_SCIP)
39 #include "ortools/linear_solver/linear_solver.pb.h"
47 #include "ortools/sat/sat_parameters.pb.h"
61 void Log(
const std::string&
message) {
75 std::string CnfObjectiveLine(
const LinearBooleanProblem& problem,
76 Coefficient objective) {
77 const double scaled_objective =
79 return absl::StrFormat(
"o %d",
static_cast<int64>(scaled_objective));
82 struct LiteralWithCoreIndex {
91 template <
typename Vector>
92 void DeleteVectorIndices(
const std::vector<int>& indices, Vector* v) {
94 int indices_index = 0;
95 for (
int i = 0; i < v->size(); ++i) {
96 if (indices_index < indices.size() && i == indices[indices_index]) {
99 (*v)[new_size] = (*v)[i];
135 class FuMalikSymmetryBreaker {
137 FuMalikSymmetryBreaker() {}
140 void StartResolvingNewCore(
int new_core_index) {
141 literal_by_core_.resize(new_core_index);
142 for (
int i = 0; i < new_core_index; ++i) {
143 literal_by_core_[i].clear();
157 std::vector<Literal> ProcessLiteral(
int assumption_index, Literal
b) {
158 if (assumption_index >= info_by_assumption_index_.size()) {
159 info_by_assumption_index_.resize(assumption_index + 1);
166 std::vector<Literal> result;
167 for (LiteralWithCoreIndex data :
168 info_by_assumption_index_[assumption_index]) {
175 result.insert(result.end(), literal_by_core_[data.core_index].begin(),
176 literal_by_core_[data.core_index].end());
180 for (LiteralWithCoreIndex data :
181 info_by_assumption_index_[assumption_index]) {
182 literal_by_core_[data.core_index].push_back(data.literal);
184 info_by_assumption_index_[assumption_index].push_back(
185 LiteralWithCoreIndex(
b, literal_by_core_.size()));
190 void DeleteIndices(
const std::vector<int>& indices) {
191 DeleteVectorIndices(indices, &info_by_assumption_index_);
196 void ClearInfo(
int assumption_index) {
197 CHECK_LE(assumption_index, info_by_assumption_index_.size());
198 info_by_assumption_index_[assumption_index].clear();
202 void AddInfo(
int assumption_index, Literal
b) {
203 CHECK_GE(assumption_index, info_by_assumption_index_.size());
204 info_by_assumption_index_.resize(assumption_index + 1);
205 info_by_assumption_index_[assumption_index].push_back(
206 LiteralWithCoreIndex(
b, literal_by_core_.size()));
210 std::vector<std::vector<LiteralWithCoreIndex>> info_by_assumption_index_;
211 std::vector<std::vector<Literal>> literal_by_core_;
219 std::vector<Literal>* core) {
221 std::set<LiteralIndex> moved_last;
222 std::vector<Literal> candidate(core->begin(), core->end());
233 if (target_level == -1)
break;
251 if (candidate.empty() || solver->
IsModelUnsat())
return;
252 moved_last.insert(candidate.back().Index());
257 if (candidate.size() < core->size()) {
258 VLOG(1) <<
"minimization " << core->size() <<
" -> " << candidate.size();
259 core->assign(candidate.begin(), candidate.end());
269 const LinearBooleanProblem& problem,
271 std::vector<bool>* solution) {
273 FuMalikSymmetryBreaker symmetry;
294 std::vector<std::vector<Literal>> blocking_clauses;
295 std::vector<Literal> assumptions;
298 const LinearObjective& objective = problem.objective();
299 CHECK_GT(objective.coefficients_size(), 0);
300 const Coefficient unique_objective_coeff(std::abs(objective.coefficients(0)));
301 for (
int i = 0; i < objective.literals_size(); ++i) {
302 CHECK_EQ(std::abs(objective.coefficients(i)), unique_objective_coeff)
303 <<
"The basic Fu & Malik algorithm needs constant objective coeffs.";
309 blocking_clauses.push_back(std::vector<Literal>(1, min_literal));
312 assumptions.push_back(min_literal);
316 logger.Log(absl::StrFormat(
"c #weights:%u #vars:%d #constraints:%d",
317 assumptions.size(), problem.num_variables(),
318 problem.constraints_size()));
325 for (
int iter = 0;; ++iter) {
331 logger.Log(CnfObjectiveLine(problem, objective));
347 logger.Log(absl::StrFormat(
"c iter:%d core:%u", iter, core.size()));
350 if (core.size() == 1) {
354 std::find(assumptions.begin(), assumptions.end(), core[0]) -
367 std::vector<int> to_delete(1,
index);
368 DeleteVectorIndices(to_delete, &assumptions);
369 DeleteVectorIndices(to_delete, &blocking_clauses);
370 symmetry.DeleteIndices(to_delete);
372 symmetry.StartResolvingNewCore(iter);
376 if (core.size() == 2) {
386 std::vector<LiteralWithCoeff> at_most_one_constraint;
387 std::vector<Literal> at_least_one_constraint;
395 for (
int i = 0; i < core.size(); ++i) {
400 std::find(assumptions.begin() +
index, assumptions.end(), core[i]) -
405 const Literal a(BooleanVariable(old_num_variables + i),
true);
406 Literal b(BooleanVariable(old_num_variables + core.size() + i),
true);
407 if (core.size() == 2) {
408 b =
Literal(BooleanVariable(old_num_variables + 2),
true);
409 if (i == 1)
b =
b.Negated();
424 if (assumptions[
index].Variable() >= problem.num_variables()) {
429 blocking_clauses[
index].push_back(
b);
433 blocking_clauses[
index].push_back(
a);
435 blocking_clauses[
index].pop_back();
439 at_least_one_constraint.push_back(
b);
442 assumptions[
index] =
a.Negated();
448 &at_most_one_constraint);
458 LOG(
INFO) <<
"Infeasible while adding a clause.";
466 const LinearBooleanProblem& problem,
468 std::vector<bool>* solution) {
470 FuMalikSymmetryBreaker symmetry;
474 Coefficient lower_bound(
static_cast<int64>(problem.objective().offset()));
478 std::vector<Literal> assumptions;
479 std::vector<Coefficient> costs;
480 std::vector<Literal> reference;
483 const LinearObjective& objective = problem.objective();
484 CHECK_GT(objective.coefficients_size(), 0);
485 for (
int i = 0; i < objective.literals_size(); ++i) {
487 const Coefficient coeff(objective.coefficients(i));
493 costs.push_back(coeff);
495 assumptions.push_back(
literal);
496 costs.push_back(-coeff);
497 lower_bound += coeff;
500 reference = assumptions;
503 Coefficient stratified_lower_bound =
504 *std::max_element(costs.begin(), costs.end());
507 logger.Log(absl::StrFormat(
"c #weights:%u #vars:%d #constraints:%d",
508 assumptions.size(), problem.num_variables(),
509 problem.constraints_size()));
511 for (
int iter = 0;; ++iter) {
517 const Coefficient hardening_threshold = upper_bound - lower_bound;
519 std::vector<int> to_delete;
520 int num_above_threshold = 0;
521 for (
int i = 0; i < assumptions.size(); ++i) {
522 if (costs[i] > hardening_threshold) {
526 to_delete.push_back(i);
527 ++num_above_threshold;
531 to_delete.push_back(i);
535 if (!to_delete.empty()) {
536 logger.Log(absl::StrFormat(
"c fixed %u assumptions, %d with cost > %d",
537 to_delete.size(), num_above_threshold,
538 hardening_threshold.value()));
539 DeleteVectorIndices(to_delete, &assumptions);
540 DeleteVectorIndices(to_delete, &costs);
541 DeleteVectorIndices(to_delete, &reference);
542 symmetry.DeleteIndices(to_delete);
547 std::vector<Literal> assumptions_subset;
548 for (
int i = 0; i < assumptions.size(); ++i) {
549 if (costs[i] >= stratified_lower_bound) {
550 assumptions_subset.push_back(assumptions[i]);
562 const Coefficient old_lower_bound = stratified_lower_bound;
563 for (Coefficient
cost : costs) {
564 if (
cost < old_lower_bound) {
565 if (stratified_lower_bound == old_lower_bound ||
566 cost > stratified_lower_bound) {
567 stratified_lower_bound =
cost;
574 const Coefficient objective_offset(
575 static_cast<int64>(problem.objective().offset()));
577 if (objective + objective_offset < upper_bound) {
578 logger.Log(CnfObjectiveLine(problem, objective));
579 upper_bound = objective + objective_offset;
582 if (stratified_lower_bound < old_lower_bound)
continue;
602 for (
int i = 0; i < core.size(); ++i) {
604 std::find(assumptions.begin() +
index, assumptions.end(), core[i]) -
610 lower_bound += min_cost;
613 logger.Log(absl::StrFormat(
614 "c iter:%d core:%u lb:%d min_cost:%d strat:%d", iter, core.size(),
615 lower_bound.value(), min_cost.value(), stratified_lower_bound.value()));
621 if (min_cost > stratified_lower_bound) {
622 stratified_lower_bound = min_cost;
626 if (core.size() == 1) {
630 std::find(assumptions.begin(), assumptions.end(), core[0]) -
640 std::vector<int> to_delete(1,
index);
641 DeleteVectorIndices(to_delete, &assumptions);
642 DeleteVectorIndices(to_delete, &costs);
643 DeleteVectorIndices(to_delete, &reference);
644 symmetry.DeleteIndices(to_delete);
646 symmetry.StartResolvingNewCore(iter);
650 if (core.size() == 2) {
660 std::vector<LiteralWithCoeff> at_most_one_constraint;
661 std::vector<Literal> at_least_one_constraint;
669 for (
int i = 0; i < core.size(); ++i) {
674 std::find(assumptions.begin() +
index, assumptions.end(), core[i]) -
679 const Literal a(BooleanVariable(old_num_variables + i),
true);
680 Literal b(BooleanVariable(old_num_variables + core.size() + i),
true);
681 if (core.size() == 2) {
682 b =
Literal(BooleanVariable(old_num_variables + 2),
true);
683 if (i == 1)
b =
b.Negated();
705 if (costs[
index] == min_cost) {
707 assumptions[
index] =
a.Negated();
717 symmetry.AddInfo(assumptions.size(),
b);
718 symmetry.ClearInfo(
index);
721 costs[
index] -= min_cost;
729 assumptions.push_back(
a.Negated());
730 costs.push_back(min_cost);
731 reference.push_back(reference[
index]);
743 at_least_one_constraint.push_back(reference[
index].Negated());
749 &at_most_one_constraint);
755 LOG(
INFO) <<
"Unsat while adding a clause.";
763 const LinearBooleanProblem& problem,
765 std::vector<bool>* solution) {
767 const SatParameters initial_parameters = solver->
parameters();
770 SatParameters
parameters = initial_parameters;
775 int max_number_of_conflicts = 5;
780 Coefficient best(min_seen);
781 for (
int i = 0; i < num_times; ++i) {
785 parameters.set_max_number_of_conflicts(max_number_of_conflicts);
791 const bool use_obj = absl::Bernoulli(random, 1.0 / 4);
810 std::vector<bool> candidate;
814 if (objective < best) {
815 *solution = candidate;
817 logger.Log(CnfObjectiveLine(problem, objective));
822 objective - 1, solver)) {
826 min_seen =
std::min(min_seen, objective);
827 max_seen =
std::max(max_seen, objective);
829 logger.Log(absl::StrCat(
830 "c ", objective.value(),
" [", min_seen.value(),
", ", max_seen.value(),
831 "] objective_preference: ", use_obj ?
"true" :
"false",
" ",
843 const LinearBooleanProblem& problem,
845 std::vector<bool>* solution) {
852 if (!solution->empty()) {
861 objective - 1, solver)) {
881 const Coefficient old_objective = objective;
884 logger.Log(CnfObjectiveLine(problem, objective));
890 std::vector<bool>* solution) {
892 std::deque<EncodingNode> repository;
895 Coefficient offset(0);
896 std::vector<EncodingNode*> nodes =
900 CHECK(!nodes.empty());
901 const Coefficient reference = nodes.front()->weight();
907 if (!solution->empty()) {
910 upper_bound = objective + offset;
914 logger.Log(absl::StrFormat(
"c #weights:%u #vars:%d #constraints:%d",
915 nodes.size(), problem.num_variables(),
916 problem.constraints_size()));
922 logger.Log(absl::StrFormat(
"c encoding depth:%d", root->
depth()));
928 const int index = offset.value() + objective.value();
949 const Coefficient old_objective = objective;
952 logger.Log(CnfObjectiveLine(problem, objective));
958 std::vector<bool>* solution) {
963 Coefficient offset(0);
964 std::deque<EncodingNode> repository;
965 std::vector<EncodingNode*> nodes =
970 Coefficient lower_bound(0);
972 if (!solution->empty()) {
978 logger.Log(absl::StrFormat(
"c #weights:%u #vars:%d #constraints:%d",
979 nodes.size(), problem.num_variables(),
980 problem.constraints_size()));
983 Coefficient stratified_lower_bound(0);
985 SatParameters::STRATIFICATION_DESCENT) {
988 stratified_lower_bound =
std::max(stratified_lower_bound, n->weight());
994 std::string previous_core_info =
"";
995 for (
int iter = 0;; ++iter) {
997 upper_bound, stratified_lower_bound, &lower_bound, &nodes, solver);
1001 const std::string gap_string =
1004 : absl::StrFormat(
" gap:%d", (upper_bound - lower_bound).value());
1006 absl::StrFormat(
"c iter:%d [%s] lb:%d%s assumptions:%u depth:%d", iter,
1008 lower_bound.value() - offset.value() +
1009 static_cast<int64>(problem.objective().offset()),
1010 gap_string, nodes.size(), max_depth));
1017 std::vector<bool> temp_solution;
1021 if (obj + offset < upper_bound) {
1022 *solution = temp_solution;
1023 logger.Log(CnfObjectiveLine(problem, obj));
1024 upper_bound = obj + offset;
1029 stratified_lower_bound =
1031 if (stratified_lower_bound > 0)
continue;
1043 previous_core_info =
1044 absl::StrFormat(
"core:%u mw:%d", core.size(), min_weight.value());
1047 if (stratified_lower_bound < min_weight &&
1049 SatParameters::STRATIFICATION_ASCENT) {
1050 stratified_lower_bound = min_weight;
1053 ProcessCore(core, min_weight, &repository, &nodes, solver);
1054 max_depth =
std::max(max_depth, nodes.back()->depth());
1059 IntegerVariable objective_var,
1060 const std::function<
void()>& feasible_solution_observer,
Model*
model) {
1063 const SatParameters&
parameters = *(
model->GetOrCreate<SatParameters>());
1071 const IntegerValue objective = integer_trail->LowerBound(objective_var);
1074 if (feasible_solution_observer !=
nullptr) {
1075 feasible_solution_observer();
1077 if (
parameters.stop_after_first_solution()) {
1083 if (!integer_trail->Enqueue(
1092 IntegerVariable objective_var,
1093 const std::function<
void()>& feasible_solution_observer,
Model*
model) {
1094 const SatParameters old_params = *
model->GetOrCreate<SatParameters>();
1101 SatParameters new_params = old_params;
1102 new_params.set_max_number_of_conflicts(
1103 old_params.binary_search_num_conflicts());
1104 *
model->GetOrCreate<SatParameters>() = new_params;
1110 IntegerValue unknown_min = integer_trail->UpperBound(objective_var);
1111 IntegerValue unknown_max = integer_trail->LowerBound(objective_var);
1113 sat_solver->Backtrack(0);
1114 const IntegerValue lb = integer_trail->LowerBound(objective_var);
1115 const IntegerValue ub = integer_trail->UpperBound(objective_var);
1116 unknown_min =
std::min(unknown_min, ub);
1117 unknown_max =
std::max(unknown_max, lb);
1120 IntegerValue target;
1121 if (lb < unknown_min) {
1122 target = lb + (unknown_min - lb) / 2;
1123 }
else if (unknown_max < ub) {
1124 target = ub - (ub - unknown_max) / 2;
1126 VLOG(1) <<
"Binary-search, done.";
1129 VLOG(1) <<
"Binary-search, objective: [" << lb <<
"," << ub <<
"]"
1130 <<
" tried: [" << unknown_min <<
"," << unknown_max <<
"]"
1131 <<
" target: obj<=" << target;
1134 const Literal assumption = integer_encoder->GetOrCreateAssociatedLiteral(
1148 sat_solver->Backtrack(0);
1149 if (!integer_trail->Enqueue(
1158 const IntegerValue objective = integer_trail->LowerBound(objective_var);
1159 if (feasible_solution_observer !=
nullptr) {
1160 feasible_solution_observer();
1165 sat_solver->Backtrack(0);
1166 if (!integer_trail->Enqueue(
1174 unknown_min =
std::min(target, unknown_min);
1175 unknown_max =
std::max(target, unknown_max);
1181 sat_solver->Backtrack(0);
1182 *
model->GetOrCreate<SatParameters>() = old_params;
1209 std::vector<IntegerValue> assumption_weights,
1210 IntegerValue stratified_threshold, Model*
model,
1211 std::vector<std::vector<Literal>>* cores) {
1213 SatSolver* sat_solver =
model->GetOrCreate<SatSolver>();
1221 std::vector<Literal> core = sat_solver->GetLastIncompatibleDecisions();
1222 if (sat_solver->parameters().minimize_core()) {
1225 CHECK(!core.empty());
1226 cores->push_back(core);
1227 if (!sat_solver->parameters().find_multiple_cores())
break;
1231 std::vector<int> indices;
1233 std::set<Literal> temp(core.begin(), core.end());
1234 for (
int i = 0; i < assumptions.size(); ++i) {
1236 indices.push_back(i);
1246 IntegerValue min_weight = assumption_weights[indices.front()];
1247 for (
const int i : indices) {
1248 min_weight =
std::min(min_weight, assumption_weights[i]);
1250 for (
const int i : indices) {
1251 assumption_weights[i] -= min_weight;
1257 for (
int i = 0; i < assumptions.size(); ++i) {
1258 if (assumption_weights[i] < stratified_threshold)
continue;
1259 assumptions[new_size] = assumptions[i];
1260 assumption_weights[new_size] = assumption_weights[i];
1263 assumptions.resize(new_size);
1264 assumption_weights.resize(new_size);
1265 }
while (!assumptions.empty());
1272 std::vector<Literal> assumptions, Model*
model,
1273 std::vector<std::vector<Literal>>* cores) {
1275 SatSolver* sat_solver =
model->GetOrCreate<SatSolver>();
1276 TimeLimit* limit =
model->GetOrCreate<TimeLimit>();
1283 std::vector<Literal> core = sat_solver->GetLastIncompatibleDecisions();
1284 if (sat_solver->parameters().minimize_core()) {
1287 CHECK(!core.empty());
1288 cores->push_back(core);
1289 if (!sat_solver->parameters().find_multiple_cores())
break;
1293 CHECK(!core.empty());
1294 auto* random =
model->GetOrCreate<ModelRandomGenerator>();
1295 const Literal random_literal =
1296 core[absl::Uniform<int>(*random, 0, core.size())];
1297 for (
int i = 0; i < assumptions.size(); ++i) {
1298 if (assumptions[i] == random_literal) {
1299 std::swap(assumptions[i], assumptions.back());
1300 assumptions.pop_back();
1304 }
while (!assumptions.empty());
1311 IntegerVariable objective_var,
1312 const std::vector<IntegerVariable>& variables,
1314 std::function<
void()> feasible_solution_observer,
Model*
model)
1315 : parameters_(
model->GetOrCreate<SatParameters>()),
1321 objective_var_(objective_var),
1322 feasible_solution_observer_(std::move(feasible_solution_observer)) {
1324 for (
int i = 0; i < variables.size(); ++i) {
1332 terms_.back().depth = 0;
1338 stratification_threshold_ = parameters_->max_sat_stratification() ==
1339 SatParameters::STRATIFICATION_NONE
1344 bool CoreBasedOptimizer::ProcessSolution() {
1347 IntegerValue objective(0);
1348 for (ObjectiveTerm& term : terms_) {
1350 objective += term.weight *
value;
1365 if (feasible_solution_observer_ !=
nullptr) {
1366 feasible_solution_observer_();
1368 if (parameters_->stop_after_first_solution()) {
1376 return integer_trail_->
Enqueue(
1380 bool CoreBasedOptimizer::PropagateObjectiveBounds() {
1382 bool some_bound_were_tightened =
true;
1383 while (some_bound_were_tightened) {
1384 some_bound_were_tightened =
false;
1388 IntegerValue implied_objective_lb(0);
1389 for (ObjectiveTerm& term : terms_) {
1390 const IntegerValue var_lb = integer_trail_->
LowerBound(term.var);
1391 term.old_var_lb = var_lb;
1392 implied_objective_lb += term.weight * var_lb.value();
1396 if (implied_objective_lb > integer_trail_->
LowerBound(objective_var_)) {
1398 objective_var_, implied_objective_lb),
1403 some_bound_were_tightened =
true;
1412 const IntegerValue gap =
1413 integer_trail_->
UpperBound(objective_var_) - implied_objective_lb;
1415 for (
const ObjectiveTerm& term : terms_) {
1416 if (term.weight == 0)
continue;
1417 const IntegerValue var_lb = integer_trail_->
LowerBound(term.var);
1418 const IntegerValue var_ub = integer_trail_->
UpperBound(term.var);
1419 if (var_lb == var_ub)
continue;
1426 if (gap / term.weight < var_ub - var_lb) {
1427 some_bound_were_tightened =
true;
1428 const IntegerValue new_ub = var_lb + gap / term.weight;
1450 void CoreBasedOptimizer::ComputeNextStratificationThreshold() {
1451 std::vector<IntegerValue> weights;
1452 for (ObjectiveTerm& term : terms_) {
1453 if (term.weight >= stratification_threshold_)
continue;
1454 if (term.weight == 0)
continue;
1458 if (var_lb == var_ub)
continue;
1460 weights.push_back(term.weight);
1462 if (weights.empty()) {
1463 stratification_threshold_ = IntegerValue(0);
1468 stratification_threshold_ =
1469 weights[
static_cast<int>(std::floor(0.9 * weights.size()))];
1472 bool CoreBasedOptimizer::CoverOptimization() {
1475 constexpr
double max_dtime_per_core = 0.5;
1476 const double old_time_limit = parameters_->max_deterministic_time();
1477 parameters_->set_max_deterministic_time(max_dtime_per_core);
1479 parameters_->set_max_deterministic_time(old_time_limit);
1482 for (
const ObjectiveTerm& term : terms_) {
1486 if (term.depth == 0)
continue;
1492 const IntegerVariable
var = term.var;
1503 const double deterministic_limit =
1515 VLOG(1) <<
"cover_opt var:" <<
var <<
" domain:["
1517 if (!ProcessSolution())
return false;
1536 if (!PropagateObjectiveBounds())
return false;
1545 std::map<LiteralIndex, int> literal_to_term_index;
1558 if (parameters_->cover_optimization()) {
1564 std::vector<int> term_indices;
1565 std::vector<IntegerLiteral> integer_assumptions;
1566 std::vector<IntegerValue> assumption_weights;
1567 IntegerValue objective_offset(0);
1568 bool some_assumptions_were_skipped =
false;
1569 for (
int i = 0; i < terms_.size(); ++i) {
1570 const ObjectiveTerm term = terms_[i];
1573 if (term.weight == 0)
continue;
1579 const IntegerValue var_lb = integer_trail_->
LowerBound(term.var);
1580 const IntegerValue var_ub = integer_trail_->
UpperBound(term.var);
1581 if (var_lb == var_ub) {
1582 objective_offset += term.weight * var_lb.value();
1587 if (term.weight >= stratification_threshold_) {
1588 integer_assumptions.push_back(
1590 assumption_weights.push_back(term.weight);
1591 term_indices.push_back(i);
1593 some_assumptions_were_skipped =
true;
1598 if (term_indices.empty() && some_assumptions_were_skipped) {
1599 ComputeNextStratificationThreshold();
1604 if (term_indices.size() <= 2 && !some_assumptions_were_skipped) {
1605 VLOG(1) <<
"Switching to linear scan...";
1606 if (!already_switched_to_linear_scan_) {
1607 already_switched_to_linear_scan_ =
true;
1608 std::vector<IntegerVariable> constraint_vars;
1609 std::vector<int64> constraint_coeffs;
1610 for (
const int index : term_indices) {
1611 constraint_vars.push_back(terms_[
index].
var);
1612 constraint_coeffs.push_back(terms_[
index].
weight.value());
1614 constraint_vars.push_back(objective_var_);
1615 constraint_coeffs.push_back(-1);
1617 -objective_offset.value()));
1621 objective_var_, feasible_solution_observer_, model_);
1627 for (
const ObjectiveTerm& term : terms_) {
1628 max_depth =
std::max(max_depth, term.depth);
1635 :
static_cast<int>(std::ceil(
1636 100.0 * (ub - lb) /
std::max(std::abs(ub), std::abs(lb))));
1637 VLOG(1) << absl::StrCat(
"unscaled_next_obj_range:[", lb,
",", ub,
1640 gap,
"%",
" assumptions:", term_indices.size(),
1641 " strat:", stratification_threshold_.value(),
1642 " depth:", max_depth);
1646 std::vector<Literal> assumptions;
1647 literal_to_term_index.clear();
1648 for (
int i = 0; i < integer_assumptions.size(); ++i) {
1650 integer_assumptions[i]));
1658 literal_to_term_index[assumptions.back().Index()] = term_indices[i];
1666 std::vector<std::vector<Literal>> cores;
1668 FindCores(assumptions, assumption_weights, stratification_threshold_,
1674 if (cores.empty()) {
1675 ComputeNextStratificationThreshold();
1684 for (
const std::vector<Literal>& core : cores) {
1687 if (core.size() == 1)
continue;
1692 bool ignore_this_core =
false;
1694 IntegerValue max_weight(0);
1695 IntegerValue new_var_lb(1);
1696 IntegerValue new_var_ub(0);
1698 for (
const Literal lit : core) {
1703 if (terms_[
index].old_var_lb <
1705 ignore_this_core =
true;
1716 if (ignore_this_core)
continue;
1718 VLOG(1) << absl::StrFormat(
1719 "core:%u weight:[%d,%d] domain:[%d,%d] depth:%d", core.size(),
1720 min_weight.value(), max_weight.value(), new_var_lb.value(),
1721 new_var_ub.value(), new_depth);
1725 const IntegerVariable new_var =
1727 terms_.push_back({new_var, min_weight, new_depth});
1728 terms_.back().cover_ub = new_var_ub;
1732 std::vector<IntegerVariable> constraint_vars;
1733 std::vector<int64> constraint_coeffs;
1734 for (
const Literal lit : core) {
1736 terms_[
index].weight -= min_weight;
1737 constraint_vars.push_back(terms_[
index].
var);
1738 constraint_coeffs.push_back(1);
1740 constraint_vars.push_back(new_var);
1741 constraint_coeffs.push_back(-1);
1759 const std::function<
void()>& feasible_solution_observer,
Model*
model) {
1760 #if !defined(__PORTABLE_PLATFORM__) && defined(USE_SCIP)
1762 IntegerVariable objective_var = objective_definition.
objective_var;
1763 std::vector<IntegerVariable> variables = objective_definition.
vars;
1771 const auto process_solution = [&]() {
1774 IntegerValue objective(0);
1775 for (
int i = 0; i < variables.size(); ++i) {
1779 if (objective > integer_trail->UpperBound(objective_var))
return true;
1781 if (feasible_solution_observer !=
nullptr) {
1782 feasible_solution_observer();
1789 if (!integer_trail->Enqueue(
1799 MPModelRequest request;
1800 request.set_solver_specific_parameters(
"limits/gap = 0");
1801 request.set_solver_type(MPModelRequest::SCIP_MIXED_INTEGER_PROGRAMMING);
1803 MPModelProto& hs_model = *request.mutable_model();
1804 const int num_variables_in_objective = variables.size();
1805 for (
int i = 0; i < num_variables_in_objective; ++i) {
1810 const IntegerVariable
var = variables[i];
1811 MPVariableProto* var_proto = hs_model.add_variable();
1812 var_proto->set_lower_bound(integer_trail->LowerBound(
var).value());
1813 var_proto->set_upper_bound(integer_trail->UpperBound(
var).value());
1815 var_proto->set_is_integer(
true);
1828 std::map<LiteralIndex, std::vector<int>> assumption_to_indices;
1831 std::map<std::pair<int, double>,
int> created_var;
1833 const SatParameters&
parameters = *(
model->GetOrCreate<SatParameters>());
1837 for (
int iter = 0;; ++iter) {
1845 const IntegerValue mip_objective(
1846 static_cast<int64>(std::round(
response.objective_value())));
1847 VLOG(1) <<
"constraints: " << hs_model.constraint_size()
1848 <<
" variables: " << hs_model.variable_size() <<
" hs_lower_bound: "
1850 <<
" strat: " << stratified_threshold;
1856 if (!integer_trail->Enqueue(
1865 std::vector<Literal> assumptions;
1866 assumption_to_indices.clear();
1867 IntegerValue next_stratified_threshold(0);
1868 for (
int i = 0; i < num_variables_in_objective; ++i) {
1869 const IntegerValue hs_value(
1871 if (hs_value == integer_trail->UpperBound(variables[i]))
continue;
1875 next_stratified_threshold =
1880 assumptions.push_back(integer_encoder->GetOrCreateAssociatedLiteral(
1882 assumption_to_indices[assumptions.back().Index()].push_back(i);
1887 if (assumptions.empty() && next_stratified_threshold > 0) {
1888 CHECK_LT(next_stratified_threshold, stratified_threshold);
1889 stratified_threshold = next_stratified_threshold;
1898 std::vector<std::vector<Literal>> cores;
1899 result = FindMultipleCoresForMaxHs(assumptions,
model, &cores);
1902 if (
parameters.stop_after_first_solution()) {
1905 if (cores.empty()) {
1908 stratified_threshold = next_stratified_threshold;
1909 if (stratified_threshold == 0)
break;
1919 for (
const std::vector<Literal>& core : cores) {
1920 if (core.size() == 1) {
1921 for (
const int index :
1923 hs_model.mutable_variable(
index)->set_lower_bound(
1924 integer_trail->LowerBound(variables[
index]).value());
1930 MPConstraintProto*
ct = hs_model.add_constraint();
1931 ct->set_lower_bound(1.0);
1932 for (
const Literal lit : core) {
1933 for (
const int index :
1935 const double lb = integer_trail->LowerBound(variables[
index]).value();
1937 if (hs_value == lb) {
1939 ct->add_coefficient(1.0);
1940 ct->set_lower_bound(
ct->lower_bound() + lb);
1942 const std::pair<int, double> key = {
index, hs_value};
1944 const int new_var_index = hs_model.variable_size();
1945 created_var[key] = new_var_index;
1947 MPVariableProto* new_var = hs_model.add_variable();
1948 new_var->set_lower_bound(0);
1949 new_var->set_upper_bound(1);
1950 new_var->set_is_integer(
true);
1954 MPConstraintProto* implication = hs_model.add_constraint();
1955 implication->set_lower_bound(lb);
1956 implication->add_var_index(
index);
1957 implication->add_coefficient(1.0);
1958 implication->add_var_index(new_var_index);
1959 implication->add_coefficient(lb - hs_value - 1);
1962 ct->add_coefficient(1.0);
#define CHECK_LT(val1, val2)
#define CHECK_EQ(val1, val2)
#define CHECK_GE(val1, val2)
#define CHECK_GT(val1, val2)
#define CHECK_NE(val1, val2)
#define DCHECK(condition)
#define CHECK_LE(val1, val2)
#define VLOG(verboselevel)
static void SolveWithProto(const MPModelRequest &model_request, MPSolutionResponse *response)
Solves the model encoded by a MPModelRequest protocol buffer and fills the solution encoded as a MPSo...
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
bool LimitReached()
Returns true when the external limit is true, or the deterministic time is over the deterministic lim...
double GetElapsedDeterministicTime() const
Returns the elapsed deterministic time since the construction of this object.
CoreBasedOptimizer(IntegerVariable objective_var, const std::vector< IntegerVariable > &variables, const std::vector< IntegerValue > &coefficients, std::function< void()> feasible_solution_observer, Model *model)
SatSolver::Status Optimize()
Literal literal(int i) const
Literal GetOrCreateAssociatedLiteral(IntegerLiteral i_lit)
ABSL_MUST_USE_RESULT bool Enqueue(IntegerLiteral i_lit, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
bool IsCurrentlyIgnored(IntegerVariable i) const
IntegerValue UpperBound(IntegerVariable i) const
IntegerValue LevelZeroUpperBound(IntegerVariable var) const
IntegerVariable AddIntegerVariable(IntegerValue lower_bound, IntegerValue upper_bound)
IntegerValue LevelZeroLowerBound(IntegerVariable var) const
IntegerValue LowerBound(IntegerVariable i) const
Class that owns everything related to a particular optimization model.
T Add(std::function< T(Model *)> f)
This makes it possible to have a nicer API on the client side, and it allows both of these forms:
bool AddLinearConstraint(bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, std::vector< LiteralWithCoeff > *cst)
void SetNumVariables(int num_variables)
bool AddTernaryClause(Literal a, Literal b, Literal c)
const SatParameters & parameters() const
void ResetDecisionHeuristic()
Status ResetAndSolveWithGivenAssumptions(const std::vector< Literal > &assumptions)
void SetAssumptionLevel(int assumption_level)
const VariablesAssignment & Assignment() const
int EnqueueDecisionAndBackjumpOnConflict(Literal true_literal)
void SetParameters(const SatParameters ¶meters)
bool AddBinaryClause(Literal a, Literal b)
int EnqueueDecisionAndBacktrackOnConflict(Literal true_literal)
void Backtrack(int target_level)
std::vector< Literal > GetLastIncompatibleDecisions()
bool IsModelUnsat() const
int CurrentDecisionLevel() const
bool AddProblemClause(absl::Span< const Literal > literals)
bool AddUnitClause(Literal true_literal)
bool LiteralIsTrue(Literal literal) const
bool LiteralIsFalse(Literal literal) const
SharedResponseManager * response
SharedTimeLimit * time_limit
static const int64 kint64max
A C++ wrapper that provides a simple and unified interface to several linear programming and mixed in...
#define DISALLOW_COPY_AND_ASSIGN(TypeName)
absl::Cleanup< absl::decay_t< Callback > > MakeCleanup(Callback &&callback)
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
bool ContainsKey(const Collection &collection, const Key &key)
const Collection::value_type::second_type & FindOrDie(const Collection &collection, const typename Collection::value_type::first_type &key)
const Collection::value_type::second_type & FindOrDieNoPrint(const Collection &collection, const typename Collection::value_type::first_type &key)
bool AddObjectiveConstraint(const LinearBooleanProblem &problem, bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, SatSolver *solver)
std::function< int64(const Model &)> LowerBound(IntegerVariable v)
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
void RestrictObjectiveDomainWithBinarySearch(IntegerVariable objective_var, const std::function< void()> &feasible_solution_observer, Model *model)
double AddOffsetAndScaleObjectiveValue(const LinearBooleanProblem &problem, Coefficient v)
SatSolver::Status ResetAndSolveIntegerProblem(const std::vector< Literal > &assumptions, Model *model)
SatSolver::Status SolveWithCardinalityEncodingAndCore(LogBehavior log, const LinearBooleanProblem &problem, SatSolver *solver, std::vector< bool > *solution)
Coefficient ComputeCoreMinWeight(const std::vector< EncodingNode * > &nodes, const std::vector< Literal > &core)
EncodingNode * MergeAllNodesWithDeque(Coefficient upper_bound, const std::vector< EncodingNode * > &nodes, SatSolver *solver, std::deque< EncodingNode > *repository)
int MoveOneUnprocessedLiteralLast(const std::set< LiteralIndex > &processed, int relevant_prefix_size, std::vector< Literal > *literals)
std::vector< Literal > ReduceNodesAndExtractAssumptions(Coefficient upper_bound, Coefficient stratified_lower_bound, Coefficient *lower_bound, std::vector< EncodingNode * > *nodes, SatSolver *solver)
std::function< int64(const Model &)> Value(IntegerVariable v)
void UseObjectiveForSatAssignmentPreference(const LinearBooleanProblem &problem, SatSolver *solver)
SatSolver::Status SolveWithLinearScan(LogBehavior log, const LinearBooleanProblem &problem, SatSolver *solver, std::vector< bool > *solution)
void MinimizeCore(SatSolver *solver, std::vector< Literal > *core)
SatSolver::Status MinimizeWithHittingSetAndLazyEncoding(const ObjectiveDefinition &objective_definition, const std::function< void()> &feasible_solution_observer, Model *model)
SatSolver::Status SolveIntegerProblem(Model *model)
std::function< void(Model *)> WeightedSumLowerOrEqual(const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 upper_bound)
SatSolver::Status SolveWithWPM1(LogBehavior log, const LinearBooleanProblem &problem, SatSolver *solver, std::vector< bool > *solution)
bool IsAssignmentValid(const LinearBooleanProblem &problem, const std::vector< bool > &assignment)
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
void MinimizeCoreWithPropagation(TimeLimit *limit, SatSolver *solver, std::vector< Literal > *core)
void ProcessCore(const std::vector< Literal > &core, Coefficient min_weight, std::deque< EncodingNode > *repository, std::vector< EncodingNode * > *nodes, SatSolver *solver)
Coefficient ComputeObjectiveValue(const LinearBooleanProblem &problem, const std::vector< bool > &assignment)
SatSolver::Status SolveWithFuMalik(LogBehavior log, const LinearBooleanProblem &problem, SatSolver *solver, std::vector< bool > *solution)
Coefficient MaxNodeWeightSmallerThan(const std::vector< EncodingNode * > &nodes, Coefficient upper_bound)
SatSolver::Status SolveWithRandomParameters(LogBehavior log, const LinearBooleanProblem &problem, int num_times, SatSolver *solver, std::vector< bool > *solution)
SatSolver::Status SolveWithCardinalityEncoding(LogBehavior log, const LinearBooleanProblem &problem, SatSolver *solver, std::vector< bool > *solution)
void ExtractAssignment(const LinearBooleanProblem &problem, const SatSolver &solver, std::vector< bool > *assignment)
std::vector< EncodingNode * > CreateInitialEncodingNodes(const std::vector< Literal > &literals, const std::vector< Coefficient > &coeffs, Coefficient *offset, std::deque< EncodingNode > *repository)
void RandomizeDecisionHeuristic(URBG *random, SatParameters *parameters)
const Coefficient kCoefficientMax(std::numeric_limits< Coefficient::ValueType >::max())
SatSolver::Status MinimizeIntegerVariableWithLinearScanAndLazyEncoding(IntegerVariable objective_var, const std::function< void()> &feasible_solution_observer, Model *model)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
std::string ProtobufShortDebugString(const P &message)
std::vector< double > coefficients
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
std::vector< IntegerValue > coeffs
std::vector< IntegerVariable > vars
IntegerVariable objective_var
double ScaleIntegerObjective(IntegerValue value) const
#define VLOG_IS_ON(verboselevel)