diff --git a/ortools/sat/2d_mandatory_overlap_propagator.cc b/ortools/sat/2d_mandatory_overlap_propagator.cc index c08b5ff5d1..c89eae4d64 100644 --- a/ortools/sat/2d_mandatory_overlap_propagator.cc +++ b/ortools/sat/2d_mandatory_overlap_propagator.cc @@ -49,7 +49,7 @@ MandatoryOverlapPropagator::~MandatoryOverlapPropagator() { } bool MandatoryOverlapPropagator::Propagate() { - if (!helper_.SynchronizeAndSetDirection(true, true, false)) return false; + if (!helper_.SynchronizeAndSetDirection()) return false; mandatory_regions_.clear(); mandatory_regions_index_.clear(); diff --git a/ortools/sat/BUILD.bazel b/ortools/sat/BUILD.bazel index cccb9ffdc3..cafe9924f9 100644 --- a/ortools/sat/BUILD.bazel +++ b/ortools/sat/BUILD.bazel @@ -110,6 +110,43 @@ cc_library( ], ) +cc_library( + name = "cp_model_copy", + srcs = ["cp_model_copy.cc"], + hdrs = ["cp_model_copy.h"], + deps = [ + ":cp_model_cc_proto", + ":cp_model_utils", + ":presolve_context", + ":sat_parameters_cc_proto", + "//ortools/base", + "//ortools/base:protobuf_util", + "//ortools/util:sorted_interval_list", + "@com_google_absl//absl/container:flat_hash_set", + "@com_google_absl//absl/log", + "@com_google_absl//absl/log:check", + "@com_google_absl//absl/strings", + "@com_google_absl//absl/types:span", + "@com_google_protobuf//:protobuf", + ], +) + +cc_test( + name = "cp_model_copy_test", + srcs = ["cp_model_copy_test.cc"], + deps = [ + ":cp_model_cc_proto", + ":cp_model_copy", + ":model", + ":presolve_context", + ":sat_parameters_cc_proto", + "//ortools/base:gmock_main", + "//ortools/base:parse_test_proto", + "//ortools/base:protobuf_util", + "//ortools/linear_solver:linear_solver_cc_proto", + ], +) + cc_proto_library( name = "cp_model_cc_proto", deps = [":cp_model_proto"], @@ -509,6 +546,7 @@ cc_library( hdrs = ["shaving_solver.h"], deps = [ ":cp_model_cc_proto", + ":cp_model_copy", ":cp_model_lns", ":cp_model_presolve", ":cp_model_solver_helpers", @@ -543,6 +581,7 @@ cc_library( ":combine_solutions", ":cp_model_cc_proto", ":cp_model_checker", + ":cp_model_copy", ":cp_model_lns", ":cp_model_loader", ":cp_model_mapping", @@ -649,6 +688,7 @@ cc_library( deps = [ ":all_different", ":circuit", + ":clause", ":cp_constraints", ":cp_model_cc_proto", ":cp_model_mapping", @@ -3388,8 +3428,8 @@ cc_library( hdrs = ["cp_model_lns.h"], deps = [ ":cp_model_cc_proto", + ":cp_model_copy", ":cp_model_mapping", - ":cp_model_presolve", ":cp_model_solver_helpers", ":cp_model_utils", ":diffn_util", diff --git a/ortools/sat/clause.cc b/ortools/sat/clause.cc index 49f63de461..6397a34ed3 100644 --- a/ortools/sat/clause.cc +++ b/ortools/sat/clause.cc @@ -2381,6 +2381,7 @@ void BinaryImplicationGraph::MarkDescendants(Literal root) { const Literal current = stack[j]; if (!implies_something[current]) continue; + work_done_in_mark_descendants_ += implications_[current].size(); for (const Literal l : implications_[current]) { if (!is_marked[l] && !is_redundant[l]) { is_marked_.SetUnsafe(is_marked, l); @@ -2390,6 +2391,7 @@ void BinaryImplicationGraph::MarkDescendants(Literal root) { if (current.Index() >= amo_size) continue; for (const int start : at_most_ones_[current]) { + work_done_in_mark_descendants_ += AtMostOne(start).size(); for (const Literal l : AtMostOne(start)) { if (l == current) continue; if (!is_marked[l.NegatedIndex()] && !is_redundant[l.NegatedIndex()]) { diff --git a/ortools/sat/cp_model_copy.cc b/ortools/sat/cp_model_copy.cc new file mode 100644 index 0000000000..ff05407aef --- /dev/null +++ b/ortools/sat/cp_model_copy.cc @@ -0,0 +1,973 @@ +// Copyright 2010-2025 Google LLC +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +#include "ortools/sat/cp_model_copy.h" + +#include +#include +#include +#include +#include +#include +#include + +#include "absl/container/flat_hash_set.h" +#include "absl/log/check.h" +#include "absl/strings/str_cat.h" +#include "absl/types/span.h" +#include "google/protobuf/arena.h" +#include "google/protobuf/repeated_field.h" +#include "google/protobuf/repeated_ptr_field.h" +#include "google/protobuf/text_format.h" +#include "ortools/base/logging.h" +#include "ortools/base/protobuf_util.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_utils.h" +#include "ortools/sat/presolve_context.h" +#include "ortools/sat/sat_parameters.pb.h" +#include "ortools/util/sorted_interval_list.h" + +namespace operations_research { +namespace sat { + +ModelCopy::ModelCopy(PresolveContext* context) : context_(context) {} + +void ModelCopy::ImportVariablesAndMaybeIgnoreNames( + const CpModelProto& in_model) { + if (context_->params().ignore_names()) { + context_->working_model->clear_variables(); + context_->working_model->mutable_variables()->Reserve( + in_model.variables_size()); + for (const IntegerVariableProto& var_proto : in_model.variables()) { + *context_->working_model->add_variables()->mutable_domain() = + var_proto.domain(); + } + } else { + *context_->working_model->mutable_variables() = in_model.variables(); + } +} + +void ModelCopy::CreateVariablesFromDomains(absl::Span domains) { + for (const Domain& domain : domains) { + FillDomainInProto(domain, context_->working_model->add_variables()); + } +} + +// TODO(user): Merge with the phase 1 of the presolve code. +// +// TODO(user): It seems easy to forget to update this if any new constraint +// contains an interval or if we add a field to an existing constraint. Find a +// way to remind contributor to not forget this. +bool ModelCopy::ImportAndSimplifyConstraints( + const CpModelProto& in_model, bool first_copy, + std::function active_constraints) { + context_->InitializeNewDomains(); + if (context_->ModelIsUnsat()) return false; + const bool ignore_names = context_->params().ignore_names(); + + // If first_copy is true, we reorder the scheduling constraint to be sure they + // refer to interval before them. + std::vector constraints_using_intervals; + + interval_mapping_.assign(in_model.constraints().size(), -1); + + starting_constraint_index_ = context_->working_model->constraints_size(); + for (int c = 0; c < in_model.constraints_size(); ++c) { + if (active_constraints != nullptr && !active_constraints(c)) continue; + const ConstraintProto& ct = in_model.constraints(c); + if (first_copy) { + if (!PrepareEnforcementCopyWithDup(ct)) continue; + } else { + if (!PrepareEnforcementCopy(ct)) continue; + } + + // TODO(user): if ignore_names is false, we should make sure the + // name are properly copied by all these functions. Or we should never copy + // name and have a separate if (!ignore_name) copy the name... + switch (ct.constraint_case()) { + case ConstraintProto::CONSTRAINT_NOT_SET: + break; + case ConstraintProto::kBoolOr: + if (first_copy) { + if (!CopyBoolOrWithDupSupport(ct)) return CreateUnsatModel(c, ct); + } else { + if (!CopyBoolOr(ct)) return CreateUnsatModel(c, ct); + } + break; + case ConstraintProto::kBoolAnd: + if (temp_enforcement_literals_.empty()) { + for (const int lit : ct.bool_and().literals()) { + context_->UpdateRuleStats("bool_and: non-reified."); + if (!context_->SetLiteralToTrue(lit)) { + return CreateUnsatModel(c, ct); + } + } + } else if (first_copy) { + if (!CopyBoolAndWithDupSupport(ct)) return CreateUnsatModel(c, ct); + } else { + if (!CopyBoolAnd(ct)) return CreateUnsatModel(c, ct); + } + break; + case ConstraintProto::kLinear: + if (!CopyLinear(ct)) return CreateUnsatModel(c, ct); + break; + case ConstraintProto::kIntProd: + if (!CopyIntProd(ct, ignore_names)) return CreateUnsatModel(c, ct); + break; + case ConstraintProto::kIntDiv: + if (!CopyIntDiv(ct, ignore_names)) return CreateUnsatModel(c, ct); + break; + case ConstraintProto::kIntMod: + if (!CopyIntMod(ct, ignore_names)) return CreateUnsatModel(c, ct); + break; + case ConstraintProto::kElement: + if (!CopyElement(ct)) return CreateUnsatModel(c, ct); + break; + case ConstraintProto::kTable: + if (!CopyTable(ct)) return CreateUnsatModel(c, ct); + break; + case ConstraintProto::kAutomaton: + if (!CopyAutomaton(ct)) return CreateUnsatModel(c, ct); + break; + case ConstraintProto::kAllDiff: + if (!CopyAllDiff(ct)) return CreateUnsatModel(c, ct); + break; + case ConstraintProto::kLinMax: + if (!CopyLinMax(ct)) return CreateUnsatModel(c, ct); + break; + case ConstraintProto::kAtMostOne: + if (!CopyAtMostOne(ct)) return CreateUnsatModel(c, ct); + break; + case ConstraintProto::kExactlyOne: + if (!CopyExactlyOne(ct)) return CreateUnsatModel(c, ct); + break; + case ConstraintProto::kInterval: + if (!CopyInterval(ct, c, ignore_names)) return CreateUnsatModel(c, ct); + if (first_copy) { + if (!AddLinearConstraintForInterval(ct)) + return CreateUnsatModel(c, ct); + } + break; + case ConstraintProto::kNoOverlap: + if (first_copy) { + constraints_using_intervals.push_back(c); + } else { + CopyAndMapNoOverlap(ct); + } + break; + case ConstraintProto::kNoOverlap2D: + if (first_copy) { + constraints_using_intervals.push_back(c); + } else { + CopyAndMapNoOverlap2D(ct); + } + break; + case ConstraintProto::kCumulative: + if (first_copy) { + constraints_using_intervals.push_back(c); + } else { + if (!CopyAndMapCumulative(ct)) return CreateUnsatModel(c, ct); + } + break; + default: { + ConstraintProto* new_ct = context_->working_model->add_constraints(); + *new_ct = ct; + new_ct->mutable_enforcement_literal()->Clear(); + FinishEnforcementCopy(new_ct); + if (ignore_names) { + // TODO(user): find a better way than copy then clear_name()? + new_ct->clear_name(); + } + } + } + } + + // This should be empty if first_copy is false. + DCHECK(first_copy || constraints_using_intervals.empty()); + for (const int c : constraints_using_intervals) { + const ConstraintProto& ct = in_model.constraints(c); + switch (ct.constraint_case()) { + case ConstraintProto::kNoOverlap: + CopyAndMapNoOverlap(ct); + break; + case ConstraintProto::kNoOverlap2D: + CopyAndMapNoOverlap2D(ct); + break; + case ConstraintProto::kCumulative: + if (!CopyAndMapCumulative(ct)) return CreateUnsatModel(c, ct); + break; + default: + LOG(DFATAL) << "Shouldn't be here."; + } + } + + return true; +} + +bool ModelCopy::PrepareEnforcementCopy(const ConstraintProto& ct) { + temp_enforcement_literals_.clear(); + for (const int lit : ct.enforcement_literal()) { + if (context_->LiteralIsTrue(lit)) continue; + if (context_->LiteralIsFalse(lit)) { + context_->UpdateRuleStats("enforcement: always false"); + return false; + } + temp_enforcement_literals_.push_back(lit); + } + return true; // Continue processing. +} + +bool ModelCopy::PrepareEnforcementCopyWithDup(const ConstraintProto& ct) { + temp_enforcement_literals_.clear(); + temp_enforcement_literals_set_.clear(); + for (const int lit : ct.enforcement_literal()) { + if (context_->LiteralIsTrue(lit)) continue; + if (temp_enforcement_literals_set_.contains(lit)) { + context_->UpdateRuleStats("enforcement: removed duplicate literal"); + continue; + } + + // Cannot be satisfied. + if (context_->LiteralIsFalse(lit)) { + context_->UpdateRuleStats("enforcement: always false"); + return false; + } + if (temp_enforcement_literals_set_.contains(NegatedRef(lit))) { + context_->UpdateRuleStats("enforcement: contains x and not(x)"); + return false; + } + + temp_enforcement_literals_.push_back(lit); + temp_enforcement_literals_set_.insert(lit); + } + return true; // Continue processing. +} + +void ModelCopy::FinishEnforcementCopy(ConstraintProto* ct) { + ct->mutable_enforcement_literal()->Add(temp_enforcement_literals_.begin(), + temp_enforcement_literals_.end()); +} + +bool ModelCopy::FinishBoolOrCopy() { + if (temp_literals_.empty()) return false; + + if (temp_literals_.size() == 1) { + context_->UpdateRuleStats("bool_or: only one literal"); + return context_->SetLiteralToTrue(temp_literals_[0]); + } + + context_->working_model->add_constraints() + ->mutable_bool_or() + ->mutable_literals() + ->Add(temp_literals_.begin(), temp_literals_.end()); + return true; +} + +bool ModelCopy::CopyBoolOr(const ConstraintProto& ct) { + temp_literals_.clear(); + for (const int lit : temp_enforcement_literals_) { + temp_literals_.push_back(NegatedRef(lit)); + } + for (const int lit : ct.bool_or().literals()) { + if (context_->LiteralIsTrue(lit)) { + return true; + } + if (!context_->LiteralIsFalse(lit)) { + temp_literals_.push_back(lit); + } + } + return FinishBoolOrCopy(); +} + +bool ModelCopy::CopyBoolOrWithDupSupport(const ConstraintProto& ct) { + temp_literals_.clear(); + temp_literals_set_.clear(); + for (const int enforcement_lit : temp_enforcement_literals_) { + // Having an enforcement literal is the same as having its negation on + // the clause. + const int lit = NegatedRef(enforcement_lit); + + // Note that we already dealt with duplicate since we should have called + // PrepareEnforcementCopyWithDup() in this case. + temp_literals_set_.insert(lit); + temp_literals_.push_back(lit); + } + for (const int lit : ct.bool_or().literals()) { + if (context_->LiteralIsTrue(lit)) { + context_->UpdateRuleStats("bool_or: always true"); + return true; + } + if (context_->LiteralIsFalse(lit)) continue; + if (temp_literals_set_.contains(NegatedRef(lit))) { + context_->UpdateRuleStats("bool_or: always true"); + return true; + } + const auto [it, inserted] = temp_literals_set_.insert(lit); + if (inserted) temp_literals_.push_back(lit); + } + return FinishBoolOrCopy(); +} + +bool ModelCopy::CopyBoolAnd(const ConstraintProto& ct) { + bool at_least_one_false = false; + int num_non_fixed_literals = 0; + for (const int lit : ct.bool_and().literals()) { + if (context_->LiteralIsFalse(lit)) { + at_least_one_false = true; + break; + } + if (!context_->LiteralIsTrue(lit)) { + num_non_fixed_literals++; + } + } + + if (at_least_one_false) { + // One enforcement literal must be false. + BoolArgumentProto* bool_or = + context_->working_model->add_constraints()->mutable_bool_or(); + for (const int lit : temp_enforcement_literals_) { + bool_or->add_literals(NegatedRef(lit)); + } + return !bool_or->literals().empty(); + } else if (num_non_fixed_literals > 0) { + ConstraintProto* new_ct = context_->working_model->add_constraints(); + FinishEnforcementCopy(new_ct); + BoolArgumentProto* bool_and = new_ct->mutable_bool_and(); + bool_and->mutable_literals()->Reserve(num_non_fixed_literals); + for (const int lit : ct.bool_and().literals()) { + if (context_->LiteralIsTrue(lit)) continue; + bool_and->add_literals(lit); + } + } + return true; +} + +bool ModelCopy::CopyBoolAndWithDupSupport(const ConstraintProto& ct) { + DCHECK(!temp_enforcement_literals_.empty()); + + bool at_least_one_false = false; + temp_literals_.clear(); + temp_literals_set_.clear(); + for (const int lit : ct.bool_and().literals()) { + if (context_->LiteralIsFalse(lit)) { + context_->UpdateRuleStats("bool and: always false"); + at_least_one_false = true; + break; + } + if (temp_literals_set_.contains(NegatedRef(lit))) { + context_->UpdateRuleStats("bool and: => x and not(x) "); + at_least_one_false = true; + break; + } + if (temp_enforcement_literals_set_.contains(NegatedRef(lit))) { + context_->UpdateRuleStats("bool and: not(x) => x"); + at_least_one_false = true; + break; + } + + if (context_->LiteralIsTrue(lit)) continue; + if (temp_enforcement_literals_set_.contains(lit)) { + context_->UpdateRuleStats("bool and: x => x"); + continue; + } + const auto [it, inserted] = temp_literals_set_.insert(lit); + if (inserted) temp_literals_.push_back(lit); + } + + if (at_least_one_false) { + // One enforcement literal must be false. + BoolArgumentProto* bool_or = + context_->working_model->add_constraints()->mutable_bool_or(); + for (const int lit : temp_enforcement_literals_) { + bool_or->add_literals(NegatedRef(lit)); + } + return !bool_or->literals().empty(); + } + + if (temp_literals_.empty()) { + context_->UpdateRuleStats("bool and: empty"); + return true; + } + + // Copy. + ConstraintProto* new_ct = context_->working_model->add_constraints(); + FinishEnforcementCopy(new_ct); + new_ct->mutable_bool_and()->mutable_literals()->Add(temp_literals_.begin(), + temp_literals_.end()); + return true; +} + +bool ModelCopy::CopyLinearExpression(const LinearExpressionProto& expr, + LinearExpressionProto* dst) { + non_fixed_variables_.clear(); + non_fixed_coefficients_.clear(); + int64_t offset = expr.offset(); + for (int i = 0; i < expr.vars_size(); ++i) { + const int ref = expr.vars(i); + const int64_t coeff = expr.coeffs(i); + if (coeff == 0) continue; + if (context_->IsFixed(ref)) { + offset += coeff * context_->MinOf(ref); + continue; + } + + // Make sure we never have negative ref in a linear constraint. + if (RefIsPositive(ref)) { + non_fixed_variables_.push_back(ref); + non_fixed_coefficients_.push_back(coeff); + } else { + non_fixed_variables_.push_back(NegatedRef(ref)); + non_fixed_coefficients_.push_back(-coeff); + } + } + + dst->set_offset(offset); + dst->mutable_vars()->Add(non_fixed_variables_.begin(), + non_fixed_variables_.end()); + dst->mutable_coeffs()->Add(non_fixed_coefficients_.begin(), + non_fixed_coefficients_.end()); + return true; +} + +bool ModelCopy::CopyLinear(const ConstraintProto& ct) { + non_fixed_variables_.clear(); + non_fixed_coefficients_.clear(); + int64_t offset = 0; + int64_t min_activity = 0; + int64_t max_activity = 0; + for (int i = 0; i < ct.linear().vars_size(); ++i) { + const int ref = ct.linear().vars(i); + const int64_t coeff = ct.linear().coeffs(i); + if (coeff == 0) continue; + if (context_->IsFixed(ref)) { + offset += coeff * context_->MinOf(ref); + continue; + } + + if (coeff > 0) { + min_activity += coeff * context_->MinOf(ref); + max_activity += coeff * context_->MaxOf(ref); + } else { + min_activity += coeff * context_->MaxOf(ref); + max_activity += coeff * context_->MinOf(ref); + } + + // Make sure we never have negative ref in a linear constraint. + if (RefIsPositive(ref)) { + non_fixed_variables_.push_back(ref); + non_fixed_coefficients_.push_back(coeff); + } else { + non_fixed_variables_.push_back(NegatedRef(ref)); + non_fixed_coefficients_.push_back(-coeff); + } + } + + const Domain implied(min_activity, max_activity); + const Domain new_rhs = + ReadDomainFromProto(ct.linear()).AdditionWith(Domain(-offset)); + + // Trivial constraint? + if (implied.IsIncludedIn(new_rhs)) { + context_->UpdateRuleStats("linear: always true"); + return true; + } + + // Constraint is false? + const Domain tight_domain = implied.IntersectionWith(new_rhs); + if (tight_domain.IsEmpty()) { + if (ct.enforcement_literal().empty()) return false; + temp_literals_.clear(); + for (const int literal : ct.enforcement_literal()) { + if (!context_->LiteralIsTrue(literal)) { + temp_literals_.push_back(NegatedRef(literal)); + } + } + context_->working_model->add_constraints() + ->mutable_bool_or() + ->mutable_literals() + ->Add(temp_literals_.begin(), temp_literals_.end()); + return !temp_literals_.empty(); + } + + DCHECK(!non_fixed_variables_.empty()); + + if (non_fixed_variables_.size() == 1 && ct.enforcement_literal().empty()) { + context_->UpdateRuleStats("linear1: x in domain"); + return context_->IntersectDomainWith( + non_fixed_variables_[0], + new_rhs.InverseMultiplicationBy(non_fixed_coefficients_[0])); + } + + ConstraintProto* new_ct = context_->working_model->add_constraints(); + FinishEnforcementCopy(new_ct); + LinearConstraintProto* linear = new_ct->mutable_linear(); + linear->mutable_vars()->Add(non_fixed_variables_.begin(), + non_fixed_variables_.end()); + linear->mutable_coeffs()->Add(non_fixed_coefficients_.begin(), + non_fixed_coefficients_.end()); + FillDomainInProto(tight_domain, linear); + return true; +} + +bool ModelCopy::CopyElement(const ConstraintProto& ct) { + ConstraintProto* new_ct = context_->working_model->add_constraints(); + if (ct.element().vars().empty() && !ct.element().exprs().empty()) { + // New format, just copy. + *new_ct = ct; + return true; + } + + auto fill_expr = [this](int var, LinearExpressionProto* expr) mutable { + if (context_->IsFixed(var)) { + expr->set_offset(context_->FixedValue(var)); + } else { + DCHECK(RefIsPositive(var)); + expr->mutable_vars()->Reserve(1); + expr->mutable_coeffs()->Reserve(1); + expr->add_vars(var); + expr->add_coeffs(1); + } + }; + + fill_expr(ct.element().index(), + new_ct->mutable_element()->mutable_linear_index()); + fill_expr(ct.element().target(), + new_ct->mutable_element()->mutable_linear_target()); + for (const int var : ct.element().vars()) { + fill_expr(var, new_ct->mutable_element()->add_exprs()); + } + return true; +} + +bool ModelCopy::CopyAutomaton(const ConstraintProto& ct) { + ConstraintProto* new_ct = context_->working_model->add_constraints(); + *new_ct = ct; + if (new_ct->automaton().vars().empty()) return true; + + auto fill_expr = [this](int var, LinearExpressionProto* expr) mutable { + if (context_->IsFixed(var)) { + expr->set_offset(context_->FixedValue(var)); + } else { + DCHECK(RefIsPositive(var)); + expr->mutable_vars()->Reserve(1); + expr->mutable_coeffs()->Reserve(1); + expr->add_vars(var); + expr->add_coeffs(1); + } + }; + + for (const int var : ct.automaton().vars()) { + fill_expr(var, new_ct->mutable_automaton()->add_exprs()); + } + new_ct->mutable_automaton()->clear_vars(); + + return true; +} + +bool ModelCopy::CopyTable(const ConstraintProto& ct) { + ConstraintProto* new_ct = context_->working_model->add_constraints(); + if (ct.table().vars().empty() && !ct.table().exprs().empty()) { + // New format, just copy. + *new_ct = ct; + return true; + } + + auto fill_expr = [this](int var, LinearExpressionProto* expr) mutable { + if (context_->IsFixed(var)) { + expr->set_offset(context_->FixedValue(var)); + } else { + DCHECK(RefIsPositive(var)); + expr->mutable_vars()->Reserve(1); + expr->mutable_coeffs()->Reserve(1); + expr->add_vars(var); + expr->add_coeffs(1); + } + }; + + for (const int var : ct.table().vars()) { + fill_expr(var, new_ct->mutable_table()->add_exprs()); + } + *new_ct->mutable_table()->mutable_values() = ct.table().values(); + new_ct->mutable_table()->set_negated(ct.table().negated()); + *new_ct->mutable_enforcement_literal() = ct.enforcement_literal(); + + return true; +} + +bool ModelCopy::CopyAllDiff(const ConstraintProto& ct) { + if (ct.all_diff().exprs().size() <= 1) return true; + ConstraintProto* new_ct = context_->working_model->add_constraints(); + for (const LinearExpressionProto& expr : ct.all_diff().exprs()) { + CopyLinearExpression(expr, new_ct->mutable_all_diff()->add_exprs()); + } + return true; +} + +bool ModelCopy::CopyLinMax(const ConstraintProto& ct) { + // We will create it lazily if we end up copying something. + ConstraintProto* new_ct = nullptr; + + // Regroup all constant terms and copy the other. + int64_t max_of_fixed_terms = std::numeric_limits::min(); + for (const auto& expr : ct.lin_max().exprs()) { + const std::optional fixed = context_->FixedValueOrNullopt(expr); + if (fixed != std::nullopt) { + max_of_fixed_terms = std::max(max_of_fixed_terms, fixed.value()); + } else { + // copy. + if (new_ct == nullptr) { + new_ct = context_->working_model->add_constraints(); + } + CopyLinearExpression(expr, new_ct->mutable_lin_max()->add_exprs()); + } + } + + // If we have no non-fixed expression, we can just fix the target when it + // involve at most one variable. + if (new_ct == nullptr && ct.enforcement_literal().empty() && + ct.lin_max().target().vars().size() <= 1) { + context_->UpdateRuleStats("lin_max: all exprs fixed during copy"); + return context_->IntersectDomainWith(ct.lin_max().target(), + Domain(max_of_fixed_terms)); + } + + // Otherwise, add a constant term if needed. + if (max_of_fixed_terms > std::numeric_limits::min()) { + if (new_ct == nullptr) { + new_ct = context_->working_model->add_constraints(); + } + new_ct->mutable_lin_max()->add_exprs()->set_offset(max_of_fixed_terms); + } + + // Finish by copying the target. + if (new_ct == nullptr) return false; // No expr == unsat. + CopyLinearExpression(ct.lin_max().target(), + new_ct->mutable_lin_max()->mutable_target()); + return true; +} + +bool ModelCopy::CopyAtMostOne(const ConstraintProto& ct) { + int num_true = 0; + temp_literals_.clear(); + for (const int lit : ct.at_most_one().literals()) { + if (context_->LiteralIsFalse(lit)) continue; + temp_literals_.push_back(lit); + if (context_->LiteralIsTrue(lit)) num_true++; + } + + if (temp_literals_.size() <= 1) return true; + if (num_true > 1) return false; + + // TODO(user): presolve if num_true == 1. + ConstraintProto* new_ct = context_->working_model->add_constraints(); + FinishEnforcementCopy(new_ct); + new_ct->mutable_at_most_one()->mutable_literals()->Add(temp_literals_.begin(), + temp_literals_.end()); + return true; +} + +bool ModelCopy::CopyExactlyOne(const ConstraintProto& ct) { + int num_true = 0; + temp_literals_.clear(); + for (const int lit : ct.exactly_one().literals()) { + if (context_->LiteralIsFalse(lit)) continue; + temp_literals_.push_back(lit); + if (context_->LiteralIsTrue(lit)) num_true++; + } + + if (temp_literals_.empty() || num_true > 1) return false; + if (temp_literals_.size() == 1 && num_true == 1) return true; + + // TODO(user): presolve if num_true == 1 and not everything is false. + ConstraintProto* new_ct = context_->working_model->add_constraints(); + FinishEnforcementCopy(new_ct); + new_ct->mutable_exactly_one()->mutable_literals()->Add(temp_literals_.begin(), + temp_literals_.end()); + return true; +} + +bool ModelCopy::CopyInterval(const ConstraintProto& ct, int c, + bool ignore_names) { + CHECK_EQ(starting_constraint_index_, 0) + << "Adding new interval constraints to partially filled model is not " + "supported."; + interval_mapping_[c] = context_->working_model->constraints_size(); + ConstraintProto* new_ct = context_->working_model->add_constraints(); + if (!ignore_names) { + new_ct->set_name(ct.name()); + } + *new_ct->mutable_enforcement_literal() = ct.enforcement_literal(); + CopyLinearExpression(ct.interval().start(), + new_ct->mutable_interval()->mutable_start()); + CopyLinearExpression(ct.interval().size(), + new_ct->mutable_interval()->mutable_size()); + CopyLinearExpression(ct.interval().end(), + new_ct->mutable_interval()->mutable_end()); + return true; +} + +bool ModelCopy::CopyIntProd(const ConstraintProto& ct, bool ignore_names) { + ConstraintProto* new_ct = context_->working_model->add_constraints(); + if (!ignore_names) { + new_ct->set_name(ct.name()); + } + for (const LinearExpressionProto& expr : ct.int_prod().exprs()) { + CopyLinearExpression(expr, new_ct->mutable_int_prod()->add_exprs()); + } + CopyLinearExpression(ct.int_prod().target(), + new_ct->mutable_int_prod()->mutable_target()); + return true; +} + +bool ModelCopy::CopyIntDiv(const ConstraintProto& ct, bool ignore_names) { + ConstraintProto* new_ct = context_->working_model->add_constraints(); + if (!ignore_names) { + new_ct->set_name(ct.name()); + } + for (const LinearExpressionProto& expr : ct.int_div().exprs()) { + CopyLinearExpression(expr, new_ct->mutable_int_div()->add_exprs()); + } + CopyLinearExpression(ct.int_div().target(), + new_ct->mutable_int_div()->mutable_target()); + return true; +} + +bool ModelCopy::CopyIntMod(const ConstraintProto& ct, bool ignore_names) { + ConstraintProto* new_ct = context_->working_model->add_constraints(); + if (!ignore_names) { + new_ct->set_name(ct.name()); + } + for (const LinearExpressionProto& expr : ct.int_mod().exprs()) { + CopyLinearExpression(expr, new_ct->mutable_int_mod()->add_exprs()); + } + CopyLinearExpression(ct.int_mod().target(), + new_ct->mutable_int_mod()->mutable_target()); + return true; +} + +bool ModelCopy::AddLinearConstraintForInterval(const ConstraintProto& ct) { + // Add the linear constraint enforcement => (start + size == end). + // + // We rely on the presolve for simplification, but deal with the trivial + // case of (start, offset, start + offset) here. + const IntervalConstraintProto& itv = ct.interval(); + if (itv.size().vars().empty() && + itv.start().offset() + itv.size().offset() == itv.end().offset() && + absl::Span(itv.start().vars()) == + absl::Span(itv.end().vars()) && + absl::Span(itv.start().coeffs()) == + absl::Span(itv.end().coeffs())) { + // Trivial constraint, nothing to do. + } else { + tmp_constraint_.Clear(); + *tmp_constraint_.mutable_enforcement_literal() = ct.enforcement_literal(); + LinearConstraintProto* mutable_linear = tmp_constraint_.mutable_linear(); + + mutable_linear->add_domain(0); + mutable_linear->add_domain(0); + AddLinearExpressionToLinearConstraint(itv.start(), 1, mutable_linear); + AddLinearExpressionToLinearConstraint(itv.size(), 1, mutable_linear); + AddLinearExpressionToLinearConstraint(itv.end(), -1, mutable_linear); + if (!CopyLinear(tmp_constraint_)) return false; + } + + // An enforced interval must have is size non-negative. + const LinearExpressionProto& size_expr = itv.size(); + if (context_->MinOf(size_expr) < 0) { + tmp_constraint_.Clear(); + *tmp_constraint_.mutable_enforcement_literal() = ct.enforcement_literal(); + *tmp_constraint_.mutable_linear()->mutable_vars() = size_expr.vars(); + *tmp_constraint_.mutable_linear()->mutable_coeffs() = size_expr.coeffs(); + tmp_constraint_.mutable_linear()->add_domain(-size_expr.offset()); + tmp_constraint_.mutable_linear()->add_domain( + std::numeric_limits::max()); + if (!CopyLinear(tmp_constraint_)) return false; + } + + return true; +} + +void ModelCopy::CopyAndMapNoOverlap(const ConstraintProto& ct) { + // Note that we don't copy names or enforcement_literal (not supported) here. + auto* new_ct = + context_->working_model->add_constraints()->mutable_no_overlap(); + new_ct->mutable_intervals()->Reserve(ct.no_overlap().intervals().size()); + for (const int index : ct.no_overlap().intervals()) { + const int new_index = interval_mapping_[index]; + if (new_index != -1) { + new_ct->add_intervals(new_index); + } + } +} + +void ModelCopy::CopyAndMapNoOverlap2D(const ConstraintProto& ct) { + // Note that we don't copy names or enforcement_literal (not supported) here. + auto* new_ct = + context_->working_model->add_constraints()->mutable_no_overlap_2d(); + + const int num_intervals = ct.no_overlap_2d().x_intervals().size(); + new_ct->mutable_x_intervals()->Reserve(num_intervals); + new_ct->mutable_y_intervals()->Reserve(num_intervals); + for (int i = 0; i < num_intervals; ++i) { + const int new_x = interval_mapping_[ct.no_overlap_2d().x_intervals(i)]; + if (new_x == -1) continue; + const int new_y = interval_mapping_[ct.no_overlap_2d().y_intervals(i)]; + if (new_y == -1) continue; + new_ct->add_x_intervals(new_x); + new_ct->add_y_intervals(new_y); + } +} + +bool ModelCopy::CopyAndMapCumulative(const ConstraintProto& ct) { + if (ct.cumulative().intervals().empty() && + context_->IsFixed(ct.cumulative().capacity())) { + // Trivial constraint, either obviously SAT or UNSAT. + return context_->FixedValue(ct.cumulative().capacity()) >= 0; + } + // Note that we don't copy names or enforcement_literal (not supported) here. + auto* new_ct = + context_->working_model->add_constraints()->mutable_cumulative(); + CopyLinearExpression(ct.cumulative().capacity(), new_ct->mutable_capacity()); + + const int num_intervals = ct.cumulative().intervals().size(); + new_ct->mutable_intervals()->Reserve(num_intervals); + new_ct->mutable_demands()->Reserve(num_intervals); + for (int i = 0; i < num_intervals; ++i) { + const int new_index = interval_mapping_[ct.cumulative().intervals(i)]; + if (new_index != -1) { + new_ct->add_intervals(new_index); + *new_ct->add_demands() = ct.cumulative().demands(i); + } + } + + return true; +} + +bool ModelCopy::CreateUnsatModel(int c, const ConstraintProto& ct) { + context_->working_model->mutable_constraints()->Clear(); + context_->working_model->add_constraints()->mutable_bool_or(); + + // If the model was already marked as unsat, we keep the old message and just + // return. TODO(user): Append messages instead? + if (context_->ModelIsUnsat()) return false; + + std::string proto_string; +#if !defined(__PORTABLE_PLATFORM__) + google::protobuf::TextFormat::Printer printer; + SetupTextFormatPrinter(&printer); + printer.PrintToString(ct, &proto_string); +#endif // !defined(__PORTABLE_PLATFORM__) + std::string message = absl::StrCat( + "proven during initial copy of constraint #", c, ":\n", proto_string); + std::vector vars = UsedVariables(ct); + if (vars.size() < 10) { + absl::StrAppend(&message, "With current variable domains:\n"); + for (const int var : vars) { + absl::StrAppend(&message, "var:", var, + " domain:", context_->DomainOf(var).ToString(), "\n"); + } + } + return context_->NotifyThatModelIsUnsat(message); +} + +bool ImportModelWithBasicPresolveIntoContext(const CpModelProto& in_model, + PresolveContext* context) { + ModelCopy copier(context); + copier.ImportVariablesAndMaybeIgnoreNames(in_model); + if (copier.ImportAndSimplifyConstraints(in_model, /*first_copy=*/true)) { + CopyEverythingExceptVariablesAndConstraintsFieldsIntoContext(in_model, + context); + return true; + } + return !context->ModelIsUnsat(); +} + +bool ImportModelAndDomainsWithBasicPresolveIntoContext( + const CpModelProto& in_model, absl::Span domains, + std::function active_constraints, PresolveContext* context) { + CHECK_EQ(domains.size(), in_model.variables_size()); + ModelCopy copier(context); + copier.CreateVariablesFromDomains(domains); + if (copier.ImportAndSimplifyConstraints(in_model, /*first_copy=*/false, + active_constraints)) { + CopyEverythingExceptVariablesAndConstraintsFieldsIntoContext(in_model, + context); + return true; + } + return !context->ModelIsUnsat(); +} + +void CopyEverythingExceptVariablesAndConstraintsFieldsIntoContext( + const CpModelProto& in_model, PresolveContext* context) { + if (!in_model.name().empty()) { + context->working_model->set_name(in_model.name()); + } + if (in_model.has_objective()) { + *context->working_model->mutable_objective() = in_model.objective(); + } + if (in_model.has_floating_point_objective()) { + *context->working_model->mutable_floating_point_objective() = + in_model.floating_point_objective(); + } + if (!in_model.search_strategy().empty()) { + // We make sure we do not use the old variables field. + *context->working_model->mutable_search_strategy() = + in_model.search_strategy(); + for (DecisionStrategyProto& strategy : + *context->working_model->mutable_search_strategy()) { + google::protobuf::util::RemoveIf(strategy.mutable_exprs(), + [](const LinearExpressionProto* expr) { + return expr->vars().empty(); + }); + if (!strategy.variables().empty()) { + CHECK(strategy.exprs().empty()); + for (const int ref : strategy.variables()) { + LinearExpressionProto* expr = strategy.add_exprs(); + expr->add_vars(PositiveRef(ref)); + expr->add_coeffs(RefIsPositive(ref) ? 1 : -1); + } + strategy.clear_variables(); + } + } + } + if (!in_model.assumptions().empty()) { + *context->working_model->mutable_assumptions() = in_model.assumptions(); + } + if (in_model.has_symmetry()) { + *context->working_model->mutable_symmetry() = in_model.symmetry(); + } + if (in_model.has_solution_hint()) { + *context->working_model->mutable_solution_hint() = in_model.solution_hint(); + + // We make sure the hint is within the variables domain. + // + // This allows to avoid overflow because we know evaluating constraints on + // the variables domains should be safe thanks to the initial validation. + const int num_terms = in_model.solution_hint().vars().size(); + for (int i = 0; i < num_terms; ++i) { + const int var = in_model.solution_hint().vars(i); + const int64_t value = in_model.solution_hint().values(i); + const Domain& domain = ReadDomainFromProto(in_model.variables(var)); + if (domain.IsEmpty()) continue; // UNSAT. + const int64_t closest_domain_value = domain.ClosestValue(value); + if (closest_domain_value != value) { + context->UpdateRuleStats("hint: moved var hint within its domain."); + context->working_model->mutable_solution_hint()->set_values( + i, closest_domain_value); + } + } + } +} + +} // namespace sat +} // namespace operations_research diff --git a/ortools/sat/cp_model_copy.h b/ortools/sat/cp_model_copy.h new file mode 100644 index 0000000000..8522af873d --- /dev/null +++ b/ortools/sat/cp_model_copy.h @@ -0,0 +1,155 @@ +// Copyright 2010-2025 Google LLC +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +#ifndef OR_TOOLS_SAT_CP_MODEL_COPY_H_ +#define OR_TOOLS_SAT_CP_MODEL_COPY_H_ + +#include +#include +#include + +#include "absl/container/flat_hash_set.h" +#include "absl/types/span.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/presolve_context.h" +#include "ortools/sat/sat_parameters.pb.h" +#include "ortools/util/sorted_interval_list.h" + +namespace operations_research { +namespace sat { + +// This helper class perform copy with simplification from a model and a +// partial assignment to another model. The purpose is to minimize the size of +// the copied model, as well as to reduce the pressure on the memory sub-system. +// +// It is currently used by the LNS part, but could be used with any other scheme +// that generates partial assignments. +class ModelCopy { + public: + explicit ModelCopy(PresolveContext* context); + + // Copies all constraints from in_model to working model of the context. + // + // During the process, it will read variable domains from the context, and + // simplify constraints to minimize the size of the copied model. + // Thus it is important that the context->working_model already have the + // variables part copied. + // + // It returns false iff the model is proven infeasible. + // + // It does not clear the constraints part of the working model of the context. + // + // Note(user): If first_copy is true, we will reorder the scheduling + // constraint so that they only use reference to previously defined intervals. + // This allow to be more efficient later in a few preprocessing steps. + bool ImportAndSimplifyConstraints( + const CpModelProto& in_model, bool first_copy = false, + std::function active_constraints = nullptr); + + // Copy variables from the in_model to the working model. + // It reads the 'ignore_names' parameters from the context, and keeps or + // deletes names accordingly. + void ImportVariablesAndMaybeIgnoreNames(const CpModelProto& in_model); + + // Setup new variables from a vector of domains. + // Inactive variables will be fixed to their lower bound. + void CreateVariablesFromDomains(absl::Span domains); + + private: + // Overwrites the out_model to be unsat. Returns false. + // The arguments are used to log which constraint caused unsat. + bool CreateUnsatModel(int c, const ConstraintProto& ct); + + // Returns false if the constraint is never enforced and can be skipped. + bool PrepareEnforcementCopy(const ConstraintProto& ct); + bool PrepareEnforcementCopyWithDup(const ConstraintProto& ct); + void FinishEnforcementCopy(ConstraintProto* ct); + + // All these functions return false if the constraint is found infeasible. + bool CopyBoolOr(const ConstraintProto& ct); + bool CopyBoolOrWithDupSupport(const ConstraintProto& ct); + bool FinishBoolOrCopy(); + + bool CopyBoolAnd(const ConstraintProto& ct); + bool CopyBoolAndWithDupSupport(const ConstraintProto& ct); + + bool CopyAtMostOne(const ConstraintProto& ct); + bool CopyExactlyOne(const ConstraintProto& ct); + + bool CopyElement(const ConstraintProto& ct); + bool CopyIntProd(const ConstraintProto& ct, bool ignore_names); + bool CopyIntDiv(const ConstraintProto& ct, bool ignore_names); + bool CopyIntMod(const ConstraintProto& ct, bool ignore_names); + bool CopyLinear(const ConstraintProto& ct); + bool CopyLinearExpression(const LinearExpressionProto& expr, + LinearExpressionProto* dst); + bool CopyAutomaton(const ConstraintProto& ct); + bool CopyTable(const ConstraintProto& ct); + bool CopyAllDiff(const ConstraintProto& ct); + bool CopyLinMax(const ConstraintProto& ct); + + // If we "copy" an interval for a first time, we make sure to create the + // linear constraint between the start, size and end. This allow to simplify + // the input proto and client side code. + bool CopyInterval(const ConstraintProto& ct, int c, bool ignore_names); + bool AddLinearConstraintForInterval(const ConstraintProto& ct); + + // These function remove unperformed intervals. Note that they requires + // interval to appear before (validated) as they test unperformed by testing + // if interval_mapping_ is empty. + void CopyAndMapNoOverlap(const ConstraintProto& ct); + void CopyAndMapNoOverlap2D(const ConstraintProto& ct); + bool CopyAndMapCumulative(const ConstraintProto& ct); + + PresolveContext* context_; + + // Temp vectors. + std::vector non_fixed_variables_; + std::vector non_fixed_coefficients_; + std::vector interval_mapping_; + int starting_constraint_index_ = 0; + + std::vector temp_enforcement_literals_; + absl::flat_hash_set temp_enforcement_literals_set_; + + std::vector temp_literals_; + absl::flat_hash_set temp_literals_set_; + + ConstraintProto tmp_constraint_; +}; + +// Copy in_model to the model in the presolve context. +// It performs on the fly simplification, and returns false if the +// model is proved infeasible. If reads the parameters 'ignore_names' and keeps +// or deletes variables and constraints names accordingly. +// +// This should only be called on the first copy of the user given model. +// Note that this reorder all constraints that use intervals last. We loose the +// user-defined order, but hopefully that should not matter too much. +bool ImportModelWithBasicPresolveIntoContext(const CpModelProto& in_model, + PresolveContext* context); + +// Same as ImportModelWithBasicPresolveIntoContext() except that variable +// domains are read from domains. +bool ImportModelAndDomainsWithBasicPresolveIntoContext( + const CpModelProto& in_model, absl::Span domains, + std::function active_constraints, PresolveContext* context); + +// Copies the non constraint, non variables part of the model. +void CopyEverythingExceptVariablesAndConstraintsFieldsIntoContext( + const CpModelProto& in_model, PresolveContext* context); + +} // namespace sat +} // namespace operations_research + +#endif // OR_TOOLS_SAT_CP_MODEL_COPY_H_ diff --git a/ortools/sat/cp_model_copy_test.cc b/ortools/sat/cp_model_copy_test.cc new file mode 100644 index 0000000000..daad1d55d3 --- /dev/null +++ b/ortools/sat/cp_model_copy_test.cc @@ -0,0 +1,214 @@ +// Copyright 2010-2025 Google LLC +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +#include "ortools/sat/cp_model_copy.h" + +#include "gtest/gtest.h" +#include "ortools/base/gmock.h" +#include "ortools/base/parse_test_proto.h" +#include "ortools/base/protobuf_util.h" +#include "ortools/linear_solver/linear_solver.pb.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/model.h" +#include "ortools/sat/presolve_context.h" +#include "ortools/sat/sat_parameters.pb.h" + +namespace operations_research { +namespace sat { +namespace { + +using ::google::protobuf::contrib::parse_proto::ParseTestProto; +using ::testing::EqualsProto; +using ::testing::IsEmpty; + +TEST(ModelCopyTest, IntervalsAddLinearConstraints) { + const CpModelProto initial_model = ParseTestProto(R"pb( + variables { domain: [ 0, 1 ] } + variables { domain: [ -10, 10 ] } + variables { domain: [ -10, 10 ] } + variables { domain: [ -10, 10 ] } + constraints { + enforcement_literal: 0 + interval { + start: { vars: 1 coeffs: 1 } + size: { vars: 2 coeffs: 1 } + end: { vars: 3 coeffs: 1 } + } + } + )pb"); + + Model model; + CpModelProto new_cp_model; + PresolveContext context(&model, &new_cp_model, nullptr); + + ImportModelWithBasicPresolveIntoContext(initial_model, &context); + const CpModelProto expected_model = ParseTestProto(R"pb( + variables { domain: [ 0, 1 ] } + variables { domain: [ -10, 10 ] } + variables { domain: [ -10, 10 ] } + variables { domain: [ -10, 10 ] } + constraints { + enforcement_literal: 0 + interval { + start: { vars: 1 coeffs: 1 } + size: { vars: 2 coeffs: 1 } + end: { vars: 3 coeffs: 1 } + } + } + constraints { + enforcement_literal: 0 + linear { + vars: [ 1, 2, 3 ] + coeffs: [ 1, 1, -1 ] + domain: [ 0, 0 ] + } + } + + constraints { + enforcement_literal: 0 + linear { + vars: [ 2 ] + coeffs: [ 1 ] + domain: [ 0, 10 ] + } + } + )pb"); + EXPECT_THAT(new_cp_model, EqualsProto(expected_model)); +} + +TEST(ModelCopyTest, IntervalsWithFixedStartAndEnd) { + const CpModelProto initial_model = ParseTestProto(R"pb( + variables { domain: [ 10, 10 ] } + variables { domain: [ 10, 10 ] } + variables { domain: [ 10, 10 ] } + constraints { + interval { + start: { vars: 0 coeffs: 1 } + size: { vars: 1 coeffs: 1 } + end: { vars: 2 coeffs: 2 } + } + } + )pb"); + + Model model; + CpModelProto new_cp_model; + PresolveContext context(&model, &new_cp_model, nullptr); + + ImportModelWithBasicPresolveIntoContext(initial_model, &context); + const CpModelProto expected_model = ParseTestProto(R"pb( + variables { domain: [ 10, 10 ] } + variables { domain: [ 10, 10 ] } + variables { domain: [ 10, 10 ] } + constraints { + interval { + start { offset: 10 } + end { offset: 20 } + size { offset: 10 } + } + } + )pb"); + EXPECT_THAT(new_cp_model, EqualsProto(expected_model)); +} + +TEST(ModelCopyTest, RemoveDuplicateFromClauses) { + const CpModelProto initial_model = ParseTestProto(R"pb( + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + constraints { + enforcement_literal: [ 1, 2, 3, 2 ] + bool_or { literals: [ -4, 9, 8 ] } + } + )pb"); + const CpModelProto expected_moded = ParseTestProto(R"pb( + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + constraints { bool_or { literals: [ -2, -3, -4, 9, 8 ] } } + )pb"); + CpModelProto new_cp_model; + Model model; + PresolveContext context(&model, &new_cp_model, nullptr); + ImportModelWithBasicPresolveIntoContext(initial_model, &context); + EXPECT_THAT(new_cp_model, EqualsProto(expected_moded)); +} + +TEST(ModelCopyTest, RemoveDuplicateFromEnforcementLiterals) { + const CpModelProto initial_model = ParseTestProto(R"pb( + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 100 ] } + variables { domain: [ 0, 100 ] } + variables { domain: [ 0, 100 ] } + constraints { + enforcement_literal: [ 1, 2, 3, 2 ] # duplicate + linear { + vars: [ 4, 5, 6 ] + coeffs: [ 1, 1, 1 ] + domain: [ 0, 100 ] + } + } + constraints { + enforcement_literal: [ 2, -3, 2 ] # can never be enforced. + linear { + vars: [ 4, 5, 6 ] + coeffs: [ 2, 1, 3 ] + domain: [ 0, 100 ] + } + } + )pb"); + const CpModelProto expected_moded = ParseTestProto(R"pb( + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 100 ] } + variables { domain: [ 0, 100 ] } + variables { domain: [ 0, 100 ] } + constraints { + enforcement_literal: [ 1, 2, 3 ] + linear { + vars: [ 4, 5, 6 ] + coeffs: [ 1, 1, 1 ] + domain: [ 0, 100 ] + } + } + )pb"); + CpModelProto new_cp_model; + Model model; + model.GetOrCreate() + ->set_keep_all_feasible_solutions_in_presolve(true); + PresolveContext context(&model, &new_cp_model, nullptr); + ImportModelWithBasicPresolveIntoContext(initial_model, &context); + EXPECT_THAT(new_cp_model, EqualsProto(expected_moded)); +} + +} // namespace +} // namespace sat +} // namespace operations_research diff --git a/ortools/sat/cp_model_expand_test.cc b/ortools/sat/cp_model_expand_test.cc index 1ed3d4a668..aee22c75fb 100644 --- a/ortools/sat/cp_model_expand_test.cc +++ b/ortools/sat/cp_model_expand_test.cc @@ -2017,7 +2017,7 @@ TEST(FinalExpansionForLinearConstraintTest, ComplexLinearExpansion) { EXPECT_THAT(initial_model, testing::EqualsProto(expected_model)); // We should properly complete the hint and choose the bucket [4, 6]. - EXPECT_THAT(context.solution_crush().SolutionHint(), + EXPECT_THAT(context.solution_crush().GetVarValues(), ::testing::ElementsAre(1, 5, 0, 1, 0)); EXPECT_TRUE(context.DebugTestHintFeasibility()); } @@ -2067,7 +2067,7 @@ TEST(FinalExpansionForLinearConstraintTest, ComplexLinearExpansionWithInteger) { EXPECT_THAT(initial_model, testing::EqualsProto(expected_model)); // We should properly complete the hint with the new slack variable. - EXPECT_THAT(context.solution_crush().SolutionHint(), + EXPECT_THAT(context.solution_crush().GetVarValues(), ::testing::ElementsAre(1, 5, 6)); EXPECT_TRUE(context.DebugTestHintFeasibility()); } @@ -2153,7 +2153,7 @@ TEST(FinalExpansionForLinearConstraintTest, // We should properly complete the hint and choose the bucket [4, 6], as well // as set the new linear_is_enforced hint to true. - EXPECT_THAT(context.solution_crush().SolutionHint(), + EXPECT_THAT(context.solution_crush().GetVarValues(), ::testing::ElementsAre(1, 5, 1, 0, 0, 1, 1)); EXPECT_TRUE(context.DebugTestHintFeasibility()); } diff --git a/ortools/sat/cp_model_lns.cc b/ortools/sat/cp_model_lns.cc index 01d2ad00a0..aa793c6681 100644 --- a/ortools/sat/cp_model_lns.cc +++ b/ortools/sat/cp_model_lns.cc @@ -43,8 +43,8 @@ #include "ortools/base/stl_util.h" #include "ortools/graph/connected_components.h" #include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_copy.h" #include "ortools/sat/cp_model_mapping.h" -#include "ortools/sat/cp_model_presolve.h" #include "ortools/sat/cp_model_solver_helpers.h" #include "ortools/sat/cp_model_utils.h" #include "ortools/sat/diffn_util.h" diff --git a/ortools/sat/cp_model_loader.cc b/ortools/sat/cp_model_loader.cc index 2b5b382711..9150902387 100644 --- a/ortools/sat/cp_model_loader.cc +++ b/ortools/sat/cp_model_loader.cc @@ -37,6 +37,7 @@ #include "ortools/base/strong_vector.h" #include "ortools/sat/all_different.h" #include "ortools/sat/circuit.h" +#include "ortools/sat/clause.h" #include "ortools/sat/cp_constraints.h" #include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_mapping.h" @@ -1034,8 +1035,12 @@ void LoadBoolAndConstraint(const ConstraintProto& ct, Model* m) { void LoadAtMostOneConstraint(const ConstraintProto& ct, Model* m) { auto* mapping = m->GetOrCreate(); + auto* implications = m->GetOrCreate(); CHECK(!HasEnforcementLiteral(ct)) << "Not supported."; - m->Add(AtMostOneConstraint(mapping->Literals(ct.at_most_one().literals()))); + if (!implications->AddAtMostOne( + mapping->Literals(ct.at_most_one().literals()))) { + m->GetOrCreate()->NotifyThatModelIsUnsat(); + } } void LoadExactlyOneConstraint(const ConstraintProto& ct, Model* m) { diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index 930d4f202b..4fe099bc5a 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/ortools/sat/cp_model_presolve.cc @@ -22,7 +22,6 @@ #include #include #include -#include #include #include #include @@ -47,7 +46,6 @@ #include "google/protobuf/arena.h" #include "google/protobuf/repeated_field.h" #include "google/protobuf/repeated_ptr_field.h" -#include "google/protobuf/text_format.h" #include "ortools/base/logging.h" #include "ortools/base/mathutil.h" #include "ortools/base/protobuf_util.h" @@ -183,7 +181,7 @@ bool CpModelPresolver::PresolveEnforcementLiteral(ConstraintProto* ct) { if (context_->VariableIsUniqueAndRemovable(literal)) { // We can simply set it to false and ignore the constraint in this case. context_->UpdateRuleStats("enforcement: literal not used"); - CHECK(context_->SetLiteralAndHintToFalse(literal)); + CHECK(context_->SetLiteralToFalse(literal)); return RemoveConstraint(ct); } @@ -196,7 +194,7 @@ bool CpModelPresolver::PresolveEnforcementLiteral(ConstraintProto* ct) { if (RefIsPositive(literal) == (obj_coeff > 0)) { // It is just more advantageous to set it to false! context_->UpdateRuleStats("enforcement: literal with unique direction"); - CHECK(context_->SetLiteralAndHintToFalse(literal)); + CHECK(context_->SetLiteralToFalse(literal)); return RemoveConstraint(ct); } } @@ -352,7 +350,7 @@ bool CpModelPresolver::PresolveBoolOr(ConstraintProto* ct) { // objective var usage by 1). if (context_->VariableIsUniqueAndRemovable(literal)) { context_->UpdateRuleStats("bool_or: singleton"); - if (!context_->SetLiteralAndHintToTrue(literal)) return true; + if (!context_->SetLiteralToTrue(literal)) return true; return RemoveConstraint(ct); } if (context_->tmp_literal_set.contains(NegatedRef(literal))) { @@ -454,7 +452,7 @@ bool CpModelPresolver::PresolveBoolAnd(ConstraintProto* ct) { changed = true; context_->UpdateRuleStats( "bool_and: setting unused literal in rhs to true"); - if (!context_->SetLiteralAndHintToTrue(literal)) return true; + if (!context_->SetLiteralToTrue(literal)) return true; continue; } @@ -1651,6 +1649,15 @@ bool CpModelPresolver::PresolveIntProd(ConstraintProto* ct) { // so we can choose a better representative. const LinearExpressionProto old_target = ct->int_prod().target(); if (!context_->IsFixed(old_target)) { + if (CapProd(constant_factor, std::max(context_->MaxOf(old_target), + -context_->MinOf(old_target))) >= + std::numeric_limits::max() / 2) { + // Re-add a new term with the constant factor. + ct->mutable_int_prod()->add_exprs()->set_offset(constant_factor); + context_->UpdateRuleStats( + "int_prod: overflow prevented creating a affine relation."); + return true; + } const int ref = old_target.vars(0); const int64_t coeff = old_target.coeffs(0); const int64_t offset = old_target.offset(); @@ -2298,8 +2305,8 @@ bool CpModelPresolver::RemoveSingletonInLinear(ConstraintProto* ct) { // Just fix everything. context_->UpdateRuleStats("independent linear: solved by DP"); for (int i = 0; i < num_vars; ++i) { - if (!context_->IntersectDomainWithAndUpdateHint( - ct->linear().vars(i), Domain(result.solution[i]))) { + if (!context_->IntersectDomainWith(ct->linear().vars(i), + Domain(result.solution[i]))) { return false; } } @@ -2323,8 +2330,8 @@ bool CpModelPresolver::RemoveSingletonInLinear(ConstraintProto* ct) { costs[i] > 0 ? domains[i].Min() : domains[i].Max(); const int64_t other_value = result.solution[i]; if (best_value == other_value) { - if (!context_->IntersectDomainWithAndUpdateHint( - ct->linear().vars(i), Domain(best_value))) { + if (!context_->IntersectDomainWith(ct->linear().vars(i), + Domain(best_value))) { return false; } continue; @@ -4586,6 +4593,11 @@ bool CpModelPresolver::PresolveLinearOnBooleans(ConstraintProto* ct) { if (ct->constraint_case() != ConstraintProto::kLinear) return false; if (context_->ModelIsUnsat()) return false; + // For special kind of constraint detection. + int64_t sum_of_coeffs = 0; + int num_positive = 0; + int num_negative = 0; + const LinearConstraintProto& arg = ct->linear(); const int num_vars = arg.vars_size(); int64_t min_coeff = std::numeric_limits::max(); @@ -4601,12 +4613,15 @@ bool CpModelPresolver::PresolveLinearOnBooleans(ConstraintProto* ct) { if (context_->MinOf(var) != 0) return false; if (context_->MaxOf(var) != 1) return false; + sum_of_coeffs += coeff; if (coeff > 0) { + ++num_positive; max_sum += coeff; min_coeff = std::min(min_coeff, coeff); max_coeff = std::max(max_coeff, coeff); } else { // We replace the Boolean ref, by a ref to its negation (1 - x). + ++num_negative; min_sum += coeff; min_coeff = std::min(min_coeff, -coeff); max_coeff = std::max(max_coeff, -coeff); @@ -4633,6 +4648,25 @@ bool CpModelPresolver::PresolveLinearOnBooleans(ConstraintProto* ct) { return RemoveConstraint(ct); } + // This discover cases like "A + B + C - 3*D = 0" + // where all Booleans must be equivalent! + // This happens a lot on woodlands09.mps for instance. + // + // TODO(user): generalize if enforced? + // TODO(user): generalize to other variant! Use DP to identify constraint with + // just one or two solutions? or a few solution with same variable values? + if (ct->enforcement_literal().empty() && sum_of_coeffs == 0 && + (num_negative == 1 || num_positive == 1) && rhs_domain.IsFixed() && + rhs_domain.FixedValue() == 0) { + // This forces either all variable at 1 or all at zero. + context_->UpdateRuleStats("linear: all equivalent!"); + for (int i = 1; i < num_vars; ++i) { + context_->StoreBooleanEqualityRelation(ct->linear().vars(0), + ct->linear().vars(i)); + } + return RemoveConstraint(ct); + } + // Detect clauses, reified ands, at_most_one. // // TODO(user): split a == 1 constraint or similar into a clause and an at @@ -7810,7 +7844,7 @@ bool CpModelPresolver::PresolvePureSatPart() { // Such variable needs to be fixed to some value for the SAT postsolve to // work. if (!context_->IsFixed(var)) { - CHECK(context_->IntersectDomainWithAndUpdateHint( + CHECK(context_->IntersectDomainWith( var, Domain(context_->DomainOf(var).SmallestValue()))); } context_->MarkVariableAsRemoved(var); @@ -9627,12 +9661,12 @@ void CpModelPresolver::DetectDuplicateConstraintsWithDifferentEnforcements( bool skip = false; if (RefIsPositive(a) == context_->ObjectiveCoeff(PositiveRef(a)) > 0) { context_->UpdateRuleStats("duplicate: dual fixing enforcement."); - if (!context_->SetLiteralAndHintToFalse(a)) return; + if (!context_->SetLiteralToFalse(a)) return; skip = true; } if (RefIsPositive(b) == context_->ObjectiveCoeff(PositiveRef(b)) > 0) { context_->UpdateRuleStats("duplicate: dual fixing enforcement."); - if (!context_->SetLiteralAndHintToFalse(b)) return; + if (!context_->SetLiteralToFalse(b)) return; skip = true; } if (skip) continue; @@ -11846,8 +11880,7 @@ void CpModelPresolver::ProcessVariableOnlyUsedInEncoding(int var) { int64_t value1, value2; if (cost == 0) { context_->UpdateRuleStats("variables: fix singleton var in linear1"); - return (void)context_->IntersectDomainWithAndUpdateHint( - var, Domain(implied.Min())); + return (void)context_->IntersectDomainWith(var, Domain(implied.Min())); } else if (cost > 0) { value1 = context_->MinOf(var); value2 = implied.Min(); @@ -12523,935 +12556,6 @@ void CpModelPresolver::PresolveToFixPoint() { context_->deductions.MarkProcessingAsDoneForNow(); } -ModelCopy::ModelCopy(PresolveContext* context) : context_(context) {} - -void ModelCopy::ImportVariablesAndMaybeIgnoreNames( - const CpModelProto& in_model) { - if (context_->params().ignore_names()) { - context_->working_model->clear_variables(); - context_->working_model->mutable_variables()->Reserve( - in_model.variables_size()); - for (const IntegerVariableProto& var_proto : in_model.variables()) { - *context_->working_model->add_variables()->mutable_domain() = - var_proto.domain(); - } - } else { - *context_->working_model->mutable_variables() = in_model.variables(); - } -} - -void ModelCopy::CreateVariablesFromDomains(absl::Span domains) { - for (const Domain& domain : domains) { - FillDomainInProto(domain, context_->working_model->add_variables()); - } -} - -// TODO(user): Merge with the phase 1 of the presolve code. -// -// TODO(user): It seems easy to forget to update this if any new constraint -// contains an interval or if we add a field to an existing constraint. Find a -// way to remind contributor to not forget this. -bool ModelCopy::ImportAndSimplifyConstraints( - const CpModelProto& in_model, bool first_copy, - std::function active_constraints) { - context_->InitializeNewDomains(); - if (context_->ModelIsUnsat()) return false; - const bool ignore_names = context_->params().ignore_names(); - - // If first_copy is true, we reorder the scheduling constraint to be sure they - // refer to interval before them. - std::vector constraints_using_intervals; - - interval_mapping_.assign(in_model.constraints().size(), -1); - - starting_constraint_index_ = context_->working_model->constraints_size(); - for (int c = 0; c < in_model.constraints_size(); ++c) { - if (active_constraints != nullptr && !active_constraints(c)) continue; - const ConstraintProto& ct = in_model.constraints(c); - if (first_copy) { - if (!PrepareEnforcementCopyWithDup(ct)) continue; - } else { - if (!PrepareEnforcementCopy(ct)) continue; - } - - // TODO(user): if ignore_names is false, we should make sure the - // name are properly copied by all these functions. Or we should never copy - // name and have a separate if (!ignore_name) copy the name... - switch (ct.constraint_case()) { - case ConstraintProto::CONSTRAINT_NOT_SET: - break; - case ConstraintProto::kBoolOr: - if (first_copy) { - if (!CopyBoolOrWithDupSupport(ct)) return CreateUnsatModel(c, ct); - } else { - if (!CopyBoolOr(ct)) return CreateUnsatModel(c, ct); - } - break; - case ConstraintProto::kBoolAnd: - if (temp_enforcement_literals_.empty()) { - for (const int lit : ct.bool_and().literals()) { - context_->UpdateRuleStats("bool_and: non-reified."); - if (!context_->SetLiteralToTrue(lit)) { - return CreateUnsatModel(c, ct); - } - } - } else if (first_copy) { - if (!CopyBoolAndWithDupSupport(ct)) return CreateUnsatModel(c, ct); - } else { - if (!CopyBoolAnd(ct)) return CreateUnsatModel(c, ct); - } - break; - case ConstraintProto::kLinear: - if (!CopyLinear(ct)) return CreateUnsatModel(c, ct); - break; - case ConstraintProto::kIntProd: - if (!CopyIntProd(ct, ignore_names)) return CreateUnsatModel(c, ct); - break; - case ConstraintProto::kIntDiv: - if (!CopyIntDiv(ct, ignore_names)) return CreateUnsatModel(c, ct); - break; - case ConstraintProto::kIntMod: - if (!CopyIntMod(ct, ignore_names)) return CreateUnsatModel(c, ct); - break; - case ConstraintProto::kElement: - if (!CopyElement(ct)) return CreateUnsatModel(c, ct); - break; - case ConstraintProto::kTable: - if (!CopyTable(ct)) return CreateUnsatModel(c, ct); - break; - case ConstraintProto::kAutomaton: - if (!CopyAutomaton(ct)) return CreateUnsatModel(c, ct); - break; - case ConstraintProto::kAllDiff: - if (!CopyAllDiff(ct)) return CreateUnsatModel(c, ct); - break; - case ConstraintProto::kLinMax: - if (!CopyLinMax(ct)) return CreateUnsatModel(c, ct); - break; - case ConstraintProto::kAtMostOne: - if (!CopyAtMostOne(ct)) return CreateUnsatModel(c, ct); - break; - case ConstraintProto::kExactlyOne: - if (!CopyExactlyOne(ct)) return CreateUnsatModel(c, ct); - break; - case ConstraintProto::kInterval: - if (!CopyInterval(ct, c, ignore_names)) return CreateUnsatModel(c, ct); - if (first_copy) { - if (!AddLinearConstraintForInterval(ct)) - return CreateUnsatModel(c, ct); - } - break; - case ConstraintProto::kNoOverlap: - if (first_copy) { - constraints_using_intervals.push_back(c); - } else { - CopyAndMapNoOverlap(ct); - } - break; - case ConstraintProto::kNoOverlap2D: - if (first_copy) { - constraints_using_intervals.push_back(c); - } else { - CopyAndMapNoOverlap2D(ct); - } - break; - case ConstraintProto::kCumulative: - if (first_copy) { - constraints_using_intervals.push_back(c); - } else { - if (!CopyAndMapCumulative(ct)) return CreateUnsatModel(c, ct); - } - break; - default: { - ConstraintProto* new_ct = context_->working_model->add_constraints(); - *new_ct = ct; - new_ct->mutable_enforcement_literal()->Clear(); - FinishEnforcementCopy(new_ct); - if (ignore_names) { - // TODO(user): find a better way than copy then clear_name()? - new_ct->clear_name(); - } - } - } - } - - // This should be empty if first_copy is false. - DCHECK(first_copy || constraints_using_intervals.empty()); - for (const int c : constraints_using_intervals) { - const ConstraintProto& ct = in_model.constraints(c); - switch (ct.constraint_case()) { - case ConstraintProto::kNoOverlap: - CopyAndMapNoOverlap(ct); - break; - case ConstraintProto::kNoOverlap2D: - CopyAndMapNoOverlap2D(ct); - break; - case ConstraintProto::kCumulative: - if (!CopyAndMapCumulative(ct)) return CreateUnsatModel(c, ct); - break; - default: - LOG(DFATAL) << "Shouldn't be here."; - } - } - - return true; -} - -bool ModelCopy::PrepareEnforcementCopy(const ConstraintProto& ct) { - temp_enforcement_literals_.clear(); - for (const int lit : ct.enforcement_literal()) { - if (context_->LiteralIsTrue(lit)) continue; - if (context_->LiteralIsFalse(lit)) { - context_->UpdateRuleStats("enforcement: always false"); - return false; - } - temp_enforcement_literals_.push_back(lit); - } - return true; // Continue processing. -} - -bool ModelCopy::PrepareEnforcementCopyWithDup(const ConstraintProto& ct) { - temp_enforcement_literals_.clear(); - temp_enforcement_literals_set_.clear(); - for (const int lit : ct.enforcement_literal()) { - if (context_->LiteralIsTrue(lit)) continue; - if (temp_enforcement_literals_set_.contains(lit)) { - context_->UpdateRuleStats("enforcement: removed duplicate literal"); - continue; - } - - // Cannot be satisfied. - if (context_->LiteralIsFalse(lit)) { - context_->UpdateRuleStats("enforcement: always false"); - return false; - } - if (temp_enforcement_literals_set_.contains(NegatedRef(lit))) { - context_->UpdateRuleStats("enforcement: contains x and not(x)"); - return false; - } - - temp_enforcement_literals_.push_back(lit); - temp_enforcement_literals_set_.insert(lit); - } - return true; // Continue processing. -} - -void ModelCopy::FinishEnforcementCopy(ConstraintProto* ct) { - ct->mutable_enforcement_literal()->Add(temp_enforcement_literals_.begin(), - temp_enforcement_literals_.end()); -} - -bool ModelCopy::FinishBoolOrCopy() { - if (temp_literals_.empty()) return false; - - if (temp_literals_.size() == 1) { - context_->UpdateRuleStats("bool_or: only one literal"); - return context_->SetLiteralToTrue(temp_literals_[0]); - } - - context_->working_model->add_constraints() - ->mutable_bool_or() - ->mutable_literals() - ->Add(temp_literals_.begin(), temp_literals_.end()); - return true; -} - -bool ModelCopy::CopyBoolOr(const ConstraintProto& ct) { - temp_literals_.clear(); - for (const int lit : temp_enforcement_literals_) { - temp_literals_.push_back(NegatedRef(lit)); - } - for (const int lit : ct.bool_or().literals()) { - if (context_->LiteralIsTrue(lit)) { - return true; - } - if (!context_->LiteralIsFalse(lit)) { - temp_literals_.push_back(lit); - } - } - return FinishBoolOrCopy(); -} - -bool ModelCopy::CopyBoolOrWithDupSupport(const ConstraintProto& ct) { - temp_literals_.clear(); - temp_literals_set_.clear(); - for (const int enforcement_lit : temp_enforcement_literals_) { - // Having an enforcement literal is the same as having its negation on - // the clause. - const int lit = NegatedRef(enforcement_lit); - - // Note that we already dealt with duplicate since we should have called - // PrepareEnforcementCopyWithDup() in this case. - temp_literals_set_.insert(lit); - temp_literals_.push_back(lit); - } - for (const int lit : ct.bool_or().literals()) { - if (context_->LiteralIsTrue(lit)) { - context_->UpdateRuleStats("bool_or: always true"); - return true; - } - if (context_->LiteralIsFalse(lit)) continue; - if (temp_literals_set_.contains(NegatedRef(lit))) { - context_->UpdateRuleStats("bool_or: always true"); - return true; - } - const auto [it, inserted] = temp_literals_set_.insert(lit); - if (inserted) temp_literals_.push_back(lit); - } - return FinishBoolOrCopy(); -} - -bool ModelCopy::CopyBoolAnd(const ConstraintProto& ct) { - bool at_least_one_false = false; - int num_non_fixed_literals = 0; - for (const int lit : ct.bool_and().literals()) { - if (context_->LiteralIsFalse(lit)) { - at_least_one_false = true; - break; - } - if (!context_->LiteralIsTrue(lit)) { - num_non_fixed_literals++; - } - } - - if (at_least_one_false) { - // One enforcement literal must be false. - BoolArgumentProto* bool_or = - context_->working_model->add_constraints()->mutable_bool_or(); - for (const int lit : temp_enforcement_literals_) { - bool_or->add_literals(NegatedRef(lit)); - } - return !bool_or->literals().empty(); - } else if (num_non_fixed_literals > 0) { - ConstraintProto* new_ct = context_->working_model->add_constraints(); - FinishEnforcementCopy(new_ct); - BoolArgumentProto* bool_and = new_ct->mutable_bool_and(); - bool_and->mutable_literals()->Reserve(num_non_fixed_literals); - for (const int lit : ct.bool_and().literals()) { - if (context_->LiteralIsTrue(lit)) continue; - bool_and->add_literals(lit); - } - } - return true; -} - -bool ModelCopy::CopyBoolAndWithDupSupport(const ConstraintProto& ct) { - DCHECK(!temp_enforcement_literals_.empty()); - - bool at_least_one_false = false; - temp_literals_.clear(); - temp_literals_set_.clear(); - for (const int lit : ct.bool_and().literals()) { - if (context_->LiteralIsFalse(lit)) { - context_->UpdateRuleStats("bool and: always false"); - at_least_one_false = true; - break; - } - if (temp_literals_set_.contains(NegatedRef(lit))) { - context_->UpdateRuleStats("bool and: => x and not(x) "); - at_least_one_false = true; - break; - } - if (temp_enforcement_literals_set_.contains(NegatedRef(lit))) { - context_->UpdateRuleStats("bool and: not(x) => x"); - at_least_one_false = true; - break; - } - - if (context_->LiteralIsTrue(lit)) continue; - if (temp_enforcement_literals_set_.contains(lit)) { - context_->UpdateRuleStats("bool and: x => x"); - continue; - } - const auto [it, inserted] = temp_literals_set_.insert(lit); - if (inserted) temp_literals_.push_back(lit); - } - - if (at_least_one_false) { - // One enforcement literal must be false. - BoolArgumentProto* bool_or = - context_->working_model->add_constraints()->mutable_bool_or(); - for (const int lit : temp_enforcement_literals_) { - bool_or->add_literals(NegatedRef(lit)); - } - return !bool_or->literals().empty(); - } - - if (temp_literals_.empty()) { - context_->UpdateRuleStats("bool and: empty"); - return true; - } - - // Copy. - ConstraintProto* new_ct = context_->working_model->add_constraints(); - FinishEnforcementCopy(new_ct); - new_ct->mutable_bool_and()->mutable_literals()->Add(temp_literals_.begin(), - temp_literals_.end()); - return true; -} - -bool ModelCopy::CopyLinearExpression(const LinearExpressionProto& expr, - LinearExpressionProto* dst) { - non_fixed_variables_.clear(); - non_fixed_coefficients_.clear(); - int64_t offset = expr.offset(); - for (int i = 0; i < expr.vars_size(); ++i) { - const int ref = expr.vars(i); - const int64_t coeff = expr.coeffs(i); - if (coeff == 0) continue; - if (context_->IsFixed(ref)) { - offset += coeff * context_->MinOf(ref); - continue; - } - - // Make sure we never have negative ref in a linear constraint. - if (RefIsPositive(ref)) { - non_fixed_variables_.push_back(ref); - non_fixed_coefficients_.push_back(coeff); - } else { - non_fixed_variables_.push_back(NegatedRef(ref)); - non_fixed_coefficients_.push_back(-coeff); - } - } - - dst->set_offset(offset); - dst->mutable_vars()->Add(non_fixed_variables_.begin(), - non_fixed_variables_.end()); - dst->mutable_coeffs()->Add(non_fixed_coefficients_.begin(), - non_fixed_coefficients_.end()); - return true; -} - -bool ModelCopy::CopyLinear(const ConstraintProto& ct) { - non_fixed_variables_.clear(); - non_fixed_coefficients_.clear(); - int64_t offset = 0; - int64_t min_activity = 0; - int64_t max_activity = 0; - for (int i = 0; i < ct.linear().vars_size(); ++i) { - const int ref = ct.linear().vars(i); - const int64_t coeff = ct.linear().coeffs(i); - if (coeff == 0) continue; - if (context_->IsFixed(ref)) { - offset += coeff * context_->MinOf(ref); - continue; - } - - if (coeff > 0) { - min_activity += coeff * context_->MinOf(ref); - max_activity += coeff * context_->MaxOf(ref); - } else { - min_activity += coeff * context_->MaxOf(ref); - max_activity += coeff * context_->MinOf(ref); - } - - // Make sure we never have negative ref in a linear constraint. - if (RefIsPositive(ref)) { - non_fixed_variables_.push_back(ref); - non_fixed_coefficients_.push_back(coeff); - } else { - non_fixed_variables_.push_back(NegatedRef(ref)); - non_fixed_coefficients_.push_back(-coeff); - } - } - - const Domain implied(min_activity, max_activity); - const Domain new_rhs = - ReadDomainFromProto(ct.linear()).AdditionWith(Domain(-offset)); - - // Trivial constraint? - if (implied.IsIncludedIn(new_rhs)) { - context_->UpdateRuleStats("linear: always true"); - return true; - } - - // Constraint is false? - const Domain tight_domain = implied.IntersectionWith(new_rhs); - if (tight_domain.IsEmpty()) { - if (ct.enforcement_literal().empty()) return false; - temp_literals_.clear(); - for (const int literal : ct.enforcement_literal()) { - if (!context_->LiteralIsTrue(literal)) { - temp_literals_.push_back(NegatedRef(literal)); - } - } - context_->working_model->add_constraints() - ->mutable_bool_or() - ->mutable_literals() - ->Add(temp_literals_.begin(), temp_literals_.end()); - return !temp_literals_.empty(); - } - - DCHECK(!non_fixed_variables_.empty()); - - if (non_fixed_variables_.size() == 1 && ct.enforcement_literal().empty()) { - context_->UpdateRuleStats("linear1: x in domain"); - return context_->IntersectDomainWith( - non_fixed_variables_[0], - new_rhs.InverseMultiplicationBy(non_fixed_coefficients_[0])); - } - - ConstraintProto* new_ct = context_->working_model->add_constraints(); - FinishEnforcementCopy(new_ct); - LinearConstraintProto* linear = new_ct->mutable_linear(); - linear->mutable_vars()->Add(non_fixed_variables_.begin(), - non_fixed_variables_.end()); - linear->mutable_coeffs()->Add(non_fixed_coefficients_.begin(), - non_fixed_coefficients_.end()); - FillDomainInProto(tight_domain, linear); - return true; -} - -bool ModelCopy::CopyElement(const ConstraintProto& ct) { - ConstraintProto* new_ct = context_->working_model->add_constraints(); - if (ct.element().vars().empty() && !ct.element().exprs().empty()) { - // New format, just copy. - *new_ct = ct; - return true; - } - - auto fill_expr = [this](int var, LinearExpressionProto* expr) mutable { - if (context_->IsFixed(var)) { - expr->set_offset(context_->FixedValue(var)); - } else { - DCHECK(RefIsPositive(var)); - expr->mutable_vars()->Reserve(1); - expr->mutable_coeffs()->Reserve(1); - expr->add_vars(var); - expr->add_coeffs(1); - } - }; - - fill_expr(ct.element().index(), - new_ct->mutable_element()->mutable_linear_index()); - fill_expr(ct.element().target(), - new_ct->mutable_element()->mutable_linear_target()); - for (const int var : ct.element().vars()) { - fill_expr(var, new_ct->mutable_element()->add_exprs()); - } - return true; -} - -bool ModelCopy::CopyAutomaton(const ConstraintProto& ct) { - ConstraintProto* new_ct = context_->working_model->add_constraints(); - *new_ct = ct; - if (new_ct->automaton().vars().empty()) return true; - - auto fill_expr = [this](int var, LinearExpressionProto* expr) mutable { - if (context_->IsFixed(var)) { - expr->set_offset(context_->FixedValue(var)); - } else { - DCHECK(RefIsPositive(var)); - expr->mutable_vars()->Reserve(1); - expr->mutable_coeffs()->Reserve(1); - expr->add_vars(var); - expr->add_coeffs(1); - } - }; - - for (const int var : ct.automaton().vars()) { - fill_expr(var, new_ct->mutable_automaton()->add_exprs()); - } - new_ct->mutable_automaton()->clear_vars(); - - return true; -} - -bool ModelCopy::CopyTable(const ConstraintProto& ct) { - ConstraintProto* new_ct = context_->working_model->add_constraints(); - if (ct.table().vars().empty() && !ct.table().exprs().empty()) { - // New format, just copy. - *new_ct = ct; - return true; - } - - auto fill_expr = [this](int var, LinearExpressionProto* expr) mutable { - if (context_->IsFixed(var)) { - expr->set_offset(context_->FixedValue(var)); - } else { - DCHECK(RefIsPositive(var)); - expr->mutable_vars()->Reserve(1); - expr->mutable_coeffs()->Reserve(1); - expr->add_vars(var); - expr->add_coeffs(1); - } - }; - - for (const int var : ct.table().vars()) { - fill_expr(var, new_ct->mutable_table()->add_exprs()); - } - *new_ct->mutable_table()->mutable_values() = ct.table().values(); - new_ct->mutable_table()->set_negated(ct.table().negated()); - *new_ct->mutable_enforcement_literal() = ct.enforcement_literal(); - - return true; -} - -bool ModelCopy::CopyAllDiff(const ConstraintProto& ct) { - if (ct.all_diff().exprs().size() <= 1) return true; - ConstraintProto* new_ct = context_->working_model->add_constraints(); - for (const LinearExpressionProto& expr : ct.all_diff().exprs()) { - CopyLinearExpression(expr, new_ct->mutable_all_diff()->add_exprs()); - } - return true; -} - -bool ModelCopy::CopyLinMax(const ConstraintProto& ct) { - // We will create it lazily if we end up copying something. - ConstraintProto* new_ct = nullptr; - - // Regroup all constant terms and copy the other. - int64_t max_of_fixed_terms = std::numeric_limits::min(); - for (const auto& expr : ct.lin_max().exprs()) { - const std::optional fixed = context_->FixedValueOrNullopt(expr); - if (fixed != std::nullopt) { - max_of_fixed_terms = std::max(max_of_fixed_terms, fixed.value()); - } else { - // copy. - if (new_ct == nullptr) { - new_ct = context_->working_model->add_constraints(); - } - CopyLinearExpression(expr, new_ct->mutable_lin_max()->add_exprs()); - } - } - - // If we have no non-fixed expression, we can just fix the target when it - // involve at most one variable. - if (new_ct == nullptr && ct.enforcement_literal().empty() && - ct.lin_max().target().vars().size() <= 1) { - context_->UpdateRuleStats("lin_max: all exprs fixed during copy"); - return context_->IntersectDomainWith(ct.lin_max().target(), - Domain(max_of_fixed_terms)); - } - - // Otherwise, add a constant term if needed. - if (max_of_fixed_terms > std::numeric_limits::min()) { - if (new_ct == nullptr) { - new_ct = context_->working_model->add_constraints(); - } - new_ct->mutable_lin_max()->add_exprs()->set_offset(max_of_fixed_terms); - } - - // Finish by copying the target. - if (new_ct == nullptr) return false; // No expr == unsat. - CopyLinearExpression(ct.lin_max().target(), - new_ct->mutable_lin_max()->mutable_target()); - return true; -} - -bool ModelCopy::CopyAtMostOne(const ConstraintProto& ct) { - int num_true = 0; - temp_literals_.clear(); - for (const int lit : ct.at_most_one().literals()) { - if (context_->LiteralIsFalse(lit)) continue; - temp_literals_.push_back(lit); - if (context_->LiteralIsTrue(lit)) num_true++; - } - - if (temp_literals_.size() <= 1) return true; - if (num_true > 1) return false; - - // TODO(user): presolve if num_true == 1. - ConstraintProto* new_ct = context_->working_model->add_constraints(); - FinishEnforcementCopy(new_ct); - new_ct->mutable_at_most_one()->mutable_literals()->Add(temp_literals_.begin(), - temp_literals_.end()); - return true; -} - -bool ModelCopy::CopyExactlyOne(const ConstraintProto& ct) { - int num_true = 0; - temp_literals_.clear(); - for (const int lit : ct.exactly_one().literals()) { - if (context_->LiteralIsFalse(lit)) continue; - temp_literals_.push_back(lit); - if (context_->LiteralIsTrue(lit)) num_true++; - } - - if (temp_literals_.empty() || num_true > 1) return false; - if (temp_literals_.size() == 1 && num_true == 1) return true; - - // TODO(user): presolve if num_true == 1 and not everything is false. - ConstraintProto* new_ct = context_->working_model->add_constraints(); - FinishEnforcementCopy(new_ct); - new_ct->mutable_exactly_one()->mutable_literals()->Add(temp_literals_.begin(), - temp_literals_.end()); - return true; -} - -bool ModelCopy::CopyInterval(const ConstraintProto& ct, int c, - bool ignore_names) { - CHECK_EQ(starting_constraint_index_, 0) - << "Adding new interval constraints to partially filled model is not " - "supported."; - interval_mapping_[c] = context_->working_model->constraints_size(); - ConstraintProto* new_ct = context_->working_model->add_constraints(); - if (!ignore_names) { - new_ct->set_name(ct.name()); - } - *new_ct->mutable_enforcement_literal() = ct.enforcement_literal(); - CopyLinearExpression(ct.interval().start(), - new_ct->mutable_interval()->mutable_start()); - CopyLinearExpression(ct.interval().size(), - new_ct->mutable_interval()->mutable_size()); - CopyLinearExpression(ct.interval().end(), - new_ct->mutable_interval()->mutable_end()); - return true; -} - -bool ModelCopy::CopyIntProd(const ConstraintProto& ct, bool ignore_names) { - ConstraintProto* new_ct = context_->working_model->add_constraints(); - if (!ignore_names) { - new_ct->set_name(ct.name()); - } - for (const LinearExpressionProto& expr : ct.int_prod().exprs()) { - CopyLinearExpression(expr, new_ct->mutable_int_prod()->add_exprs()); - } - CopyLinearExpression(ct.int_prod().target(), - new_ct->mutable_int_prod()->mutable_target()); - return true; -} - -bool ModelCopy::CopyIntDiv(const ConstraintProto& ct, bool ignore_names) { - ConstraintProto* new_ct = context_->working_model->add_constraints(); - if (!ignore_names) { - new_ct->set_name(ct.name()); - } - for (const LinearExpressionProto& expr : ct.int_div().exprs()) { - CopyLinearExpression(expr, new_ct->mutable_int_div()->add_exprs()); - } - CopyLinearExpression(ct.int_div().target(), - new_ct->mutable_int_div()->mutable_target()); - return true; -} - -bool ModelCopy::CopyIntMod(const ConstraintProto& ct, bool ignore_names) { - ConstraintProto* new_ct = context_->working_model->add_constraints(); - if (!ignore_names) { - new_ct->set_name(ct.name()); - } - for (const LinearExpressionProto& expr : ct.int_mod().exprs()) { - CopyLinearExpression(expr, new_ct->mutable_int_mod()->add_exprs()); - } - CopyLinearExpression(ct.int_mod().target(), - new_ct->mutable_int_mod()->mutable_target()); - return true; -} - -bool ModelCopy::AddLinearConstraintForInterval(const ConstraintProto& ct) { - // Add the linear constraint enforcement => (start + size == end). - // - // We rely on the presolve for simplification, but deal with the trivial - // case of (start, offset, start + offset) here. - const IntervalConstraintProto& itv = ct.interval(); - if (itv.size().vars().empty() && - itv.start().offset() + itv.size().offset() == itv.end().offset() && - absl::Span(itv.start().vars()) == - absl::Span(itv.end().vars()) && - absl::Span(itv.start().coeffs()) == - absl::Span(itv.end().coeffs())) { - // Trivial constraint, nothing to do. - } else { - tmp_constraint_.Clear(); - *tmp_constraint_.mutable_enforcement_literal() = ct.enforcement_literal(); - LinearConstraintProto* mutable_linear = tmp_constraint_.mutable_linear(); - - mutable_linear->add_domain(0); - mutable_linear->add_domain(0); - AddLinearExpressionToLinearConstraint(itv.start(), 1, mutable_linear); - AddLinearExpressionToLinearConstraint(itv.size(), 1, mutable_linear); - AddLinearExpressionToLinearConstraint(itv.end(), -1, mutable_linear); - if (!CopyLinear(tmp_constraint_)) return false; - } - - // An enforced interval must have is size non-negative. - const LinearExpressionProto& size_expr = itv.size(); - if (context_->MinOf(size_expr) < 0) { - tmp_constraint_.Clear(); - *tmp_constraint_.mutable_enforcement_literal() = ct.enforcement_literal(); - *tmp_constraint_.mutable_linear()->mutable_vars() = size_expr.vars(); - *tmp_constraint_.mutable_linear()->mutable_coeffs() = size_expr.coeffs(); - tmp_constraint_.mutable_linear()->add_domain(-size_expr.offset()); - tmp_constraint_.mutable_linear()->add_domain( - std::numeric_limits::max()); - if (!CopyLinear(tmp_constraint_)) return false; - } - - return true; -} - -void ModelCopy::CopyAndMapNoOverlap(const ConstraintProto& ct) { - // Note that we don't copy names or enforcement_literal (not supported) here. - auto* new_ct = - context_->working_model->add_constraints()->mutable_no_overlap(); - new_ct->mutable_intervals()->Reserve(ct.no_overlap().intervals().size()); - for (const int index : ct.no_overlap().intervals()) { - const int new_index = interval_mapping_[index]; - if (new_index != -1) { - new_ct->add_intervals(new_index); - } - } -} - -void ModelCopy::CopyAndMapNoOverlap2D(const ConstraintProto& ct) { - // Note that we don't copy names or enforcement_literal (not supported) here. - auto* new_ct = - context_->working_model->add_constraints()->mutable_no_overlap_2d(); - - const int num_intervals = ct.no_overlap_2d().x_intervals().size(); - new_ct->mutable_x_intervals()->Reserve(num_intervals); - new_ct->mutable_y_intervals()->Reserve(num_intervals); - for (int i = 0; i < num_intervals; ++i) { - const int new_x = interval_mapping_[ct.no_overlap_2d().x_intervals(i)]; - if (new_x == -1) continue; - const int new_y = interval_mapping_[ct.no_overlap_2d().y_intervals(i)]; - if (new_y == -1) continue; - new_ct->add_x_intervals(new_x); - new_ct->add_y_intervals(new_y); - } -} - -bool ModelCopy::CopyAndMapCumulative(const ConstraintProto& ct) { - if (ct.cumulative().intervals().empty() && - context_->IsFixed(ct.cumulative().capacity())) { - // Trivial constraint, either obviously SAT or UNSAT. - return context_->FixedValue(ct.cumulative().capacity()) >= 0; - } - // Note that we don't copy names or enforcement_literal (not supported) here. - auto* new_ct = - context_->working_model->add_constraints()->mutable_cumulative(); - CopyLinearExpression(ct.cumulative().capacity(), new_ct->mutable_capacity()); - - const int num_intervals = ct.cumulative().intervals().size(); - new_ct->mutable_intervals()->Reserve(num_intervals); - new_ct->mutable_demands()->Reserve(num_intervals); - for (int i = 0; i < num_intervals; ++i) { - const int new_index = interval_mapping_[ct.cumulative().intervals(i)]; - if (new_index != -1) { - new_ct->add_intervals(new_index); - *new_ct->add_demands() = ct.cumulative().demands(i); - } - } - - return true; -} - -bool ModelCopy::CreateUnsatModel(int c, const ConstraintProto& ct) { - context_->working_model->mutable_constraints()->Clear(); - context_->working_model->add_constraints()->mutable_bool_or(); - - // If the model was already marked as unsat, we keep the old message and just - // return. TODO(user): Append messages instead? - if (context_->ModelIsUnsat()) return false; - - std::string proto_string; -#if !defined(__PORTABLE_PLATFORM__) - google::protobuf::TextFormat::Printer printer; - SetupTextFormatPrinter(&printer); - printer.PrintToString(ct, &proto_string); -#endif // !defined(__PORTABLE_PLATFORM__) - std::string message = absl::StrCat( - "proven during initial copy of constraint #", c, ":\n", proto_string); - std::vector vars = UsedVariables(ct); - if (vars.size() < 10) { - absl::StrAppend(&message, "With current variable domains:\n"); - for (const int var : vars) { - absl::StrAppend(&message, "var:", var, - " domain:", context_->DomainOf(var).ToString(), "\n"); - } - } - return context_->NotifyThatModelIsUnsat(message); -} - -bool ImportModelWithBasicPresolveIntoContext(const CpModelProto& in_model, - PresolveContext* context) { - ModelCopy copier(context); - copier.ImportVariablesAndMaybeIgnoreNames(in_model); - if (copier.ImportAndSimplifyConstraints(in_model, /*first_copy=*/true)) { - CopyEverythingExceptVariablesAndConstraintsFieldsIntoContext(in_model, - context); - return true; - } - return !context->ModelIsUnsat(); -} - -bool ImportModelAndDomainsWithBasicPresolveIntoContext( - const CpModelProto& in_model, absl::Span domains, - std::function active_constraints, PresolveContext* context) { - CHECK_EQ(domains.size(), in_model.variables_size()); - ModelCopy copier(context); - copier.CreateVariablesFromDomains(domains); - if (copier.ImportAndSimplifyConstraints(in_model, /*first_copy=*/false, - active_constraints)) { - CopyEverythingExceptVariablesAndConstraintsFieldsIntoContext(in_model, - context); - return true; - } - return !context->ModelIsUnsat(); -} - -void CopyEverythingExceptVariablesAndConstraintsFieldsIntoContext( - const CpModelProto& in_model, PresolveContext* context) { - if (!in_model.name().empty()) { - context->working_model->set_name(in_model.name()); - } - if (in_model.has_objective()) { - *context->working_model->mutable_objective() = in_model.objective(); - } - if (in_model.has_floating_point_objective()) { - *context->working_model->mutable_floating_point_objective() = - in_model.floating_point_objective(); - } - if (!in_model.search_strategy().empty()) { - // We make sure we do not use the old variables field. - *context->working_model->mutable_search_strategy() = - in_model.search_strategy(); - for (DecisionStrategyProto& strategy : - *context->working_model->mutable_search_strategy()) { - google::protobuf::util::RemoveIf(strategy.mutable_exprs(), - [](const LinearExpressionProto* expr) { - return expr->vars().empty(); - }); - if (!strategy.variables().empty()) { - CHECK(strategy.exprs().empty()); - for (const int ref : strategy.variables()) { - LinearExpressionProto* expr = strategy.add_exprs(); - expr->add_vars(PositiveRef(ref)); - expr->add_coeffs(RefIsPositive(ref) ? 1 : -1); - } - strategy.clear_variables(); - } - } - } - if (!in_model.assumptions().empty()) { - *context->working_model->mutable_assumptions() = in_model.assumptions(); - } - if (in_model.has_symmetry()) { - *context->working_model->mutable_symmetry() = in_model.symmetry(); - } - if (in_model.has_solution_hint()) { - *context->working_model->mutable_solution_hint() = in_model.solution_hint(); - - // We make sure the hint is within the variables domain. - // - // This allows to avoid overflow because we know evaluating constraints on - // the variables domains should be safe thanks to the initial validation. - const int num_terms = in_model.solution_hint().vars().size(); - for (int i = 0; i < num_terms; ++i) { - const int var = in_model.solution_hint().vars(i); - const int64_t value = in_model.solution_hint().values(i); - const Domain& domain = ReadDomainFromProto(in_model.variables(var)); - if (domain.IsEmpty()) continue; // UNSAT. - const int64_t closest_domain_value = domain.ClosestValue(value); - if (closest_domain_value != value) { - context->UpdateRuleStats("hint: moved var hint within its domain."); - context->working_model->mutable_solution_hint()->set_values( - i, closest_domain_value); - } - } - } -} - // TODO(user): Use better heuristic? // // TODO(user): This is similar to what Bounded variable addition (BVA) does. @@ -13722,47 +12826,29 @@ void CpModelPresolver::ExpandCpModelAndCanonicalizeConstraints() { namespace { +// Updates the solution hint in the proto with the crushed solution values. void UpdateHintInProto(PresolveContext* context) { CpModelProto* proto = context->working_model; if (!proto->has_solution_hint()) return; if (context->ModelIsUnsat()) return; - // Extract the new hint information from the context. SolutionCrush& crush = context->solution_crush(); - auto* mutable_hint = proto->mutable_solution_hint(); - mutable_hint->clear_vars(); - mutable_hint->clear_values(); const int num_vars = context->working_model->variables().size(); - for (int hinted_var = 0; hinted_var < num_vars; ++hinted_var) { - if (!crush.VarHasSolutionHint(hinted_var)) continue; - - // Note the use of ClampedSolutionHint() instead of SolutionHint() below. - // This also make sure a hint of INT_MIN or INT_MAX does not overflow. - // - // TODO(user): This should no longer be necessary, as we try to do that as - // soon as we update the domains, but we still do it to be safe. - int64_t hinted_value; - - // If the variable had a hint and has a representative with a hint, we also - // hint it using the representative value as a "ground truth". - const auto relation = context->GetAffineRelation(hinted_var); - if (relation.representative != hinted_var) { - // Lets first fetch the value of the representative. - const int rep = relation.representative; - if (!crush.VarHasSolutionHint(rep)) continue; - const int64_t rep_value = - crush.ClampedSolutionHint(rep, context->DomainOf(rep)); - - // Apply the affine relation. - hinted_value = rep_value * relation.coeff + relation.offset; - } else { - hinted_value = - crush.ClampedSolutionHint(hinted_var, context->DomainOf(hinted_var)); + for (int i = 0; i < num_vars; ++i) { + // If the initial hint is incomplete or infeasible, the crushed hint might + // contain values outside of their respective domains (see SolutionCrush). + crush.SetOrUpdateVarToDomain(i, context->DomainOf(i)); + } + // If the time limit is reached, the presolved model might still contain + // non-representative "affine" variables. + for (int i = 0; i < num_vars; ++i) { + const auto relation = context->GetAffineRelation(i); + if (relation.representative != i) { + crush.SetVarToLinearExpression( + i, {{relation.representative, relation.coeff}}, relation.offset); } - - mutable_hint->add_vars(hinted_var); - mutable_hint->add_values(hinted_value); } + crush.StoreSolutionAsHint(*proto); } } // namespace @@ -13844,7 +12930,7 @@ CpSolverStatus CpModelPresolver::Presolve() { } } - if (!solution_crush_.HintIsLoaded()) { + if (!solution_crush_.SolutionIsLoaded()) { context_->LoadSolutionHint(); } ExpandCpModelAndCanonicalizeConstraints(); diff --git a/ortools/sat/cp_model_presolve.h b/ortools/sat/cp_model_presolve.h index b791dac676..a016a19cd4 100644 --- a/ortools/sat/cp_model_presolve.h +++ b/ortools/sat/cp_model_presolve.h @@ -18,7 +18,6 @@ #include #include #include -#include #include #include @@ -36,7 +35,6 @@ #include "ortools/sat/solution_crush.h" #include "ortools/sat/util.h" #include "ortools/util/logging.h" -#include "ortools/util/sorted_interval_list.h" #include "ortools/util/time_limit.h" namespace operations_research { @@ -385,127 +383,6 @@ class CpModelPresolver { interval_representative_; }; -// This helper class perform copy with simplification from a model and a -// partial assignment to another model. The purpose is to minimize the size of -// the copied model, as well as to reduce the pressure on the memory sub-system. -// -// It is currently used by the LNS part, but could be used with any other scheme -// that generates partial assignments. -class ModelCopy { - public: - explicit ModelCopy(PresolveContext* context); - - // Copies all constraints from in_model to working model of the context. - // - // During the process, it will read variable domains from the context, and - // simplify constraints to minimize the size of the copied model. - // Thus it is important that the context->working_model already have the - // variables part copied. - // - // It returns false iff the model is proven infeasible. - // - // It does not clear the constraints part of the working model of the context. - // - // Note(user): If first_copy is true, we will reorder the scheduling - // constraint so that they only use reference to previously defined intervals. - // This allow to be more efficient later in a few preprocessing steps. - bool ImportAndSimplifyConstraints( - const CpModelProto& in_model, bool first_copy = false, - std::function active_constraints = nullptr); - - // Copy variables from the in_model to the working model. - // It reads the 'ignore_names' parameters from the context, and keeps or - // deletes names accordingly. - void ImportVariablesAndMaybeIgnoreNames(const CpModelProto& in_model); - - // Setup new variables from a vector of domains. - // Inactive variables will be fixed to their lower bound. - void CreateVariablesFromDomains(absl::Span domains); - - private: - // Overwrites the out_model to be unsat. Returns false. - // The arguments are used to log which constraint caused unsat. - bool CreateUnsatModel(int c, const ConstraintProto& ct); - - // Returns false if the constraint is never enforced and can be skipped. - bool PrepareEnforcementCopy(const ConstraintProto& ct); - bool PrepareEnforcementCopyWithDup(const ConstraintProto& ct); - void FinishEnforcementCopy(ConstraintProto* ct); - - // All these functions return false if the constraint is found infeasible. - bool CopyBoolOr(const ConstraintProto& ct); - bool CopyBoolOrWithDupSupport(const ConstraintProto& ct); - bool FinishBoolOrCopy(); - - bool CopyBoolAnd(const ConstraintProto& ct); - bool CopyBoolAndWithDupSupport(const ConstraintProto& ct); - - bool CopyAtMostOne(const ConstraintProto& ct); - bool CopyExactlyOne(const ConstraintProto& ct); - - bool CopyElement(const ConstraintProto& ct); - bool CopyIntProd(const ConstraintProto& ct, bool ignore_names); - bool CopyIntDiv(const ConstraintProto& ct, bool ignore_names); - bool CopyIntMod(const ConstraintProto& ct, bool ignore_names); - bool CopyLinear(const ConstraintProto& ct); - bool CopyLinearExpression(const LinearExpressionProto& expr, - LinearExpressionProto* dst); - bool CopyAutomaton(const ConstraintProto& ct); - bool CopyTable(const ConstraintProto& ct); - bool CopyAllDiff(const ConstraintProto& ct); - bool CopyLinMax(const ConstraintProto& ct); - - // If we "copy" an interval for a first time, we make sure to create the - // linear constraint between the start, size and end. This allow to simplify - // the input proto and client side code. - bool CopyInterval(const ConstraintProto& ct, int c, bool ignore_names); - bool AddLinearConstraintForInterval(const ConstraintProto& ct); - - // These function remove unperformed intervals. Note that they requires - // interval to appear before (validated) as they test unperformed by testing - // if interval_mapping_ is empty. - void CopyAndMapNoOverlap(const ConstraintProto& ct); - void CopyAndMapNoOverlap2D(const ConstraintProto& ct); - bool CopyAndMapCumulative(const ConstraintProto& ct); - - PresolveContext* context_; - - // Temp vectors. - std::vector non_fixed_variables_; - std::vector non_fixed_coefficients_; - std::vector interval_mapping_; - int starting_constraint_index_ = 0; - - std::vector temp_enforcement_literals_; - absl::flat_hash_set temp_enforcement_literals_set_; - - std::vector temp_literals_; - absl::flat_hash_set temp_literals_set_; - - ConstraintProto tmp_constraint_; -}; - -// Copy in_model to the model in the presolve context. -// It performs on the fly simplification, and returns false if the -// model is proved infeasible. If reads the parameters 'ignore_names' and keeps -// or deletes variables and constraints names accordingly. -// -// This should only be called on the first copy of the user given model. -// Note that this reorder all constraints that use intervals last. We loose the -// user-defined order, but hopefully that should not matter too much. -bool ImportModelWithBasicPresolveIntoContext(const CpModelProto& in_model, - PresolveContext* context); - -// Same as ImportModelWithBasicPresolveIntoContext() except that variable -// domains are read from domains. -bool ImportModelAndDomainsWithBasicPresolveIntoContext( - const CpModelProto& in_model, absl::Span domains, - std::function active_constraints, PresolveContext* context); - -// Copies the non constraint, non variables part of the model. -void CopyEverythingExceptVariablesAndConstraintsFieldsIntoContext( - const CpModelProto& in_model, PresolveContext* context); - // Convenient wrapper to call the full presolve. CpSolverStatus PresolveCpModel(PresolveContext* context, std::vector* postsolve_mapping); diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index afb1129c7f..b7b4ea14b7 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -55,6 +55,7 @@ #include "ortools/sat/combine_solutions.h" #include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_checker.h" +#include "ortools/sat/cp_model_copy.h" #include "ortools/sat/cp_model_lns.h" #include "ortools/sat/cp_model_mapping.h" #include "ortools/sat/cp_model_postsolve.h" @@ -817,8 +818,6 @@ void RestrictObjectiveUsingHint(CpModelProto* model_proto) { bool SolutionHintIsCompleteAndFeasible( const CpModelProto& model_proto, SolverLogger* logger = nullptr, SharedResponseManager* manager = nullptr) { - if (!model_proto.has_solution_hint()) return false; - int num_active_variables = 0; int num_hinted_variables = 0; for (int var = 0; var < model_proto.variables_size(); ++var) { @@ -889,7 +888,7 @@ bool SolutionHintIsCompleteAndFeasible( return false; } if (is_feasible) { - if (manager != nullptr) { + if (manager != nullptr && !solution.empty()) { // Add it to the pool right away! Note that we already have a log in this // case, so we don't log anything more. manager->NewSolution(solution, "complete_hint", nullptr); diff --git a/ortools/sat/diffn.cc b/ortools/sat/diffn.cc index fc05d2ddec..a541c30e28 100644 --- a/ortools/sat/diffn.cc +++ b/ortools/sat/diffn.cc @@ -248,7 +248,7 @@ NonOverlappingRectanglesEnergyPropagator:: bool NonOverlappingRectanglesEnergyPropagator::Propagate() { // TODO(user): double-check/revisit the algo for box of variable sizes. const int num_boxes = helper_.NumBoxes(); - if (!helper_.SynchronizeAndSetDirection(true, true, false)) return false; + if (!helper_.SynchronizeAndSetDirection()) return false; Rectangle bounding_box = {.x_min = std::numeric_limits::max(), .x_max = std::numeric_limits::min(), @@ -872,7 +872,7 @@ RectanglePairwisePropagator::~RectanglePairwisePropagator() { } bool RectanglePairwisePropagator::Propagate() { - if (!helper_->SynchronizeAndSetDirection(true, true, false)) return false; + if (!helper_->SynchronizeAndSetDirection()) return false; num_calls_++; std::vector restrictions; diff --git a/ortools/sat/diffn_cuts.cc b/ortools/sat/diffn_cuts.cc index 43d11f26fc..3164eec022 100644 --- a/ortools/sat/diffn_cuts.cc +++ b/ortools/sat/diffn_cuts.cc @@ -311,77 +311,54 @@ void GenerateNoOverlap2dEnergyCut( } CutGenerator CreateNoOverlap2dEnergyCutGenerator( - SchedulingConstraintHelper* x_helper, SchedulingConstraintHelper* y_helper, - SchedulingDemandHelper* x_demands_helper, - SchedulingDemandHelper* y_demands_helper, + NoOverlap2DConstraintHelper* helper, absl::Span> energies, Model* model) { CutGenerator result; result.only_run_at_level_zero = true; - AddIntegerVariableFromIntervals(x_helper, model, &result.vars); - AddIntegerVariableFromIntervals(y_helper, model, &result.vars); + AddIntegerVariableFromIntervals(&helper->x_helper(), model, &result.vars); + AddIntegerVariableFromIntervals(&helper->y_helper(), model, &result.vars); gtl::STLSortAndRemoveDuplicates(&result.vars); - result.generate_cuts = [x_helper, y_helper, x_demands_helper, - y_demands_helper, model, + result.generate_cuts = [helper, model, energies = std::vector>( energies.begin(), energies.end())]( LinearConstraintManager* manager) { - if (!x_helper->SynchronizeAndSetTimeDirection(true)) return false; - if (!y_helper->SynchronizeAndSetTimeDirection(true)) return false; + if (!helper->SynchronizeAndSetDirection(true, true, false)) return false; + SchedulingDemandHelper* x_demands_helper = &helper->x_demands_helper(); + SchedulingDemandHelper* y_demands_helper = &helper->y_demands_helper(); if (!x_demands_helper->CacheAllEnergyValues()) return true; if (!y_demands_helper->CacheAllEnergyValues()) return true; - const int num_rectangles = x_helper->NumTasks(); - std::vector active_rectangles_indexes; - active_rectangles_indexes.reserve(num_rectangles); - std::vector active_rectangles; - active_rectangles.reserve(num_rectangles); - for (int rect = 0; rect < num_rectangles; ++rect) { - if (y_helper->IsAbsent(rect) || y_helper->IsAbsent(rect)) continue; - // We do not consider rectangles controlled by 2 different unassigned - // enforcement literals. - if (!x_helper->IsPresent(rect) && !y_helper->IsPresent(rect) && - x_helper->PresenceLiteral(rect) != y_helper->PresenceLiteral(rect)) { - continue; - } - - // TODO(user): It might be possible/better to use some shifted value - // here, but for now this code is not in the hot spot, so better be - // defensive and only do connected components on really disjoint - // rectangles. - active_rectangles_indexes.push_back(rect); - Rectangle& rectangle = active_rectangles.emplace_back(); - rectangle.x_min = x_helper->StartMin(rect); - rectangle.x_max = x_helper->EndMax(rect); - rectangle.y_min = y_helper->StartMin(rect); - rectangle.y_max = y_helper->EndMax(rect); - } - - if (active_rectangles.size() <= 1) return true; - - const CompactVectorVector components = - GetOverlappingRectangleComponents(active_rectangles); - - // Forward pass. No need to do a backward pass. + const int num_rectangles = helper->NumBoxes(); std::vector rectangles; - for (int i = 0; i < components.size(); ++i) { - absl::Span indexes = components[i]; - if (indexes.size() <= 1) continue; - + rectangles.reserve(num_rectangles); + for (const auto& component : + helper->connected_components().AsVectorOfSpan()) { rectangles.clear(); - rectangles.reserve(indexes.size()); - for (const int index : indexes) { - rectangles.push_back(active_rectangles_indexes[index]); + for (const int rect : component) { + if (helper->IsAbsent(rect)) continue; + // We do not consider rectangles controlled by 2 different unassigned + // enforcement literals. + if (!helper->x_helper().IsPresent(rect) && + !helper->y_helper().IsPresent(rect) && + helper->x_helper().PresenceLiteral(rect) != + helper->y_helper().PresenceLiteral(rect)) { + continue; + } + + rectangles.push_back(rect); } + + if (rectangles.size() <= 1) continue; + GenerateNoOverlap2dEnergyCut(energies, rectangles, "NoOverlap2dXEnergy", - model, manager, x_helper, y_helper, - y_demands_helper); + model, manager, &helper->x_helper(), + &helper->y_helper(), y_demands_helper); GenerateNoOverlap2dEnergyCut(energies, rectangles, "NoOverlap2dYEnergy", - model, manager, y_helper, x_helper, - x_demands_helper); + model, manager, &helper->y_helper(), + &helper->x_helper(), x_demands_helper); } - return true; }; return result; @@ -585,49 +562,25 @@ CutGenerator CreateNoOverlap2dCompletionTimeCutGenerator( auto* product_decomposer = model->GetOrCreate(); result.generate_cuts = [helper, product_decomposer, model](LinearConstraintManager* manager) { - if (!helper->SynchronizeAndSetDirection(true, true, false)) { + if (!helper->SynchronizeAndSetDirection()) { return false; } const int num_rectangles = helper->NumBoxes(); - std::vector active_rectangles_indexes; - active_rectangles_indexes.reserve(num_rectangles); - std::vector active_rectangles; - active_rectangles.reserve(num_rectangles); - std::vector cached_areas(num_rectangles); + std::vector rectangles; + rectangles.reserve(num_rectangles); const SchedulingConstraintHelper* x_helper = &helper->x_helper(); const SchedulingConstraintHelper* y_helper = &helper->y_helper(); - for (int rect = 0; rect < num_rectangles; ++rect) { - if (!helper->IsPresent(rect)) continue; - - cached_areas[rect] = x_helper->SizeMin(rect) * y_helper->SizeMin(rect); - if (cached_areas[rect] == 0) continue; - - // TODO(user): It might be possible/better to use some shifted value - // here, but for now this code is not in the hot spot, so better be - // defensive and only do connected components on really disjoint - // rectangles. - active_rectangles_indexes.push_back(rect); - Rectangle& rectangle = active_rectangles.emplace_back(); - rectangle.x_min = x_helper->StartMin(rect); - rectangle.x_max = x_helper->EndMax(rect); - rectangle.y_min = y_helper->StartMin(rect); - rectangle.y_max = y_helper->EndMax(rect); - } - - if (active_rectangles.size() <= 1) return true; - - const CompactVectorVector components = - GetOverlappingRectangleComponents(active_rectangles); - std::vector rectangles; - for (int i = 0; i < components.size(); ++i) { - absl::Span indexes = components[i]; - if (indexes.size() <= 1) continue; - + for (const auto& component : + helper->connected_components().AsVectorOfSpan()) { rectangles.clear(); - rectangles.reserve(indexes.size()); - for (const int index : indexes) { - rectangles.push_back(active_rectangles_indexes[index]); + if (component.size() <= 1) continue; + for (int rect : component) { + if (!helper->IsPresent(rect)) continue; + if (x_helper->SizeMin(rect) == 0 || y_helper->SizeMin(rect) == 0) { + continue; + } + rectangles.push_back(rect); } auto generate_cuts = [product_decomposer, manager, model, helper, diff --git a/ortools/sat/diffn_cuts.h b/ortools/sat/diffn_cuts.h index 8532adb929..1024cc00c8 100644 --- a/ortools/sat/diffn_cuts.h +++ b/ortools/sat/diffn_cuts.h @@ -48,9 +48,7 @@ CutGenerator CreateNoOverlap2dCompletionTimeCutGenerator( // The maximum area is the area of the bounding rectangle of each intervals // at level 0. CutGenerator CreateNoOverlap2dEnergyCutGenerator( - SchedulingConstraintHelper* x_helper, SchedulingConstraintHelper* y_helper, - SchedulingDemandHelper* x_demands_helper, - SchedulingDemandHelper* y_demands_helper, + NoOverlap2DConstraintHelper* helper, absl::Span> energies, Model* model); // Internal methods and data structures, useful for testing. diff --git a/ortools/sat/linear_relaxation.cc b/ortools/sat/linear_relaxation.cc index 6e41755bce..edc222ad26 100644 --- a/ortools/sat/linear_relaxation.cc +++ b/ortools/sat/linear_relaxation.cc @@ -1712,10 +1712,6 @@ void AddNoOverlap2dCutGenerator(const ConstraintProto& ct, Model* m, IntervalsRepository* intervals_repository = m->GetOrCreate(); - SchedulingConstraintHelper* x_helper = - intervals_repository->GetOrCreateHelper(x_intervals); - SchedulingConstraintHelper* y_helper = - intervals_repository->GetOrCreateHelper(y_intervals); NoOverlap2DConstraintHelper* no_overlap_helper = intervals_repository->GetOrCreate2DHelper(x_intervals, y_intervals); @@ -1750,23 +1746,17 @@ void AddNoOverlap2dCutGenerator(const ConstraintProto& ct, Model* m, if (!has_variable_part) return; - SchedulingDemandHelper* x_demands_helper = - intervals_repository->GetOrCreateDemandHelper(y_helper, - x_helper->Sizes()); - SchedulingDemandHelper* y_demands_helper = - intervals_repository->GetOrCreateDemandHelper(x_helper, - y_helper->Sizes()); - std::vector> energies; - const int num_rectangles = x_helper->NumTasks(); + const int num_rectangles = no_overlap_helper->NumBoxes(); auto* product_decomposer = m->GetOrCreate(); for (int i = 0; i < num_rectangles; ++i) { energies.push_back(product_decomposer->TryToDecompose( - x_helper->Sizes()[i], y_helper->Sizes()[i])); + no_overlap_helper->x_helper().Sizes()[i], + no_overlap_helper->y_helper().Sizes()[i])); } - relaxation->cut_generators.push_back(CreateNoOverlap2dEnergyCutGenerator( - x_helper, y_helper, x_demands_helper, y_demands_helper, energies, m)); + relaxation->cut_generators.push_back( + CreateNoOverlap2dEnergyCutGenerator(no_overlap_helper, energies, m)); } void AddLinMaxCutGenerator(const ConstraintProto& ct, Model* m, diff --git a/ortools/sat/no_overlap_2d_helper.cc b/ortools/sat/no_overlap_2d_helper.cc index 47f3e6473a..e04a4e955e 100644 --- a/ortools/sat/no_overlap_2d_helper.cc +++ b/ortools/sat/no_overlap_2d_helper.cc @@ -38,6 +38,7 @@ bool NoOverlap2DConstraintHelper::SynchronizeAndSetDirection( bool swap_x_and_y) { if (axes_are_swapped_ != swap_x_and_y) { std::swap(x_helper_, y_helper_); + std::swap(x_demands_helper_, y_demands_helper_); axes_are_swapped_ = !axes_are_swapped_; } if (!x_helper_->SynchronizeAndSetTimeDirection(x_is_forward_after_swap)) @@ -47,6 +48,22 @@ bool NoOverlap2DConstraintHelper::SynchronizeAndSetDirection( return true; } +SchedulingDemandHelper& NoOverlap2DConstraintHelper::x_demands_helper() { + if (x_demands_helper_ == nullptr) { + x_demands_helper_ = std::make_unique( + x_helper_->Sizes(), y_helper_.get(), model_); + } + return *x_demands_helper_; +} + +SchedulingDemandHelper& NoOverlap2DConstraintHelper::y_demands_helper() { + if (y_demands_helper_ == nullptr) { + y_demands_helper_ = std::make_unique( + y_helper_->Sizes(), x_helper_.get(), model_); + } + return *y_demands_helper_; +} + RectangleInRange NoOverlap2DConstraintHelper::GetItemRangeForSizeMin( int index) const { return RectangleInRange{ @@ -249,10 +266,7 @@ void NoOverlap2DConstraintHelper::Reset( active_bounding_boxes.reserve(new_num_boxes); active_box_indexes.reserve(new_num_boxes); for (int box : non_fixed_box_indexes) { - active_bounding_boxes.push_back({.x_min = x_helper_->StartMin(box), - .x_max = x_helper_->EndMax(box), - .y_min = y_helper_->StartMin(box), - .y_max = y_helper_->EndMax(box)}); + active_bounding_boxes.push_back(GetBoundingRectangle(box)); active_box_indexes.push_back({box, false}); } for (int box = 0; box < fixed_boxes.size(); ++box) { @@ -297,6 +311,8 @@ void NoOverlap2DConstraintHelper::Reset( y_helper_ = std::make_unique( std::move(y_starts), std::move(y_ends), std::move(y_sizes), std::move(y_reason_for_presence), model_); + x_demands_helper_ = nullptr; + y_demands_helper_ = nullptr; } bool NoOverlap2DConstraintHelper::Propagate() { @@ -306,7 +322,7 @@ bool NoOverlap2DConstraintHelper::Propagate() { if (!x_helper_->Propagate() || !y_helper_->Propagate()) return false; if (x_helper_->CurrentDecisionLevel() == 0) { - SynchronizeAndSetDirection(true, true, false); + SynchronizeAndSetDirection(); int num_boxes = NumBoxes(); // Subtle: it is tempting to run this logic once for every connected @@ -330,10 +346,7 @@ bool NoOverlap2DConstraintHelper::Propagate() { } if (IsOptional(box_index) || !IsFixed(box_index)) { non_fixed_boxes.push_back( - {.bounding_area = {.x_min = x_helper_->StartMin(box_index), - .x_max = x_helper_->EndMax(box_index), - .y_min = y_helper_->StartMin(box_index), - .y_max = y_helper_->EndMax(box_index)}, + {.bounding_area = GetBoundingRectangle(box_index), .x_size = x_helper_->SizeMin(box_index), .y_size = y_helper_->SizeMin(box_index)}); non_fixed_box_indexes.push_back(box_index); diff --git a/ortools/sat/no_overlap_2d_helper.h b/ortools/sat/no_overlap_2d_helper.h index bf993252b5..c466b8ec84 100644 --- a/ortools/sat/no_overlap_2d_helper.h +++ b/ortools/sat/no_overlap_2d_helper.h @@ -64,9 +64,9 @@ class NoOverlap2DConstraintHelper : public PropagatorInterface { void RegisterWith(GenericLiteralWatcher* watcher); - bool SynchronizeAndSetDirection(bool x_is_forward_after_swap, - bool y_is_forward_after_swap, - bool swap_x_and_y); + bool SynchronizeAndSetDirection(bool x_is_forward_after_swap = true, + bool y_is_forward_after_swap = true, + bool swap_x_and_y = false); bool IsOptional(int index) const { return x_helper_->IsOptional(index) || y_helper_->IsOptional(index); @@ -76,6 +76,17 @@ class NoOverlap2DConstraintHelper : public PropagatorInterface { return x_helper_->IsPresent(index) && y_helper_->IsPresent(index); } + bool IsAbsent(int index) const { + return x_helper_->IsAbsent(index) || y_helper_->IsAbsent(index); + } + + Rectangle GetBoundingRectangle(int index) const { + return {.x_min = x_helper_->StartMin(index), + .x_max = x_helper_->EndMax(index), + .y_min = y_helper_->StartMin(index), + .y_max = y_helper_->EndMax(index)}; + } + bool IsFixed(int index) const { return x_helper_->StartIsFixed(index) && x_helper_->EndIsFixed(index) && y_helper_->StartIsFixed(index) && y_helper_->EndIsFixed(index); @@ -196,6 +207,9 @@ class NoOverlap2DConstraintHelper : public PropagatorInterface { SchedulingConstraintHelper& x_helper() const { return *x_helper_; } SchedulingConstraintHelper& y_helper() const { return *y_helper_; } + SchedulingDemandHelper& x_demands_helper(); + SchedulingDemandHelper& y_demands_helper(); + const CompactVectorVector& connected_components() const { return connected_components_; } @@ -211,6 +225,8 @@ class NoOverlap2DConstraintHelper : public PropagatorInterface { bool axes_are_swapped_; std::unique_ptr x_helper_; std::unique_ptr y_helper_; + std::unique_ptr x_demands_helper_; + std::unique_ptr y_demands_helper_; Model* model_; GenericLiteralWatcher* watcher_; std::vector propagators_watching_; diff --git a/ortools/sat/presolve_context.cc b/ortools/sat/presolve_context.cc index aa033dc01d..129cfe85a5 100644 --- a/ortools/sat/presolve_context.cc +++ b/ortools/sat/presolve_context.cc @@ -141,6 +141,7 @@ int PresolveContext::GetTrueLiteral() { if (!true_literal_is_defined_) { true_literal_is_defined_ = true; true_literal_ = NewIntVar(Domain(1)); + solution_crush_.SetVarToConjunction(true_literal_, {}); } return true_literal_; } @@ -511,8 +512,8 @@ bool PresolveContext::DomainContains(const LinearExpressionProto& expr, return DomainContains(expr.vars(0), (value - expr.offset()) / expr.coeffs(0)); } -ABSL_MUST_USE_RESULT bool PresolveContext::IntersectDomainWithInternal( - int ref, const Domain& domain, bool* domain_modified, bool update_hint) { +ABSL_MUST_USE_RESULT bool PresolveContext::IntersectDomainWith( + int ref, const Domain& domain, bool* domain_modified) { DCHECK(!DomainIsEmpty(ref)); const int var = PositiveRef(ref); @@ -539,20 +540,17 @@ ABSL_MUST_USE_RESULT bool PresolveContext::IntersectDomainWithInternal( domain.ToString())); } - // TODO(user): always update the hint, remove the `update_hint` argument. - if (update_hint) { - solution_crush_.UpdateVarToDomain(var, domains_[var]); - } + solution_crush_.SetOrUpdateVarToDomain(var, domains_[var]); // Propagate the domain of the representative right away. // Note that the recursive call should only by one level deep. const AffineRelation::Relation r = GetAffineRelation(var); if (r.representative == var) return true; - return IntersectDomainWithInternal(r.representative, - DomainOf(var) - .AdditionWith(Domain(-r.offset)) - .InverseMultiplicationBy(r.coeff), - /*domain_modified=*/nullptr, update_hint); + return IntersectDomainWith(r.representative, + DomainOf(var) + .AdditionWith(Domain(-r.offset)) + .InverseMultiplicationBy(r.coeff), + /*domain_modified=*/nullptr); } ABSL_MUST_USE_RESULT bool PresolveContext::IntersectDomainWith( @@ -588,16 +586,6 @@ ABSL_MUST_USE_RESULT bool PresolveContext::SetLiteralToTrue(int lit) { return SetLiteralToFalse(NegatedRef(lit)); } -ABSL_MUST_USE_RESULT bool PresolveContext::SetLiteralAndHintToFalse(int lit) { - const int var = PositiveRef(lit); - const int64_t value = RefIsPositive(lit) ? 0 : 1; - return IntersectDomainWithAndUpdateHint(var, Domain(value)); -} - -ABSL_MUST_USE_RESULT bool PresolveContext::SetLiteralAndHintToTrue(int lit) { - return SetLiteralAndHintToFalse(NegatedRef(lit)); -} - bool PresolveContext::ConstraintIsInactive(int index) const { const ConstraintProto& ct = working_model->constraints(index); if (ct.constraint_case() == @@ -687,9 +675,10 @@ void PresolveContext::AddVariableUsage(int c) { #ifdef CHECK_HINT // Crash if the loaded hint is infeasible for this constraint. // This is helpful to debug a wrong presolve that kill a feasible solution. - if (working_model->has_solution_hint() && solution_crush_.HintIsLoaded() && + if (working_model->has_solution_hint() && + solution_crush_.SolutionIsLoaded() && !ConstraintIsFeasible(*working_model, ct, - solution_crush_.SolutionHint())) { + solution_crush_.GetVarValues())) { LOG(FATAL) << "Hint infeasible for constraint #" << c << " : " << ct.ShortDebugString(); } @@ -745,9 +734,10 @@ void PresolveContext::UpdateConstraintVariableUsage(int c) { #ifdef CHECK_HINT // Crash if the loaded hint is infeasible for this constraint. // This is helpful to debug a wrong presolve that kill a feasible solution. - if (working_model->has_solution_hint() && solution_crush_.HintIsLoaded() && + if (working_model->has_solution_hint() && + solution_crush_.SolutionIsLoaded() && !ConstraintIsFeasible(*working_model, ct, - solution_crush_.SolutionHint())) { + solution_crush_.GetVarValues())) { LOG(FATAL) << "Hint infeasible for constraint #" << c << " : " << ct.ShortDebugString(); } @@ -1339,7 +1329,7 @@ void PresolveContext::ResetAfterCopy() { var_to_constraints_.clear(); var_to_num_linear1_.clear(); objective_map_.clear(); - DCHECK(!solution_crush_.HintIsLoaded()); + DCHECK(!solution_crush_.SolutionIsLoaded()); } // Create the internal structure for any new variables in working_model. @@ -1394,8 +1384,7 @@ void PresolveContext::LoadSolutionHint() { } } } - solution_crush_.Resize(working_model->variables().size()); - solution_crush_.LoadSolution(hint_values); + solution_crush_.LoadSolution(working_model->variables().size(), hint_values); } void PresolveContext::CanonicalizeDomainOfSizeTwo(int var) { @@ -1909,11 +1898,11 @@ bool PresolveContext::CanonicalizeOneObjectiveVariable(int var) { var_to_constraints_[var].contains(kObjectiveConstraint)) { UpdateRuleStats("objective: variable not used elsewhere"); if (coeff > 0) { - if (!IntersectDomainWithAndUpdateHint(var, Domain(MinOf(var)))) { + if (!IntersectDomainWith(var, Domain(MinOf(var)))) { return false; } } else { - if (!IntersectDomainWithAndUpdateHint(var, Domain(MaxOf(var)))) { + if (!IntersectDomainWith(var, Domain(MaxOf(var)))) { return false; } } @@ -2768,7 +2757,7 @@ void CreateValidModelWithSingleConstraint(const ConstraintProto& ct, bool PresolveContext::DebugTestHintFeasibility() { WriteVariableDomainsToProto(); - const absl::Span hint = solution_crush_.SolutionHint(); + const absl::Span hint = solution_crush_.GetVarValues(); if (hint.size() != working_model->variables().size()) return false; return SolutionIsFeasible(*working_model, hint); } diff --git a/ortools/sat/presolve_context.h b/ortools/sat/presolve_context.h index 44195ac37e..ccde615ac4 100644 --- a/ortools/sat/presolve_context.h +++ b/ortools/sat/presolve_context.h @@ -103,28 +103,30 @@ class PresolveContext { random_(model->GetOrCreate()) {} // Helpers to adds new variables to the presolved model. - // - // TODO(user): We should control more how this is called so we can update - // a solution hint accordingly. + + // Creates a new integer variable with the given domain. + // WARNING: this does not set any hint value for the new variable. int NewIntVar(const Domain& domain); + + // Creates a new Boolean variable. + // WARNING: this does not set any hint value for the new variable. int NewBoolVar(absl::string_view source); - // This should replace NewIntVar() eventually in order to be able to crush - // primal solution or just update the hint. - // - // By default this also create the linking constraint new_var = definition. - // Returns -1 if we couldn't create the definition due to overflow. + // Creates a new integer variable with the given domain and definition. + // By default this also creates the linking constraint new_var = definition. + // Its hint value is set to the value of the definition. Returns -1 if we + // couldn't create the definition due to overflow. int NewIntVarWithDefinition( const Domain& domain, absl::Span> definition, bool append_constraint_to_mapping_model = false); - // Create a new bool var. - // Its hint value will be the same as the value of the given clause. + // Creates a new bool var. + // Its hint value is set to the value of the given clause. int NewBoolVarWithClause(absl::Span clause); - // Create a new bool var. - // Its hint value will be the same as the value of the given conjunction. + // Creates a new bool var. + // Its hint value is set to the value of the given conjunction. int NewBoolVarWithConjunction(absl::Span conjunction); // Some expansion code use constant literal to be simpler to write. This will @@ -275,22 +277,11 @@ class PresolveContext { // Returns false if the new domain is empty. Sets 'domain_modified' (if // provided) to true iff the domain is modified otherwise does not change it. ABSL_MUST_USE_RESULT bool IntersectDomainWith( - int ref, const Domain& domain, bool* domain_modified = nullptr) { - return IntersectDomainWithInternal(ref, domain, domain_modified, - /*update_hint=*/false); - } - - ABSL_MUST_USE_RESULT bool IntersectDomainWithAndUpdateHint( - int ref, const Domain& domain, bool* domain_modified = nullptr) { - return IntersectDomainWithInternal(ref, domain, domain_modified, - /*update_hint=*/true); - } + int ref, const Domain& domain, bool* domain_modified = nullptr); // Returns false if the 'lit' doesn't have the desired value in the domain. ABSL_MUST_USE_RESULT bool SetLiteralToFalse(int lit); ABSL_MUST_USE_RESULT bool SetLiteralToTrue(int lit); - ABSL_MUST_USE_RESULT bool SetLiteralAndHintToFalse(int lit); - ABSL_MUST_USE_RESULT bool SetLiteralAndHintToTrue(int lit); // Same as IntersectDomainWith() but take a linear expression as input. // If this expression if of size > 1, this does nothing for now, so it will @@ -713,11 +704,6 @@ class PresolveContext { bool InsertVarValueEncodingInternal(int literal, int var, int64_t value, bool add_constraints); - ABSL_MUST_USE_RESULT bool IntersectDomainWithInternal(int ref, - const Domain& domain, - bool* domain_modified, - bool update_hint); - SolverLogger* logger_; const SatParameters& params_; TimeLimit* time_limit_; diff --git a/ortools/sat/presolve_context_test.cc b/ortools/sat/presolve_context_test.cc index 1d212f2136..d6e45ea991 100644 --- a/ortools/sat/presolve_context_test.cc +++ b/ortools/sat/presolve_context_test.cc @@ -756,7 +756,7 @@ TEST(PresolveContextTest, IntersectDomainWithAffineExpression) { EXPECT_EQ(context.DomainOf(0), Domain(0, 1)); } -TEST(PresolveContextTest, IntersectDomainAndUpdateHint) { +TEST(PresolveContextTest, IntersectDomainWithUpdatesHint) { Model model; CpModelProto working_model = ParseTestProto(R"pb( variables { domain: [ 0, 10 ] } @@ -769,10 +769,10 @@ TEST(PresolveContextTest, IntersectDomainAndUpdateHint) { context.InitializeNewDomains(); context.LoadSolutionHint(); - EXPECT_TRUE(context.IntersectDomainWithAndUpdateHint(0, Domain(5, 20))); + EXPECT_TRUE(context.IntersectDomainWith(0, Domain(5, 20))); EXPECT_EQ(context.DomainOf(0), Domain(5, 10)); - EXPECT_EQ(context.solution_crush().SolutionHint(0), 5); + EXPECT_EQ(context.solution_crush().GetVarValues()[0], 5); } TEST(PresolveContextTest, DomainSuperSetOf) { @@ -1074,21 +1074,14 @@ TEST(PresolveContextTest, LoadSolutionHint) { context.InitializeNewDomains(); context.LoadSolutionHint(); - SolutionCrush& crush = context.solution_crush(); - EXPECT_TRUE(crush.HintIsLoaded()); - EXPECT_TRUE(crush.VarHasSolutionHint(0)); - EXPECT_TRUE(crush.VarHasSolutionHint(1)); // From the fixed domain. - EXPECT_TRUE(crush.VarHasSolutionHint(2)); - EXPECT_EQ(crush.SolutionHint(0), 10); // Clamped to the domain. - EXPECT_EQ(crush.SolutionHint(1), 5); // From the fixed domain. - EXPECT_EQ(crush.SolutionHint(2), 0); - EXPECT_EQ(crush.GetRefSolutionHint(0), 10); - EXPECT_EQ(crush.GetRefSolutionHint(NegatedRef(0)), -10); - EXPECT_FALSE(crush.LiteralSolutionHint(2)); - EXPECT_TRUE(crush.LiteralSolutionHint(NegatedRef(2))); - EXPECT_TRUE(crush.LiteralSolutionHintIs(2, false)); - EXPECT_TRUE(crush.LiteralSolutionHintIs(NegatedRef(2), true)); - EXPECT_THAT(crush.SolutionHint(), ::testing::ElementsAre(10, 5, 0)); + context.solution_crush().StoreSolutionAsHint(working_model); + // All hints should be clamped to their respective domains, and new hints + // should be added for the fixed variables. + PartialVariableAssignment expected_solution_hint = + ParseTestProto(R"pb(vars: [ 0, 1, 2 ] + values: [ 10, 5, 0 ])pb"); + EXPECT_THAT(working_model.solution_hint(), + testing::EqualsProto(expected_solution_hint)); } } // namespace diff --git a/ortools/sat/presolve_util.cc b/ortools/sat/presolve_util.cc index aad993fb1f..ffe0a02b62 100644 --- a/ortools/sat/presolve_util.cc +++ b/ortools/sat/presolve_util.cc @@ -344,7 +344,7 @@ int64_t ActivityBoundHelper::ComputeActivity( // - If not, choose biggest part left. TODO(user): compute sum of coeff in part? void ActivityBoundHelper::PartitionIntoAmo( absl::Span> terms) { - amo_sums_.clear(); + auto amo_sums = amo_sums_.ClearedView(num_at_most_ones_); const int num_terms = terms.size(); to_sort_.clear(); @@ -352,9 +352,10 @@ void ActivityBoundHelper::PartitionIntoAmo( for (int i = 0; i < num_terms; ++i) { const Index index = IndexFromLiteral(terms[i].first); const int64_t coeff = terms[i].second; + DCHECK_GE(coeff, 0); if (index < amo_indices_.size()) { for (const int a : amo_indices_[index]) { - amo_sums_[a] += coeff; + amo_sums[a] += coeff; } } to_sort_.push_back( @@ -369,7 +370,6 @@ void ActivityBoundHelper::PartitionIntoAmo( int num_parts = 0; partition_.resize(num_terms); - used_amo_to_dense_index_.clear(); for (const TermWithIndex& term : to_sort_) { const int original_i = term.span_index; const Index index = term.index; @@ -379,15 +379,16 @@ void ActivityBoundHelper::PartitionIntoAmo( bool done = false; if (index < amo_indices_.size()) { for (const int a : amo_indices_[index]) { - const auto it = used_amo_to_dense_index_.find(a); - if (it != used_amo_to_dense_index_.end()) { - partition_[original_i] = it->second; + // Tricky/Optim: we use negative amo_sums to indicate if this amo was + // already used and its dense index (we use -1 - index). + const int64_t sum_left = amo_sums[a]; + if (sum_left < 0) { + partition_[original_i] = -sum_left - 1; done = true; break; } - const int64_t sum_left = amo_sums_[a]; - amo_sums_[a] -= coeff; + amo_sums[a] -= coeff; if (sum_left > best_sum) { best_sum = sum_left; best = a; @@ -400,7 +401,7 @@ void ActivityBoundHelper::PartitionIntoAmo( if (best == -1) { partition_[original_i] = num_parts++; } else { - used_amo_to_dense_index_[best] = num_parts; + amo_sums[best] = -num_parts - 1; // "dense indexing" partition_[original_i] = num_parts; ++num_parts; } @@ -412,12 +413,12 @@ void ActivityBoundHelper::PartitionIntoAmo( // Similar algo as above for this simpler case. std::vector> ActivityBoundHelper::PartitionLiteralsIntoAmo(absl::Span literals) { - amo_sums_.clear(); + auto amo_sums = amo_sums_.ClearedView(num_at_most_ones_); for (const int ref : literals) { const Index index = IndexFromLiteral(ref); if (index < amo_indices_.size()) { for (const int a : amo_indices_[index]) { - amo_sums_[a] += 1; + amo_sums[a] += 1; } } } @@ -425,7 +426,6 @@ ActivityBoundHelper::PartitionLiteralsIntoAmo(absl::Span literals) { int num_parts = 0; const int num_literals = literals.size(); partition_.resize(num_literals); - used_amo_to_dense_index_.clear(); for (int i = 0; i < literals.size(); ++i) { const Index index = IndexFromLiteral(literals[i]); int best = -1; @@ -433,15 +433,17 @@ ActivityBoundHelper::PartitionLiteralsIntoAmo(absl::Span literals) { bool done = false; if (index < amo_indices_.size()) { for (const int a : amo_indices_[index]) { - const auto it = used_amo_to_dense_index_.find(a); - if (it != used_amo_to_dense_index_.end()) { - partition_[i] = it->second; + const int64_t sum_left = amo_sums[a]; + + // Tricky/Optim: we use negative amo_sums to indicate if this amo was + // already used and its dense index (we use -1 - index). + if (sum_left < 0) { + partition_[i] = -sum_left - 1; done = true; break; } - const int64_t sum_left = amo_sums_[a]; - amo_sums_[a] -= 1; + amo_sums[a] -= 1; if (sum_left > best_sum) { best_sum = sum_left; best = a; @@ -452,7 +454,7 @@ ActivityBoundHelper::PartitionLiteralsIntoAmo(absl::Span literals) { // New element. if (best != -1) { - used_amo_to_dense_index_[best] = num_parts; + amo_sums[best] = -num_parts - 1; } partition_[i] = num_parts++; } @@ -464,13 +466,13 @@ ActivityBoundHelper::PartitionLiteralsIntoAmo(absl::Span literals) { } bool ActivityBoundHelper::IsAmo(absl::Span literals) { - amo_sums_.clear(); + auto amo_sums = amo_sums_.ClearedView(num_at_most_ones_); for (int i = 0; i < literals.size(); ++i) { bool has_max_size = false; const Index index = IndexFromLiteral(literals[i]); if (index >= amo_indices_.size()) return false; for (const int a : amo_indices_[index]) { - if (amo_sums_[a]++ == i) has_max_size = true; + if (amo_sums[a]++ == i) has_max_size = true; } if (!has_max_size) return false; } diff --git a/ortools/sat/presolve_util.h b/ortools/sat/presolve_util.h index 98ffd1e4d0..d950574a1d 100644 --- a/ortools/sat/presolve_util.h +++ b/ortools/sat/presolve_util.h @@ -152,6 +152,63 @@ bool AddLinearConstraintMultiple(int64_t factor, const ConstraintProto& to_add, bool SubstituteVariable(int var, int64_t var_coeff_in_definition, const ConstraintProto& definition, ConstraintProto* ct); +// Same as a vector or hash_map where the index are in [0, size), +// but optimized for the case where only a few entries are touched before the +// vector need to be reset to zero and used again. +// +// TODO(user): Maybe a SparseBitset + sparse clear is better. But this is a +// worth alternative to test IMO. +template +class VectorWithSparseUsage { + public: + // Taking a view allow to cache the never changing addresses. + class View { + public: + View(int* i, int* pi, T* pv) + : index_to_position_(i), + position_to_index_(pi), + position_to_value_(pv) {} + + T& operator[](int index) { + const int p = index_to_position_[index]; + if (p < size_ && index == position_to_index_[p]) { + // [index] was already called. + return position_to_value_[p]; + } + + // First call. + index_to_position_[index] = size_; + position_to_index_[size_] = index; + position_to_value_[size_] = 0; + return position_to_value_[size_++]; + } + + private: + int size_ = 0; + int* const index_to_position_; + int* const position_to_index_; + T* const position_to_value_; + }; + + // This reserve the size for using indices in [0, size). + View ClearedView(int size) { + index_to_position_.resize(size); + position_to_index_.resize(size); + position_to_value_.resize(size); + return View(index_to_position_.data(), position_to_index_.data(), + position_to_value_.data()); + } + + private: + // We never need to clear this. We can detect stale positions if + // position_to_index_[index_to_position_[index]] is inconsistent. + std::vector index_to_position_; + + // Only the beginning [0, num touched indices) is used here. + std::vector position_to_index_; + std::vector position_to_value_; +}; + // Try to get more precise min/max activity of a linear constraints using // at most ones from the model. This is heuristic based but should be relatively // fast. @@ -184,7 +241,7 @@ class ActivityBoundHelper { // // Important: We shouldn't have duplicates or a lit and NegatedRef(lit) // appearing both. - + // // Note: the result of this function is not exact (it uses an heuristic to // detect AMOs), but it does not depend on the order of the input terms, so // passing an input in non-deterministic order is fine. @@ -273,8 +330,7 @@ class ActivityBoundHelper { std::vector to_sort_; // We partition the set of term into disjoint at most one. - absl::flat_hash_map used_amo_to_dense_index_; - absl::flat_hash_map amo_sums_; + VectorWithSparseUsage amo_sums_; std::vector partition_; std::vector max_by_partition_; std::vector second_max_by_partition_; diff --git a/ortools/sat/presolve_util_test.cc b/ortools/sat/presolve_util_test.cc index 606764df09..71398b8809 100644 --- a/ortools/sat/presolve_util_test.cc +++ b/ortools/sat/presolve_util_test.cc @@ -508,6 +508,22 @@ TEST(FindSingleLinearDifferenceTest, OkNotSamePosition) { EXPECT_EQ(coeff2, 3); } +TEST(VectorWithSparseUsageTest, RandomTest) { + absl::BitGen random; + VectorWithSparseUsage to_test; + for (int num_test = 0; num_test < 20; ++num_test) { + const int size = absl::Uniform(random, 0, 1000); + auto view = to_test.ClearedView(size); + std::vector reference(size, 0); + for (int j = 0; j < size; ++j) { + const int index = absl::Uniform(random, 0, size); + reference[index] += 1; + view[index] += 1; + ASSERT_EQ(view[index], reference[index]); + } + } +} + } // namespace } // namespace sat } // namespace operations_research diff --git a/ortools/sat/sat_inprocessing.cc b/ortools/sat/sat_inprocessing.cc index 7d4a85ae33..f13067f17d 100644 --- a/ortools/sat/sat_inprocessing.cc +++ b/ortools/sat/sat_inprocessing.cc @@ -171,6 +171,7 @@ bool Inprocessing::PresolveLoop(SatPresolveOptions options) { bool Inprocessing::InprocessingRound() { DCHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0); + if (sat_solver_->ModelIsUnsat()) return false; WallTimer wall_timer; wall_timer.Start(); diff --git a/ortools/sat/shaving_solver.cc b/ortools/sat/shaving_solver.cc index d3430b0d40..7c0e611068 100644 --- a/ortools/sat/shaving_solver.cc +++ b/ortools/sat/shaving_solver.cc @@ -28,6 +28,7 @@ #include "absl/synchronization/mutex.h" #include "ortools/base/logging.h" #include "ortools/graph/connected_components.h" +#include "ortools/sat/cp_model_copy.h" #include "ortools/sat/cp_model_lns.h" #include "ortools/sat/cp_model_presolve.h" #include "ortools/sat/cp_model_solver_helpers.h" diff --git a/ortools/sat/solution_crush.cc b/ortools/sat/solution_crush.cc index 001660da13..7681b9e6cb 100644 --- a/ortools/sat/solution_crush.cc +++ b/ortools/sat/solution_crush.cc @@ -17,7 +17,7 @@ #include #include #include -#ifdef CHECK_HINT +#ifdef CHECK_CRUSH #include #include #endif @@ -38,131 +38,121 @@ namespace operations_research { namespace sat { -void SolutionCrush::Resize(int new_size) { - hint_.resize(new_size, 0); - hint_has_value_.resize(new_size, false); -} - void SolutionCrush::LoadSolution( - const absl::flat_hash_map& solution) { - CHECK(!hint_is_loaded_); - model_has_hint_ = !solution.empty(); - hint_is_loaded_ = true; + int num_vars, const absl::flat_hash_map& solution) { + CHECK(!solution_is_loaded_); + CHECK(var_has_value_.empty()); + CHECK(var_values_.empty()); + solution_is_loaded_ = true; + var_has_value_.resize(num_vars, false); + var_values_.resize(num_vars, 0); for (const auto [var, value] : solution) { - hint_has_value_[var] = true; - hint_[var] = value; + var_has_value_[var] = true; + var_values_[var] = value; } } +void SolutionCrush::Resize(int new_size) { + if (!solution_is_loaded_) return; + var_has_value_.resize(new_size, false); + var_values_.resize(new_size, 0); +} + void SolutionCrush::MaybeSetLiteralToValueEncoding(int literal, int var, int64_t value) { - if (hint_is_loaded_) { - const int bool_var = PositiveRef(literal); - DCHECK(RefIsPositive(var)); - if (!hint_has_value_[bool_var] && hint_has_value_[var]) { - const int64_t bool_value = hint_[var] == value ? 1 : 0; - hint_has_value_[bool_var] = true; - hint_[bool_var] = RefIsPositive(literal) ? bool_value : 1 - bool_value; - } + DCHECK(RefIsPositive(var)); + if (!solution_is_loaded_) return; + if (!HasValue(PositiveRef(literal)) && HasValue(var)) { + SetLiteralValue(literal, GetVarValue(var) == value); } } void SolutionCrush::SetVarToLinearExpression( - int new_var, absl::Span> linear) { - // We only fill the hint of the new variable if all the variable involved - // in its definition have a value. - if (!hint_is_loaded_) return; - int64_t new_value = 0; + int new_var, absl::Span> linear, + int64_t offset) { + if (!solution_is_loaded_) return; + int64_t new_value = offset; for (const auto [var, coeff] : linear) { - CHECK_GE(var, 0); - CHECK_LE(var, hint_.size()); - if (!hint_has_value_[var]) return; - new_value += coeff * hint_[var]; + if (!HasValue(var)) return; + new_value += coeff * GetVarValue(var); } - SetVarHint(new_var, new_value); + SetVarValue(new_var, new_value); } void SolutionCrush::SetVarToLinearExpression(int new_var, absl::Span vars, - absl::Span coeffs) { + absl::Span coeffs, + int64_t offset) { DCHECK_EQ(vars.size(), coeffs.size()); - if (!hint_is_loaded_) return; - int64_t new_value = 0; + if (!solution_is_loaded_) return; + int64_t new_value = offset; for (int i = 0; i < vars.size(); ++i) { const int var = vars[i]; const int64_t coeff = coeffs[i]; - CHECK_GE(var, 0); - CHECK_LE(var, hint_.size()); - if (!hint_has_value_[var]) return; - new_value += coeff * hint_[var]; + if (!HasValue(var)) return; + new_value += coeff * GetVarValue(var); } - SetVarHint(new_var, new_value); + SetVarValue(new_var, new_value); } void SolutionCrush::SetVarToClause(int new_var, absl::Span clause) { - if (hint_is_loaded_) { - int new_hint = 0; - bool all_have_hint = true; - for (const int literal : clause) { - const int var = PositiveRef(literal); - if (!hint_has_value_[var]) { - all_have_hint = false; - break; - } - if (hint_[var] == (RefIsPositive(literal) ? 1 : 0)) { - new_hint = 1; - break; - } + if (!solution_is_loaded_) return; + int new_value = 0; + bool all_have_value = true; + for (const int literal : clause) { + const int var = PositiveRef(literal); + if (!HasValue(var)) { + all_have_value = false; + break; } - // Leave the `new_var` hint unassigned if any literal is not hinted. - if (all_have_hint) { - hint_has_value_[new_var] = true; - hint_[new_var] = new_hint; + if (GetVarValue(var) == (RefIsPositive(literal) ? 1 : 0)) { + new_value = 1; + break; } } + // Leave the `new_var` unassigned if any literal is unassigned. + if (all_have_value) { + SetVarValue(new_var, new_value); + } } void SolutionCrush::SetVarToConjunction(int new_var, absl::Span conjunction) { - if (hint_is_loaded_) { - int new_hint = 1; - bool all_have_hint = true; - for (const int literal : conjunction) { - const int var = PositiveRef(literal); - if (!hint_has_value_[var]) { - all_have_hint = false; - break; - } - if (hint_[var] == (RefIsPositive(literal) ? 0 : 1)) { - new_hint = 0; - break; - } + if (!solution_is_loaded_) return; + int new_value = 1; + bool all_have_value = true; + for (const int literal : conjunction) { + const int var = PositiveRef(literal); + if (!HasValue(var)) { + all_have_value = false; + break; } - // Leave the `new_var` hint unassigned if any literal is not hinted. - if (all_have_hint) { - hint_has_value_[new_var] = true; - hint_[new_var] = new_hint; + if (GetVarValue(var) == (RefIsPositive(literal) ? 0 : 1)) { + new_value = 0; + break; } } + // Leave the `new_var` unassigned if any literal is unassigned. + if (all_have_value) { + SetVarValue(new_var, new_value); + } } void SolutionCrush::SetVarToValueIfLinearConstraintViolated( int new_var, int64_t value, absl::Span> linear, const Domain& domain) { - if (hint_is_loaded_) { - int64_t linear_value = 0; - bool all_have_hint = true; - for (const auto [var, coeff] : linear) { - if (!hint_has_value_[var]) { - all_have_hint = false; - break; - } - linear_value += hint_[var] * coeff; - } - if (all_have_hint && !domain.Contains(linear_value)) { - hint_has_value_[new_var] = true; - hint_[new_var] = value; + if (!solution_is_loaded_) return; + int64_t linear_value = 0; + bool all_have_value = true; + for (const auto [var, coeff] : linear) { + if (!HasValue(var)) { + all_have_value = false; + break; } + linear_value += GetVarValue(var) * coeff; + } + if (all_have_value && !domain.Contains(linear_value)) { + SetVarValue(new_var, value); } } @@ -182,12 +172,12 @@ void SolutionCrush::SetVarToValueIf(int var, int64_t value, int condition_lit) { void SolutionCrush::SetVarToLinearExpressionIf( int var, const LinearExpressionProto& expr, int condition_lit) { - if (!hint_is_loaded_) return; - if (!VarHasSolutionHint(PositiveRef(condition_lit))) return; - if (!LiteralSolutionHint(condition_lit)) return; - const std::optional expr_value = GetExpressionSolutionHint(expr); + if (!solution_is_loaded_) return; + if (!HasValue(PositiveRef(condition_lit))) return; + if (!GetLiteralValue(condition_lit)) return; + const std::optional expr_value = GetExpressionValue(expr); if (expr_value.has_value()) { - SetVarHint(var, expr_value.value()); + SetVarValue(var, expr_value.value()); } } @@ -201,39 +191,34 @@ void SolutionCrush::SetLiteralToValueIf(int literal, bool value, void SolutionCrush::SetVarToConditionalValue( int var, absl::Span condition_lits, int64_t value_if_true, int64_t value_if_false) { - if (!hint_is_loaded_) return; + if (!solution_is_loaded_) return; bool condition_value = true; for (const int condition_lit : condition_lits) { - if (!VarHasSolutionHint(PositiveRef(condition_lit))) return; - if (!LiteralSolutionHint(condition_lit)) { + if (!HasValue(PositiveRef(condition_lit))) return; + if (!GetLiteralValue(condition_lit)) { condition_value = false; break; } } - SetVarHint(var, condition_value ? value_if_true : value_if_false); + SetVarValue(var, condition_value ? value_if_true : value_if_false); } void SolutionCrush::MakeLiteralsEqual(int lit1, int lit2) { - if (!hint_is_loaded_) return; - if (hint_has_value_[PositiveRef(lit2)]) { - SetLiteralHint(lit1, LiteralSolutionHint(lit2)); - } else if (hint_has_value_[PositiveRef(lit1)]) { - SetLiteralHint(lit2, LiteralSolutionHint(lit1)); + if (!solution_is_loaded_) return; + if (HasValue(PositiveRef(lit2))) { + SetLiteralValue(lit1, GetLiteralValue(lit2)); + } else if (HasValue(PositiveRef(lit1))) { + SetLiteralValue(lit2, GetLiteralValue(lit1)); } } -void SolutionCrush::UpdateVarToDomain(int var, const Domain& domain) { - if (VarHasSolutionHint(var)) { - UpdateVarSolutionHint(var, domain.ClosestValue(SolutionHint(var))); - } - -#ifdef CHECK_HINT - if (model_has_hint_ && hint_is_loaded_ && !domain.Contains(hint_[var])) { - LOG(FATAL) << "Hint with value " << hint_[var] - << " infeasible when changing domain of " << var << " to " - << domain; +void SolutionCrush::SetOrUpdateVarToDomain(int var, const Domain& domain) { + if (!solution_is_loaded_) return; + if (HasValue(var)) { + SetVarValue(var, domain.ClosestValue(GetVarValue(var))); + } else if (domain.IsFixed()) { + SetVarValue(var, domain.FixedValue()); } -#endif } void SolutionCrush::UpdateLiteralsToFalseIfDifferent(int lit1, int lit2) { @@ -248,19 +233,22 @@ void SolutionCrush::UpdateLiteralsToFalseIfDifferent(int lit1, int lit2) { } void SolutionCrush::UpdateLiteralsWithDominance(int lit, int dominating_lit) { - if (LiteralSolutionHintIs(lit, true) && - LiteralSolutionHintIs(dominating_lit, false)) { - UpdateLiteralSolutionHint(lit, false); - UpdateLiteralSolutionHint(dominating_lit, true); + if (!solution_is_loaded_) return; + if (!HasValue(PositiveRef(lit)) || !HasValue(PositiveRef(dominating_lit))) { + return; + } + if (GetLiteralValue(lit) && !GetLiteralValue(dominating_lit)) { + SetLiteralValue(lit, false); + SetLiteralValue(dominating_lit, true); } } void SolutionCrush::MaybeUpdateVarWithSymmetriesToValue( int var, bool value, absl::Span> generators) { - if (!hint_is_loaded_) return; - if (!VarHasSolutionHint(var)) return; - if (SolutionHint(var) == static_cast(value)) return; + if (!solution_is_loaded_) return; + if (!HasValue(var)) return; + if (GetVarValue(var) == static_cast(value)) return; std::vector schrier_vector; std::vector orbit; @@ -269,15 +257,14 @@ void SolutionCrush::MaybeUpdateVarWithSymmetriesToValue( bool found_target = false; int target_var; for (int v : orbit) { - if (VarHasSolutionHint(v) && - SolutionHint(v) == static_cast(value)) { + if (HasValue(v) && GetVarValue(v) == static_cast(value)) { found_target = true; target_var = v; break; } } if (!found_target) { - VLOG(1) << "Couldn't transform hint properly"; + VLOG(1) << "Couldn't transform solution properly"; return; } @@ -287,36 +274,37 @@ void SolutionCrush::MaybeUpdateVarWithSymmetriesToValue( PermuteVariables(*generators[i]); } - DCHECK(VarHasSolutionHint(var)); - DCHECK_EQ(SolutionHint(var), value); + DCHECK(HasValue(var)); + DCHECK_EQ(GetVarValue(var), value); } void SolutionCrush::UpdateRefsWithDominance( int ref, int64_t min_value, int64_t max_value, absl::Span> dominating_refs) { - const std::optional ref_hint = GetRefSolutionHint(ref); - if (!ref_hint.has_value()) return; - // This can happen if the solution hint is not initially feasible (in which + if (!solution_is_loaded_) return; + const std::optional ref_value = GetRefValue(ref); + if (!ref_value.has_value()) return; + // This can happen if the solution is not initially feasible (in which // case we can't fix it). - if (*ref_hint < min_value) return; - // If the solution hint is already in the new domain there is nothing to do. - if (*ref_hint <= max_value) return; - // The quantity to subtract from the solution hint of `ref`. - const int64_t ref_hint_delta = *ref_hint - max_value; - - UpdateRefSolutionHint(ref, *ref_hint - ref_hint_delta); - int64_t remaining_delta = ref_hint_delta; + if (*ref_value < min_value) return; + // If the value is already in the new domain there is nothing to do. + if (*ref_value <= max_value) return; + // The quantity to subtract from the value of `ref`. + const int64_t ref_value_delta = *ref_value - max_value; + + SetRefValue(ref, *ref_value - ref_value_delta); + int64_t remaining_delta = ref_value_delta; for (const auto& [dominating_ref, dominating_ref_domain] : dominating_refs) { - const std::optional dominating_ref_hint = - GetRefSolutionHint(dominating_ref); - if (!dominating_ref_hint.has_value()) continue; - const int64_t new_dominating_ref_hint = - dominating_ref_domain.ValueAtOrBefore(*dominating_ref_hint + + const std::optional dominating_ref_value = + GetRefValue(dominating_ref); + if (!dominating_ref_value.has_value()) continue; + const int64_t new_dominating_ref_value = + dominating_ref_domain.ValueAtOrBefore(*dominating_ref_value + remaining_delta); - // This might happen if the solution hint is not initially feasible. - if (!dominating_ref_domain.Contains(new_dominating_ref_hint)) continue; - UpdateRefSolutionHint(dominating_ref, new_dominating_ref_hint); - remaining_delta -= (new_dominating_ref_hint - *dominating_ref_hint); + // This might happen if the solution is not initially feasible. + if (!dominating_ref_domain.Contains(new_dominating_ref_value)) continue; + SetRefValue(dominating_ref, new_dominating_ref_value); + remaining_delta -= (new_dominating_ref_value - *dominating_ref_value); if (remaining_delta == 0) break; } } @@ -326,12 +314,12 @@ void SolutionCrush::SetVarToLinearConstraintSolution( absl::Span coeffs, int64_t rhs) { DCHECK_EQ(vars.size(), coeffs.size()); DCHECK(!var_index.has_value() || var_index.value() < vars.size()); - if (!hint_is_loaded_) return; + if (!solution_is_loaded_) return; int64_t term_value = rhs; for (int i = 0; i < vars.size(); ++i) { - if (VarHasSolutionHint(vars[i])) { + if (HasValue(vars[i])) { if (i != var_index) { - term_value -= SolutionHint(vars[i]) * coeffs[i]; + term_value -= GetVarValue(vars[i]) * coeffs[i]; } } else if (!var_index.has_value()) { var_index = i; @@ -340,13 +328,13 @@ void SolutionCrush::SetVarToLinearConstraintSolution( } } if (!var_index.has_value()) return; - SetVarHint(vars[var_index.value()], term_value / coeffs[var_index.value()]); + SetVarValue(vars[var_index.value()], term_value / coeffs[var_index.value()]); -#ifdef CHECK_HINT +#ifdef CHECK_CRUSH if (term_value % coeffs[var_index.value()] != 0) { std::stringstream lhs; for (int i = 0; i < vars.size(); ++i) { - lhs << (i == var_index ? "x" : std::to_string(SolutionHint(vars[i]))); + lhs << (i == var_index ? "x" : std::to_string(GetVarValue(vars[i]))); lhs << " * " << coeffs[i]; if (i < vars.size() - 1) lhs << " + "; } @@ -360,62 +348,63 @@ void SolutionCrush::SetReservoirCircuitVars( const ReservoirConstraintProto& reservoir, int64_t min_level, int64_t max_level, absl::Span level_vars, const CircuitConstraintProto& circuit) { - if (!hint_is_loaded_) return; - // The hints of the active events, in the order they should appear in the - // circuit. The hints are collected first, and sorted later. - struct ReservoirEventHint { + if (!solution_is_loaded_) return; + // The values of the active events, in the order they should appear in the + // circuit. The values are collected first, and sorted later. + struct ReservoirEventValues { int index; // In the reservoir constraint. int64_t time; int64_t level_change; }; const int num_events = reservoir.time_exprs_size(); - std::vector active_event_hints; + std::vector active_event_values; for (int i = 0; i < num_events; ++i) { - if (!VarHasSolutionHint(PositiveRef(reservoir.active_literals(i)))) return; - if (LiteralSolutionHint(reservoir.active_literals(i))) { - const std::optional time_hint = - GetExpressionSolutionHint(reservoir.time_exprs(i)); - const std::optional change_hint = - GetExpressionSolutionHint(reservoir.level_changes(i)); - if (!time_hint.has_value() || !change_hint.has_value()) return; - active_event_hints.push_back({i, time_hint.value(), change_hint.value()}); + if (!HasValue(PositiveRef(reservoir.active_literals(i)))) return; + if (GetLiteralValue(reservoir.active_literals(i))) { + const std::optional time_value = + GetExpressionValue(reservoir.time_exprs(i)); + const std::optional change_value = + GetExpressionValue(reservoir.level_changes(i)); + if (!time_value.has_value() || !change_value.has_value()) return; + active_event_values.push_back( + {i, time_value.value(), change_value.value()}); } } - // Update the `level_vars` hints by computing the level at each active event. - std::sort(active_event_hints.begin(), active_event_hints.end(), - [](const ReservoirEventHint& a, const ReservoirEventHint& b) { + // Update the `level_vars` values by computing the level at each active event. + std::sort(active_event_values.begin(), active_event_values.end(), + [](const ReservoirEventValues& a, const ReservoirEventValues& b) { return a.time < b.time; }); int64_t current_level = 0; - for (int i = 0; i < active_event_hints.size(); ++i) { + for (int i = 0; i < active_event_values.size(); ++i) { int j = i; // Adjust the order of the events occurring at the same time, in the // circuit, so that, at each node, the level is between `var_min` and // `var_max`. For instance, if e1 = {t, +1} and e2 = {t, -1}, and if // `current_level` = 0, `var_min` = -1 and `var_max` = 0, then e2 must occur // before e1. - while (j < active_event_hints.size() && - active_event_hints[j].time == active_event_hints[i].time && - (current_level + active_event_hints[j].level_change < min_level || - current_level + active_event_hints[j].level_change > max_level)) { + while (j < active_event_values.size() && + active_event_values[j].time == active_event_values[i].time && + (current_level + active_event_values[j].level_change < min_level || + current_level + active_event_values[j].level_change > max_level)) { ++j; } - if (j < active_event_hints.size() && - active_event_hints[j].time == active_event_hints[i].time) { - if (i != j) std::swap(active_event_hints[i], active_event_hints[j]); - current_level += active_event_hints[i].level_change; - SetVarHint(level_vars[active_event_hints[i].index], current_level); + if (j < active_event_values.size() && + active_event_values[j].time == active_event_values[i].time) { + if (i != j) std::swap(active_event_values[i], active_event_values[j]); + current_level += active_event_values[i].level_change; + SetVarValue(level_vars[active_event_values[i].index], current_level); } else { return; } } - // The index of each event in `active_event_hints`, or -1 if the event's - // "active" hint is false. - std::vector active_event_hint_index(num_events, -1); - for (int i = 0; i < active_event_hints.size(); ++i) { - active_event_hint_index[active_event_hints[i].index] = i; + // The index of each event in `active_event_values`, or -1 if the event's + // "active" value is false. + std::vector active_event_value_index(num_events, -1); + for (int i = 0; i < active_event_values.size(); ++i) { + active_event_value_index[active_event_values[i].index] = i; } for (int i = 0; i < circuit.literals_size(); ++i) { const int head = circuit.heads(i); @@ -424,22 +413,22 @@ void SolutionCrush::SetReservoirCircuitVars( if (tail == num_events) { if (head == num_events) { // Self-arc on the start and end node. - SetLiteralHint(literal, active_event_hints.empty()); + SetLiteralValue(literal, active_event_values.empty()); } else { // Arc from the start node to an event node. - SetLiteralHint(literal, !active_event_hints.empty() && - active_event_hints.front().index == head); + SetLiteralValue(literal, !active_event_values.empty() && + active_event_values.front().index == head); } } else if (head == num_events) { // Arc from an event node to the end node. - SetLiteralHint(literal, !active_event_hints.empty() && - active_event_hints.back().index == tail); + SetLiteralValue(literal, !active_event_values.empty() && + active_event_values.back().index == tail); } else if (tail != head) { // Arc between two different event nodes. - const int tail_index = active_event_hint_index[tail]; - const int head_index = active_event_hint_index[head]; - SetLiteralHint(literal, tail_index != -1 && tail_index != -1 && - head_index == tail_index + 1); + const int tail_index = active_event_value_index[tail]; + const int head_index = active_event_value_index[head]; + SetLiteralValue(literal, tail_index != -1 && tail_index != -1 && + head_index == tail_index + 1); } } } @@ -447,19 +436,17 @@ void SolutionCrush::SetReservoirCircuitVars( void SolutionCrush::SetVarToReifiedPrecedenceLiteral( int var, const LinearExpressionProto& time_i, const LinearExpressionProto& time_j, int active_i, int active_j) { - // Take care of hints. - if (hint_is_loaded_) { - std::optional time_i_hint = GetExpressionSolutionHint(time_i); - std::optional time_j_hint = GetExpressionSolutionHint(time_j); - std::optional active_i_hint = GetRefSolutionHint(active_i); - std::optional active_j_hint = GetRefSolutionHint(active_j); - if (time_i_hint.has_value() && time_j_hint.has_value() && - active_i_hint.has_value() && active_j_hint.has_value()) { - const bool reified_hint = (active_i_hint.value() != 0) && - (active_j_hint.value() != 0) && - (time_i_hint.value() <= time_j_hint.value()); - SetNewVariableHint(var, reified_hint); - } + if (!solution_is_loaded_) return; + std::optional time_i_value = GetExpressionValue(time_i); + std::optional time_j_value = GetExpressionValue(time_j); + std::optional active_i_value = GetRefValue(active_i); + std::optional active_j_value = GetRefValue(active_j); + if (time_i_value.has_value() && time_j_value.has_value() && + active_i_value.has_value() && active_j_value.has_value()) { + const bool reified_value = (active_i_value.value() != 0) && + (active_j_value.value() != 0) && + (time_i_value.value() <= time_j_value.value()); + SetVarValue(var, reified_value); } } @@ -467,69 +454,69 @@ void SolutionCrush::SetIntModExpandedVars(const ConstraintProto& ct, int div_var, int prod_var, int64_t default_div_value, int64_t default_prod_value) { - if (!hint_is_loaded_) return; - bool enforced_hint = true; + if (!solution_is_loaded_) return; + bool enforced_value = true; for (const int lit : ct.enforcement_literal()) { - if (!VarHasSolutionHint(PositiveRef(lit))) return; - enforced_hint = enforced_hint && LiteralSolutionHint(lit); + if (!HasValue(PositiveRef(lit))) return; + enforced_value = enforced_value && GetLiteralValue(lit); } - if (!enforced_hint) { - SetVarHint(div_var, default_div_value); - SetVarHint(prod_var, default_prod_value); + if (!enforced_value) { + SetVarValue(div_var, default_div_value); + SetVarValue(prod_var, default_prod_value); return; } const LinearArgumentProto& int_mod = ct.int_mod(); - std::optional hint = GetExpressionSolutionHint(int_mod.exprs(0)); - if (!hint.has_value()) return; - const int64_t expr_hint = hint.value(); + std::optional v = GetExpressionValue(int_mod.exprs(0)); + if (!v.has_value()) return; + const int64_t expr_value = v.value(); - hint = GetExpressionSolutionHint(int_mod.exprs(1)); - if (!hint.has_value()) return; - const int64_t mod_expr_hint = hint.value(); + v = GetExpressionValue(int_mod.exprs(1)); + if (!v.has_value()) return; + const int64_t mod_expr_value = v.value(); - hint = GetExpressionSolutionHint(int_mod.target()); - if (!hint.has_value()) return; - const int64_t target_expr_hint = hint.value(); + v = GetExpressionValue(int_mod.target()); + if (!v.has_value()) return; + const int64_t target_expr_value = v.value(); - // target_expr_hint should be equal to "expr_hint % mod_expr_hint". - SetVarHint(div_var, expr_hint / mod_expr_hint); - SetVarHint(prod_var, expr_hint - target_expr_hint); + // target_expr_value should be equal to "expr_value % mod_expr_value". + SetVarValue(div_var, expr_value / mod_expr_value); + SetVarValue(prod_var, expr_value - target_expr_value); } void SolutionCrush::SetIntProdExpandedVars(const LinearArgumentProto& int_prod, absl::Span prod_vars) { DCHECK_EQ(int_prod.exprs_size(), prod_vars.size() + 2); - if (!hint_is_loaded_) return; - std::optional hint = GetExpressionSolutionHint(int_prod.exprs(0)); - if (!hint.has_value()) return; - int64_t last_prod_hint = hint.value(); + if (!solution_is_loaded_) return; + std::optional v = GetExpressionValue(int_prod.exprs(0)); + if (!v.has_value()) return; + int64_t last_prod_value = v.value(); for (int i = 1; i < int_prod.exprs_size() - 1; ++i) { - hint = GetExpressionSolutionHint(int_prod.exprs(i)); - if (!hint.has_value()) return; - last_prod_hint *= hint.value(); - SetVarHint(prod_vars[i - 1], last_prod_hint); + v = GetExpressionValue(int_prod.exprs(i)); + if (!v.has_value()) return; + last_prod_value *= v.value(); + SetVarValue(prod_vars[i - 1], last_prod_value); } } void SolutionCrush::SetLinMaxExpandedVars( const LinearArgumentProto& lin_max, absl::Span enforcement_lits) { - if (!hint_is_loaded_) return; + if (!solution_is_loaded_) return; DCHECK_EQ(enforcement_lits.size(), lin_max.exprs_size()); - const std::optional target_hint = - GetExpressionSolutionHint(lin_max.target()); - if (!target_hint.has_value()) return; - int enforcement_hint_sum = 0; + const std::optional target_value = + GetExpressionValue(lin_max.target()); + if (!target_value.has_value()) return; + int enforcement_value_sum = 0; for (int i = 0; i < enforcement_lits.size(); ++i) { - const std::optional expr_hint = - GetExpressionSolutionHint(lin_max.exprs(i)); - if (!expr_hint.has_value()) return; - if (enforcement_hint_sum == 0) { - const bool hint = target_hint.value() <= expr_hint.value(); - SetLiteralHint(enforcement_lits[i], hint); - enforcement_hint_sum += hint; + const std::optional expr_value = + GetExpressionValue(lin_max.exprs(i)); + if (!expr_value.has_value()) return; + if (enforcement_value_sum == 0) { + const bool enforcement_value = target_value.value() <= expr_value.value(); + SetLiteralValue(enforcement_lits[i], enforcement_value); + enforcement_value_sum += enforcement_value; } else { - SetLiteralHint(enforcement_lits[i], false); + SetLiteralValue(enforcement_lits[i], false); } } } @@ -538,90 +525,101 @@ void SolutionCrush::SetAutomatonExpandedVars( const AutomatonConstraintProto& automaton, absl::Span state_vars, absl::Span transition_vars) { - if (!hint_is_loaded_) return; + if (!solution_is_loaded_) return; absl::flat_hash_map, int64_t> transitions; for (int i = 0; i < automaton.transition_tail_size(); ++i) { transitions[{automaton.transition_tail(i), automaton.transition_label(i)}] = automaton.transition_head(i); } - std::vector label_hints; - std::vector state_hints; + std::vector label_values; + std::vector state_values; int64_t current_state = automaton.starting_state(); - state_hints.push_back(current_state); + state_values.push_back(current_state); for (int i = 0; i < automaton.exprs_size(); ++i) { - const std::optional label_hint = - GetExpressionSolutionHint(automaton.exprs(i)); - if (!label_hint.has_value()) return; - label_hints.push_back(label_hint.value()); + const std::optional label_value = + GetExpressionValue(automaton.exprs(i)); + if (!label_value.has_value()) return; + label_values.push_back(label_value.value()); - const auto it = transitions.find({current_state, label_hint.value()}); + const auto it = transitions.find({current_state, label_value.value()}); if (it == transitions.end()) return; current_state = it->second; - state_hints.push_back(current_state); + state_values.push_back(current_state); } for (const auto& [var, time, state] : state_vars) { - SetVarHint(var, state_hints[time] == state); + SetVarValue(var, state_values[time] == state); } for (const auto& [var, time, transition_tail, transition_label] : transition_vars) { - SetVarHint(var, state_hints[time] == transition_tail && - label_hints[time] == transition_label); + SetVarValue(var, state_values[time] == transition_tail && + label_values[time] == transition_label); } } void SolutionCrush::SetTableExpandedVars( absl::Span column_vars, absl::Span existing_row_lits, absl::Span new_row_lits) { - if (!hint_is_loaded_) return; - int hint_sum = 0; + if (!solution_is_loaded_) return; + int row_lit_values_sum = 0; for (const int lit : existing_row_lits) { - if (!VarHasSolutionHint(PositiveRef(lit))) return; - hint_sum += LiteralSolutionHint(lit); + if (!HasValue(PositiveRef(lit))) return; + row_lit_values_sum += GetLiteralValue(lit); } const int num_vars = column_vars.size(); for (const auto& [lit, var_values] : new_row_lits) { - if (hint_sum >= 1) { - SetLiteralHint(lit, false); + if (row_lit_values_sum >= 1) { + SetLiteralValue(lit, false); continue; } - bool row_hint = true; + bool row_lit_value = true; for (int var_index = 0; var_index < num_vars; ++var_index) { const auto& values = var_values[var_index]; if (!values.empty() && std::find(values.begin(), values.end(), - SolutionHint(column_vars[var_index])) == values.end()) { - row_hint = false; + GetVarValue(column_vars[var_index])) == values.end()) { + row_lit_value = false; break; } } - SetLiteralHint(lit, row_hint); - hint_sum += row_hint; + SetLiteralValue(lit, row_lit_value); + row_lit_values_sum += row_lit_value; } } void SolutionCrush::SetLinearWithComplexDomainExpandedVars( const LinearConstraintProto& linear, absl::Span bucket_lits) { - if (!hint_is_loaded_) return; - int64_t expr_hint = 0; + if (!solution_is_loaded_) return; + int64_t expr_value = 0; for (int i = 0; i < linear.vars_size(); ++i) { const int var = linear.vars(i); - if (!VarHasSolutionHint(var)) return; - expr_hint += linear.coeffs(i) * hint_[var]; + if (!HasValue(var)) return; + expr_value += linear.coeffs(i) * GetVarValue(var); } DCHECK_LE(bucket_lits.size(), linear.domain_size() / 2); for (int i = 0; i < bucket_lits.size(); ++i) { const int64_t lb = linear.domain(2 * i); const int64_t ub = linear.domain(2 * i + 1); - SetLiteralHint(bucket_lits[i], expr_hint >= lb && expr_hint <= ub); + SetLiteralValue(bucket_lits[i], expr_value >= lb && expr_value <= ub); + } +} + +void SolutionCrush::StoreSolutionAsHint(CpModelProto& model) const { + if (!solution_is_loaded_) return; + model.clear_solution_hint(); + for (int i = 0; i < var_values_.size(); ++i) { + if (var_has_value_[i]) { + model.mutable_solution_hint()->add_vars(i); + model.mutable_solution_hint()->add_values(var_values_[i]); + } } } void SolutionCrush::PermuteVariables(const SparsePermutation& permutation) { - CHECK(hint_is_loaded_); - permutation.ApplyToDenseCollection(hint_); - permutation.ApplyToDenseCollection(hint_has_value_); + CHECK(solution_is_loaded_); + permutation.ApplyToDenseCollection(var_has_value_); + permutation.ApplyToDenseCollection(var_values_); } } // namespace sat diff --git a/ortools/sat/solution_crush.h b/ortools/sat/solution_crush.h index cf0abf9c92..f85511074d 100644 --- a/ortools/sat/solution_crush.h +++ b/ortools/sat/solution_crush.h @@ -22,15 +22,31 @@ #include "absl/container/flat_hash_map.h" #include "absl/container/inlined_vector.h" -#include "absl/log/check.h" #include "absl/types/span.h" #include "ortools/algorithms/sparse_permutation.h" +#include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_utils.h" #include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { +// Transforms (or "crushes") solutions of the initial model into solutions of +// the presolved model. +// +// Note that partial solution crushing is not a priority: as of Jan 2025, most +// methods of this class do nothing if some solution values are missing to +// perform their work. If one just want to complete a partial solution to a full +// one for convenience, it should be relatively easy to first solve a +// feasibility model where all hinted variables are fixed, and use the solution +// to that problem as a starting hint. +// +// Note also that if the initial "solution" is incomplete or infeasible, the +// crushed "solution" might contain values outside of the domain of their +// variables. Consider for instance two constraints "b => v=1" and "!b => v=2", +// presolved into "v = b+1", with SetVarToLinearConstraintSolution called to set +// b's value from v's value. If the initial solution is infeasible, with v=0, +// this will set b to -1, which is outside of its [0,1] domain. class SolutionCrush { public: SolutionCrush() = default; @@ -41,6 +57,17 @@ class SolutionCrush { SolutionCrush& operator=(const SolutionCrush&) = delete; SolutionCrush& operator=(SolutionCrush&&) = delete; + bool SolutionIsLoaded() const { return solution_is_loaded_; } + + // Visible for testing. + absl::Span GetVarValues() const { return var_values_; } + + // Sets the given values in the solution. `solution` must be a map from + // variable indices to variable values. This must be called only once, before + // any other method. + void LoadSolution(int num_vars, + const absl::flat_hash_map& solution); + // Resizes the solution to contain `new_size` variables. Does not change the // value of existing variables, and does not set any value for the new // variables. @@ -48,99 +75,22 @@ class SolutionCrush { // the value of a new variable with one of them, call this method first. void Resize(int new_size); - // Sets the given values in the solution. `solution` must be a map from - // variable indices to variable values. This must be called only once, before - // any other method (besides `Resize`). - // TODO(user): revisit this near the end of the refactoring. - void LoadSolution(const absl::flat_hash_map& solution); - - // Solution hint accessors. - bool VarHasSolutionHint(int var) const { return hint_has_value_[var]; } - int64_t SolutionHint(int var) const { return hint_[var]; } - bool HintIsLoaded() const { return hint_is_loaded_; } - absl::Span SolutionHint() const { return hint_; } - - // Similar to SolutionHint() but make sure the value is within the given - // domain. - int64_t ClampedSolutionHint(int var, const Domain& domain) { - int64_t value = hint_[var]; - if (value > domain.Max()) { - value = domain.Max(); - } else if (value < domain.Min()) { - value = domain.Min(); - } - return value; - } - - bool LiteralSolutionHint(int lit) const { - const int var = PositiveRef(lit); - return RefIsPositive(lit) ? hint_[var] : !hint_[var]; - } - - bool LiteralSolutionHintIs(int lit, bool value) const { - const int var = PositiveRef(lit); - return hint_is_loaded_ && hint_has_value_[var] && - hint_[var] == (RefIsPositive(lit) ? value : !value); - } - - // If the given literal is already hinted, updates its hint. - // Otherwise do nothing. - void UpdateLiteralSolutionHint(int lit, bool value) { - UpdateVarSolutionHint(PositiveRef(lit), - RefIsPositive(lit) == value ? 1 : 0); - } - - std::optional GetRefSolutionHint(int ref) { - const int var = PositiveRef(ref); - if (!VarHasSolutionHint(var)) return std::nullopt; - const int64_t var_hint = SolutionHint(var); - return RefIsPositive(ref) ? var_hint : -var_hint; - } - - std::optional GetExpressionSolutionHint( - const LinearExpressionProto& expr) { - int64_t result = expr.offset(); - for (int i = 0; i < expr.vars().size(); ++i) { - if (expr.coeffs(i) == 0) continue; - if (!VarHasSolutionHint(expr.vars(i))) return std::nullopt; - result += expr.coeffs(i) * SolutionHint(expr.vars(i)); - } - return result; - } - - void UpdateRefSolutionHint(int ref, int hint) { - UpdateVarSolutionHint(PositiveRef(ref), RefIsPositive(ref) ? hint : -hint); - } - - // If the given variable is already hinted, updates its hint value. - // Otherwise, do nothing. - void UpdateVarSolutionHint(int var, int64_t value) { - DCHECK(RefIsPositive(var)); - if (!hint_is_loaded_) return; - if (!hint_has_value_[var]) return; - hint_[var] = value; - } - - // Allows to set the hint of a newly created variable. - void SetNewVariableHint(int var, int64_t value) { - CHECK(hint_is_loaded_); - CHECK(!hint_has_value_[var]); - SetVarHint(var, value); - } - // Sets the value of `literal` to "`var`'s value == `value`". Does nothing if // `literal` already has a value. void MaybeSetLiteralToValueEncoding(int literal, int var, int64_t value); - // Sets the value of `var` to the value of the given linear expression. - // `linear` must be a list of (variable index, coefficient) pairs. + // Sets the value of `var` to the value of the given linear expression, if all + // the variables in this expression have a value. `linear` must be a list of + // (variable index, coefficient) pairs. void SetVarToLinearExpression( - int var, absl::Span> linear); + int var, absl::Span> linear, + int64_t offset = 0); // Sets the value of `var` to the value of the given linear expression. // The two spans must have the same size. void SetVarToLinearExpression(int var, absl::Span vars, - absl::Span coeffs); + absl::Span coeffs, + int64_t offset = 0); // Sets the value of `var` to 1 if the value of at least one literal in // `clause` is equal to 1 (or to 0 otherwise). `clause` must be a list of @@ -188,10 +138,10 @@ class SolutionCrush { // value, sets the value of `lit1` to the value of `lit2`. void MakeLiteralsEqual(int lit1, int lit2); - // Updates the value of the given variable to be within the given domain. The - // variable is updated to the closest value within the domain. `var` must - // already have a value. - void UpdateVarToDomain(int var, const Domain& domain); + // If `var` already has a value, updates it to be within the given domain. + // Otherwise, if the domain is fixed, sets the value of `var` to this fixed + // value. Otherwise does nothing. + void SetOrUpdateVarToDomain(int var, const Domain& domain); // Updates the value of the given literals to false if their current values // are different (or does nothing otherwise). @@ -325,24 +275,55 @@ class SolutionCrush { void SetLinearWithComplexDomainExpandedVars( const LinearConstraintProto& linear, absl::Span bucket_lits); + // Stores the solution as a hint in the given model. + void StoreSolutionAsHint(CpModelProto& model) const; + private: - void SetVarHint(int var, int64_t value) { - hint_has_value_[var] = true; - hint_[var] = value; + bool HasValue(int var) const { return var_has_value_[var]; } + + int64_t GetVarValue(int var) const { return var_values_[var]; } + + bool GetLiteralValue(int lit) const { + const int var = PositiveRef(lit); + return RefIsPositive(lit) ? GetVarValue(var) : !GetVarValue(var); + } + + std::optional GetRefValue(int ref) const { + const int var = PositiveRef(ref); + if (!HasValue(var)) return std::nullopt; + return RefIsPositive(ref) ? GetVarValue(var) : -GetVarValue(var); + } + + std::optional GetExpressionValue( + const LinearExpressionProto& expr) const { + int64_t result = expr.offset(); + for (int i = 0; i < expr.vars().size(); ++i) { + if (expr.coeffs(i) == 0) continue; + if (!HasValue(expr.vars(i))) return std::nullopt; + result += expr.coeffs(i) * GetVarValue(expr.vars(i)); + } + return result; + } + + void SetVarValue(int var, int64_t value) { + var_has_value_[var] = true; + var_values_[var] = value; + } + + void SetLiteralValue(int lit, bool value) { + SetVarValue(PositiveRef(lit), RefIsPositive(lit) == value ? 1 : 0); } - void SetLiteralHint(int lit, bool value) { - SetVarHint(PositiveRef(lit), RefIsPositive(lit) == value ? 1 : 0); + void SetRefValue(int ref, int value) { + SetVarValue(PositiveRef(ref), RefIsPositive(ref) ? value : -value); } void PermuteVariables(const SparsePermutation& permutation); - // This contains all the hinted value or zero if the hint wasn't specified. - // We try to maintain this as we create new variable. - bool model_has_hint_ = false; - bool hint_is_loaded_ = false; - std::vector hint_has_value_; - std::vector hint_; + bool solution_is_loaded_ = false; + std::vector var_has_value_; + // This contains all the solution values or zero if a solution is not loaded. + std::vector var_values_; }; } // namespace sat diff --git a/ortools/sat/var_domination.cc b/ortools/sat/var_domination.cc index 243b8a08ab..e6a4da6c89 100644 --- a/ortools/sat/var_domination.cc +++ b/ortools/sat/var_domination.cc @@ -736,7 +736,7 @@ bool DualBoundStrengthening::Strengthen(PresolveContext* context) { const int64_t ub_limit = std::max(lb, CanFreelyDecreaseUntil(var)); if (ub_limit == lb) { ++num_fixed_vars; - CHECK(context->IntersectDomainWithAndUpdateHint(var, Domain(lb))); + CHECK(context->IntersectDomainWith(var, Domain(lb))); continue; } @@ -746,7 +746,7 @@ bool DualBoundStrengthening::Strengthen(PresolveContext* context) { std::min(ub, -CanFreelyDecreaseUntil(NegatedRef(var))); if (lb_limit == ub) { ++num_fixed_vars; - CHECK(context->IntersectDomainWithAndUpdateHint(var, Domain(ub))); + CHECK(context->IntersectDomainWith(var, Domain(ub))); continue; } @@ -764,7 +764,7 @@ bool DualBoundStrengthening::Strengthen(PresolveContext* context) { } ++num_fixed_vars; context->UpdateRuleStats("dual: fix variable with multiple choices"); - CHECK(context->IntersectDomainWithAndUpdateHint(var, Domain(value))); + CHECK(context->IntersectDomainWith(var, Domain(value))); continue; } } @@ -787,8 +787,7 @@ bool DualBoundStrengthening::Strengthen(PresolveContext* context) { .Max() : lb; context->UpdateRuleStats("dual: reduced domain"); - CHECK(context->IntersectDomainWithAndUpdateHint(var, - Domain(new_lb, new_ub))); + CHECK(context->IntersectDomainWith(var, Domain(new_lb, new_ub))); } } if (num_fixed_vars > 0) { @@ -853,9 +852,8 @@ bool DualBoundStrengthening::Strengthen(PresolveContext* context) { context->deductions.ImpliedDomain(enf, positive_ref)); if (implied.IsEmpty()) { context->UpdateRuleStats("dual: fix variable"); - if (!context->SetLiteralAndHintToFalse(enf)) return false; - if (!context->IntersectDomainWithAndUpdateHint(positive_ref, - Domain(bound))) { + if (!context->SetLiteralToFalse(enf)) return false; + if (!context->IntersectDomainWith(positive_ref, Domain(bound))) { return false; } continue; @@ -864,8 +862,7 @@ bool DualBoundStrengthening::Strengthen(PresolveContext* context) { // Corner case. if (implied.FixedValue() == bound) { context->UpdateRuleStats("dual: fix variable"); - if (!context->IntersectDomainWithAndUpdateHint(positive_ref, - implied)) { + if (!context->IntersectDomainWith(positive_ref, implied)) { return false; } continue; @@ -935,7 +932,7 @@ bool DualBoundStrengthening::Strengthen(PresolveContext* context) { .IntersectionWith(var_domain); if (rhs.IsEmpty()) { context->UpdateRuleStats("linear1: infeasible"); - if (!context->SetLiteralAndHintToFalse(ct.enforcement_literal(0))) { + if (!context->SetLiteralToFalse(ct.enforcement_literal(0))) { return false; } processed[PositiveRef(ref)] = true; @@ -1069,7 +1066,7 @@ bool DualBoundStrengthening::Strengthen(PresolveContext* context) { if (ref == NegatedRef(other_ref)) { context->UpdateRuleStats( "dual: detected l => ct and not(l) => ct with unused l!"); - if (!context->IntersectDomainWithAndUpdateHint(ref, Domain(0))) { + if (!context->IntersectDomainWith(ref, Domain(0))) { return false; } continue; diff --git a/ortools/sat/var_domination_test.cc b/ortools/sat/var_domination_test.cc index cfeb0dda34..543d9729b0 100644 --- a/ortools/sat/var_domination_test.cc +++ b/ortools/sat/var_domination_test.cc @@ -229,8 +229,8 @@ TEST(VarDominationTest, ExploitDominanceOfImplicant) { EXPECT_THAT(var_dom.DominatingVariables(X), ElementsAre(NegationOf(Y))); EXPECT_EQ(context.DomainOf(0).ToString(), "[0]"); EXPECT_EQ(context.DomainOf(1).ToString(), "[0]"); - EXPECT_EQ(context.solution_crush().SolutionHint(0), 0); - EXPECT_EQ(context.solution_crush().SolutionHint(1), 0); + EXPECT_EQ(context.solution_crush().GetVarValues()[0], 0); + EXPECT_EQ(context.solution_crush().GetVarValues()[1], 0); } // 2X - Y >= 0 @@ -278,8 +278,8 @@ TEST(VarDominationTest, ExploitDominanceOfNegatedImplicand) { EXPECT_THAT(var_dom.DominatingVariables(NegationOf(X)), ElementsAre(Y)); EXPECT_EQ(context.DomainOf(0).ToString(), "[1]"); EXPECT_EQ(context.DomainOf(1).ToString(), "[1]"); - EXPECT_EQ(context.solution_crush().SolutionHint(0), 1); - EXPECT_EQ(context.solution_crush().SolutionHint(1), 1); + EXPECT_EQ(context.solution_crush().GetVarValues()[0], 1); + EXPECT_EQ(context.solution_crush().GetVarValues()[1], 1); } // X + 2Y >= 0 @@ -324,8 +324,8 @@ TEST(VarDominationTest, ExploitDominanceInExactlyOne) { EXPECT_THAT(var_dom.DominatingVariables(X), ElementsAre(Y)); EXPECT_EQ(context.DomainOf(0).ToString(), "[0]"); EXPECT_EQ(context.DomainOf(1).ToString(), "[0,1]"); - EXPECT_EQ(context.solution_crush().SolutionHint(0), 0); - EXPECT_EQ(context.solution_crush().SolutionHint(1), 1); + EXPECT_EQ(context.solution_crush().GetVarValues()[0], 0); + EXPECT_EQ(context.solution_crush().GetVarValues()[1], 1); } // Objective: min(X + Y + 2Z) @@ -380,9 +380,9 @@ TEST(VarDominationTest, ExploitDominanceWithIntegerVariables) { EXPECT_EQ(context.DomainOf(0).ToString(), "[-5]"); EXPECT_EQ(context.DomainOf(1).ToString(), "[0,10]"); EXPECT_EQ(context.DomainOf(2).ToString(), "[5]"); - EXPECT_EQ(context.solution_crush().SolutionHint(0), -5); - EXPECT_EQ(context.solution_crush().SolutionHint(1), 10); - EXPECT_EQ(context.solution_crush().SolutionHint(2), 5); + EXPECT_EQ(context.solution_crush().GetVarValues()[0], -5); + EXPECT_EQ(context.solution_crush().GetVarValues()[1], 10); + EXPECT_EQ(context.solution_crush().GetVarValues()[2], 5); } // Objective: min(X + 2Y) @@ -429,8 +429,8 @@ TEST(VarDominationTest, ExploitRemainingDominance) { EqualsProto(expected_constraint_proto)); EXPECT_EQ(context.DomainOf(0).ToString(), "[0,1]"); EXPECT_EQ(context.DomainOf(1).ToString(), "[0,1]"); - EXPECT_EQ(context.solution_crush().SolutionHint(0), 1); - EXPECT_EQ(context.solution_crush().SolutionHint(1), 0); + EXPECT_EQ(context.solution_crush().GetVarValues()[0], 1); + EXPECT_EQ(context.solution_crush().GetVarValues()[1], 0); } // Objective: min(X) @@ -492,9 +492,9 @@ TEST(VarDominationTest, ExploitRemainingDominanceWithIntegerVariables) { EXPECT_EQ(context.DomainOf(0).ToString(), "[-10,-5]"); EXPECT_EQ(context.DomainOf(1).ToString(), "[5,10]"); EXPECT_EQ(context.DomainOf(2).ToString(), "[5]"); - EXPECT_EQ(context.solution_crush().SolutionHint(0), -5); - EXPECT_EQ(context.solution_crush().SolutionHint(1), 6); - EXPECT_EQ(context.solution_crush().SolutionHint(2), 5); + EXPECT_EQ(context.solution_crush().GetVarValues()[0], -5); + EXPECT_EQ(context.solution_crush().GetVarValues()[1], 6); + EXPECT_EQ(context.solution_crush().GetVarValues()[2], 5); } // X + Y + Z = 0 @@ -835,8 +835,8 @@ TEST(DualBoundReductionTest, FixVariableToDomainBound) { EXPECT_EQ(context.DomainOf(0).ToString(), "[-10]"); EXPECT_EQ(context.DomainOf(1).ToString(), "[10]"); - EXPECT_EQ(context.solution_crush().SolutionHint(0), -10); - EXPECT_EQ(context.solution_crush().SolutionHint(1), 10); + EXPECT_EQ(context.solution_crush().GetVarValues()[0], -10); + EXPECT_EQ(context.solution_crush().GetVarValues()[1], 10); } // Bound propagation see nothing, but if we can remove feasible solution, from @@ -874,9 +874,9 @@ TEST(DualBoundReductionTest, BasicTest) { EXPECT_EQ(context.DomainOf(0).ToString(), "[0]"); EXPECT_EQ(context.DomainOf(1).ToString(), "[0]"); EXPECT_EQ(context.DomainOf(2).ToString(), "[0]"); - EXPECT_EQ(context.solution_crush().SolutionHint(0), 0); - EXPECT_EQ(context.solution_crush().SolutionHint(1), 0); - EXPECT_EQ(context.solution_crush().SolutionHint(2), 0); + EXPECT_EQ(context.solution_crush().GetVarValues()[0], 0); + EXPECT_EQ(context.solution_crush().GetVarValues()[1], 0); + EXPECT_EQ(context.solution_crush().GetVarValues()[2], 0); } TEST(DualBoundReductionTest, CarefulWithHoles) { @@ -938,9 +938,9 @@ TEST(DualBoundReductionTest, Choices) { EXPECT_EQ(context.DomainOf(0).ToString(), "[0]"); EXPECT_EQ(context.DomainOf(1).ToString(), "[-2]"); EXPECT_EQ(context.DomainOf(2).ToString(), "[2]"); - EXPECT_EQ(context.solution_crush().SolutionHint(0), 0); - EXPECT_EQ(context.solution_crush().SolutionHint(1), -2); - EXPECT_EQ(context.solution_crush().SolutionHint(2), 2); + EXPECT_EQ(context.solution_crush().GetVarValues()[0], 0); + EXPECT_EQ(context.solution_crush().GetVarValues()[1], -2); + EXPECT_EQ(context.solution_crush().GetVarValues()[2], 2); } TEST(DualBoundReductionTest, AddImplication) { @@ -987,9 +987,9 @@ TEST(DualBoundReductionTest, AddImplication) { EXPECT_EQ(context.DomainOf(0).ToString(), "[0]"); EXPECT_EQ(context.DomainOf(1).ToString(), "[0,1]"); EXPECT_EQ(context.DomainOf(2).ToString(), "[0,1]"); - EXPECT_EQ(context.solution_crush().SolutionHint(0), 0); - EXPECT_EQ(context.solution_crush().SolutionHint(1), 0); - EXPECT_EQ(context.solution_crush().SolutionHint(2), 0); + EXPECT_EQ(context.solution_crush().GetVarValues()[0], 0); + EXPECT_EQ(context.solution_crush().GetVarValues()[1], 0); + EXPECT_EQ(context.solution_crush().GetVarValues()[2], 0); } TEST(DualBoundReductionTest, EquivalenceDetection) { @@ -1035,7 +1035,7 @@ TEST(DualBoundReductionTest, EquivalenceDetection) { EXPECT_EQ(context.DomainOf(2).ToString(), "[0,1]"); // Equivalence between a and b. EXPECT_EQ(context.GetLiteralRepresentative(1), 0); - EXPECT_TRUE(context.solution_crush().LiteralSolutionHint(0)); + EXPECT_EQ(context.solution_crush().GetVarValues()[0], 1); } } // namespace