From 8d3645a6cdc9462aa29d67d7d96a8a973875ce54 Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Wed, 7 Jan 2026 13:01:43 +0100 Subject: [PATCH] [CP-SAT] fix vivification bug; more work on encodings --- ortools/sat/BUILD.bazel | 28 ++ ortools/sat/clause.cc | 15 +- ortools/sat/clause.h | 8 +- ortools/sat/cp_model_presolve.cc | 342 +--------------- ortools/sat/cp_model_presolve_test.cc | 6 +- ortools/sat/cp_model_solver.cc | 6 +- ortools/sat/integer_base.cc | 17 - ortools/sat/integer_base.h | 5 - ortools/sat/integer_base_test.cc | 22 - ortools/sat/presolve_encoding.cc | 570 +++++++++++++++++++++++++- ortools/sat/presolve_encoding.h | 48 +++ ortools/sat/presolve_encoding_test.cc | 462 +++++++++++++++++++++ ortools/sat/sat_parameters.proto | 6 +- ortools/sat/stat_tables.cc | 6 +- ortools/sat/vivification.cc | 92 +++-- ortools/sat/vivification.h | 4 +- ortools/sat/work_assignment.cc | 9 +- ortools/util/logging.cc | 4 +- ortools/util/logging.h | 6 +- 19 files changed, 1224 insertions(+), 432 deletions(-) create mode 100644 ortools/sat/presolve_encoding_test.cc diff --git a/ortools/sat/BUILD.bazel b/ortools/sat/BUILD.bazel index d2e6fd6fff..5566b0410e 100644 --- a/ortools/sat/BUILD.bazel +++ b/ortools/sat/BUILD.bazel @@ -335,7 +335,9 @@ cc_library( "//ortools/util:time_limit", "@abseil-cpp//absl/algorithm:container", "@abseil-cpp//absl/base:core_headers", + "@abseil-cpp//absl/cleanup", "@abseil-cpp//absl/container:btree", + "@abseil-cpp//absl/log", "@abseil-cpp//absl/log:check", "@abseil-cpp//absl/types:span", ], @@ -393,8 +395,32 @@ cc_library( deps = [ ":cp_model_utils", ":presolve_context", + "//ortools/base:stl_util", + "//ortools/util:bitset", "//ortools/util:sorted_interval_list", + "@abseil-cpp//absl/algorithm:container", + "@abseil-cpp//absl/container:flat_hash_map", + "@abseil-cpp//absl/container:flat_hash_set", + "@abseil-cpp//absl/container:inlined_vector", "@abseil-cpp//absl/log", + "@abseil-cpp//absl/log:check", + "@protobuf", + ], +) + +cc_test( + name = "presolve_encoding_test", + srcs = ["presolve_encoding_test.cc"], + deps = [ + ":cp_model_cc_proto", + ":model", + ":presolve_context", + ":presolve_encoding", + "//ortools/base:gmock_main", + "//ortools/base:parse_test_proto", + "//ortools/util:sorted_interval_list", + "@abseil-cpp//absl/container:flat_hash_map", + "@abseil-cpp//absl/log:check", ], ) @@ -975,8 +1001,10 @@ cc_library( "//ortools/util:sigint", "//ortools/util:sorted_interval_list", "//ortools/util:strong_integers", + "//ortools/util:testing_utils", "//ortools/util:time_limit", "@abseil-cpp//absl/base:core_headers", + "@abseil-cpp//absl/base:log_severity", "@abseil-cpp//absl/cleanup", "@abseil-cpp//absl/container:btree", "@abseil-cpp//absl/container:flat_hash_map", diff --git a/ortools/sat/clause.cc b/ortools/sat/clause.cc index 7b1b47078e..e463b8e5df 100644 --- a/ortools/sat/clause.cc +++ b/ortools/sat/clause.cc @@ -529,7 +529,8 @@ bool ClauseManager::InprocessingRewriteClause( } const bool is_reason = ClauseIsUsedAsReason(clause); - CHECK(!is_reason || new_clause[0] == clause->PropagatedLiteral()); + CHECK(!is_reason || new_clause[0] == clause->PropagatedLiteral()) + << new_clause << " old " << clause->AsSpan(); if (new_clause.empty()) return false; // UNSAT. @@ -682,12 +683,24 @@ SatClause* ClauseManager::NextNewClauseToMinimize() { } SatClause* ClauseManager::NextClauseToMinimize() { + const int old = to_first_minimize_index_; for (; to_minimize_index_ < clauses_.size(); ++to_minimize_index_) { if (clauses_[to_minimize_index_]->IsRemoved()) continue; if (!IsRemovable(clauses_[to_minimize_index_])) { return clauses_[to_minimize_index_++]; } } + + // Lets reset and try once more to find one. + to_minimize_index_ = 0; + ++num_to_minimize_index_resets_; + for (; to_minimize_index_ < old; ++to_minimize_index_) { + if (clauses_[to_minimize_index_]->IsRemoved()) continue; + if (!IsRemovable(clauses_[to_minimize_index_])) { + return clauses_[to_minimize_index_++]; + } + } + return nullptr; } diff --git a/ortools/sat/clause.h b/ortools/sat/clause.h index d254e9ba28..5aab10b4a4 100644 --- a/ortools/sat/clause.h +++ b/ortools/sat/clause.h @@ -308,6 +308,7 @@ class ClauseManager : public SatPropagator { // Returns the next clause to minimize that has never been minimized before. // Note that we only minimize clauses kept forever. SatClause* NextNewClauseToMinimize(); + // Returns the next clause to minimize, this iterator will be reset to the // start so the clauses will be returned in round-robin order. // Note that we only minimize clauses kept forever. @@ -324,7 +325,10 @@ class ClauseManager : public SatPropagator { // Restart the scans. void ResetToProbeIndex() { to_probe_index_ = 0; } - void ResetToMinimizeIndex() { to_minimize_index_ = 0; } + int64_t NumToMinimizeIndexResets() const { + return num_to_minimize_index_resets_; + } + // Ensures that NextNewClauseToMinimize() returns only learned clauses. // This is a noop after the first call. void EnsureNewClauseIndexInitialized() { @@ -499,6 +503,8 @@ class ClauseManager : public SatPropagator { // TODO(user): If more indices are needed, switch to a generic API. int to_minimize_index_ = 0; + + int num_to_minimize_index_resets_ = 0; int to_first_minimize_index_ = 0; int to_probe_index_ = 0; diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index ae01a7177c..71e7510534 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/ortools/sat/cp_model_presolve.cc @@ -6815,7 +6815,8 @@ bool CpModelPresolver::PresolveNoOverlap2D(int /*c*/, ConstraintProto* ct) { IntegerValue(context_->EndMax(y))}); } CompactVectorVector no_overlaps; - absl::c_sort(indexed_intervals, IndexedInterval::ComparatorByStart()); + absl::c_stable_sort(indexed_intervals, + IndexedInterval::ComparatorByStart()); ConstructOverlappingSets(absl::MakeSpan(indexed_intervals), &no_overlaps); for (int i = 0; i < no_overlaps.size(); ++i) { ConstraintProto* new_ct = context_->working_model->add_constraints(); @@ -9431,341 +9432,18 @@ bool CpModelPresolver::MergeNoOverlap2DConstraints() { return true; } -namespace { -bool ConstraintIsEncodingBound(const ConstraintProto& ct) { - if (ct.constraint_case() != ConstraintProto::kLinear) return false; - if (ct.linear().vars_size() != 1) return false; - if (ct.linear().coeffs(0) != 1) return false; - if (ct.enforcement_literal_size() != 1) return false; - return true; -} -} // namespace - -// Return true if something changed. -bool CpModelPresolver::DetectEncodedComplexDomain( - PresolveContext* context, ConstraintProto* ct, - const Bitset64& pertinent_bools) { - if (context->ModelIsUnsat()) return false; - if (ct->constraint_case() != ConstraintProto::kAtMostOne && - ct->constraint_case() != ConstraintProto::kExactlyOne && - ct->constraint_case() != ConstraintProto::kBoolOr) { - return false; - } - - // Handling exaclty_one, at_most_one and bool_or is pretty similar. If we have - // l1 <=> v \in D1 - // l2 <=> v \in D2 - // - // We built - // l <=> v \in (D1 U D2). - // - // Moreover, if we have exactly_one(l1, l2, ...) or at_most_one(l1, l2, ...), - // we know that v cannot be in the intersection of D1 and D2. Thus, we first - // unconditionally remove (D1 ∩ D2) from the domain of v, making - // (l1=true and l2=true) impossible and allowing us to write our clauses as - // exactly_one(l1 or l2, ...) or at_most_one(l1 or l2, ...). - // - // Thus, other than the domain reduction that should not be done for the - // bool_or, all we need is to create a variable - // (l1 or l2) == l <=> (v \in (D1 U D2)). - google::protobuf::RepeatedField& literals = - ct->constraint_case() == ConstraintProto::kAtMostOne - ? *ct->mutable_at_most_one()->mutable_literals() - : (ct->constraint_case() == ConstraintProto::kExactlyOne - ? *ct->mutable_exactly_one()->mutable_literals() - : *ct->mutable_bool_or()->mutable_literals()); - if (literals.size() <= 1) return false; - - if (!ct->enforcement_literal().empty()) { - // TODO(user): support this case if it any problem needs it. - return false; - } - - struct Linear1Info { - int lit = -1; - int positive_linear1_ct = -1; - int negative_linear1_ct = -1; - }; - absl::flat_hash_map> var_to_linear1; - for (const int lit : literals) { - if (PositiveRef(lit) < pertinent_bools.size() && - !pertinent_bools[PositiveRef(lit)]) { - continue; - } - bool or_and_single_var_linear1 = true; - Linear1Info info; - int var = -1; - for (const int c : context->VarToConstraints(PositiveRef(lit))) { - if (c < 0) { - or_and_single_var_linear1 = false; - break; - } - const ConstraintProto& other_ct = context->working_model->constraints(c); - if (&other_ct == ct) continue; - if (!ConstraintIsEncodingBound(other_ct)) { - or_and_single_var_linear1 = false; - break; - } - if (other_ct.enforcement_literal(0) != lit && - other_ct.enforcement_literal(0) != NegatedRef(lit)) { - or_and_single_var_linear1 = false; - break; - } - if (var == -1) { - var = other_ct.linear().vars(0); - } else if (var != other_ct.linear().vars(0)) { - or_and_single_var_linear1 = false; - break; - } - info.lit = lit; - if (other_ct.enforcement_literal(0) == lit) { - info.positive_linear1_ct = c; - } else { - DCHECK_EQ(other_ct.enforcement_literal(0), NegatedRef(lit)); - info.negative_linear1_ct = c; - } - } - // When we have - // lit => var in D1 - // ~lit => var in D2 - // we can represent this on a line: - // - // ----------------D1---------------- - // ----------------D2--------------- - // |+++++++++++|*********************|++++++++++| - // lit=false lit unconstrained lit=true - // - // Handling the case where the variable is unconstrained by the lit is a - // bit of a pain: we want to replace two literals in a exactly_one by a - // single one, and if they are both unconstrained we might be forced to pick - // one arbitrarily to set to true. In any case, this is not a proper - // encoding of a complex domain, so we just ignore it. - // TODO(user): This can be implemented if it turns out to be common. - if (or_and_single_var_linear1 && info.negative_linear1_ct != -1 && - info.positive_linear1_ct != -1) { - const Domain domain_enforced_lit = ReadDomainFromProto( - context->working_model->constraints(info.positive_linear1_ct) - .linear()); - - // ~lit1 => var in domain_enforced_not_lit1 - const Domain domain_enforced_not_lit = ReadDomainFromProto( - context->working_model->constraints(info.negative_linear1_ct) - .linear()); - if (domain_enforced_lit.IntersectionWith(domain_enforced_not_lit) - .IsEmpty()) { - var_to_linear1[var].push_back(info); - } - } - } - // Ignore all variables that only appear once. - std::vector>> var_to_linear1_infos; - for (const auto& [var, linear1_infos] : var_to_linear1) { - if (linear1_infos.size() > 1) { - var_to_linear1_infos.push_back( - {var, std::vector(linear1_infos.begin(), - linear1_infos.end())}); - } - } - if (var_to_linear1_infos.empty()) return false; - - // We have some variables to simplify! Start by sorting to make the code - // deterministic. - absl::c_sort(var_to_linear1_infos, - [](const std::pair>& a, - const std::pair>& b) { - return a.first < b.first; - }); - // Doing the general code is rather complex, so we will just simplify one - // variable and two literals at a time, and leave for the presolve fixpoint - // to do the rest. - for (const auto& [var, infos] : var_to_linear1_infos) { - const Linear1Info& info1 = infos[0]; - const Linear1Info& info2 = infos[1]; - const int lit1 = info1.lit; - const int lit2 = info2.lit; - const Domain original_var_domain = context->DomainOf(var); - - DCHECK_NE(info1.positive_linear1_ct, -1); - DCHECK_NE(info2.positive_linear1_ct, -1); - DCHECK_NE(info1.negative_linear1_ct, -1); - DCHECK_NE(info2.negative_linear1_ct, -1); - - // lit1 => var in domain_enforced_lit1 - const Domain domain_enforced_lit1 = ReadDomainFromProto( - context->working_model->constraints(info1.positive_linear1_ct) - .linear()); - - // ~lit1 => var in domain_enforced_not_lit1 - const Domain domain_enforced_not_lit1 = ReadDomainFromProto( - context->working_model->constraints(info1.negative_linear1_ct) - .linear()); - - // lit2 => var in domain_enforced_lit2 - const Domain domain_enforced_lit2 = ReadDomainFromProto( - context->working_model->constraints(info2.positive_linear1_ct) - .linear()); - - // ~lit2 => var in domain_enforced_not_lit2 - const Domain domain_enforced_not_lit2 = ReadDomainFromProto( - context->working_model->constraints(info2.negative_linear1_ct) - .linear()); - - DCHECK(domain_enforced_lit1.IntersectionWith(domain_enforced_not_lit1) - .IsEmpty()); - DCHECK(domain_enforced_lit2.IntersectionWith(domain_enforced_not_lit2) - .IsEmpty()); - - // First, the variable must be in the domain of either the lit or of its - // negation. - if (!context->IntersectDomainWith( - var, domain_enforced_lit1.UnionWith(domain_enforced_not_lit1))) { - return true; - } - if (!context->IntersectDomainWith( - var, domain_enforced_lit2.UnionWith(domain_enforced_not_lit2))) { - return true; - } - - if (ct->constraint_case() != ConstraintProto::kBoolOr) { - // In virtue of the AMO, var must not be in the intersection of the two - // domains where both literals are true. - if (!context->IntersectDomainWith( - var, domain_enforced_lit2.IntersectionWith(domain_enforced_lit1) - .Complement())) { - return true; - } - } - const Domain domain_new_var_false = context->DomainOf(var).IntersectionWith( - domain_enforced_not_lit1.IntersectionWith(domain_enforced_not_lit2)); - const Domain domain_new_var_true = context->DomainOf(var).IntersectionWith( - domain_new_var_false.Complement()); - - // Now we want to build a lit3 = (lit1 or lit2) to use in the AMO/bool_or. - const int new_var = context->NewBoolVarWithClause({lit1, lit2}); - - if (domain_new_var_true.IsEmpty()) { - if (!context->SetLiteralToFalse(new_var)) return true; - } else if (domain_new_var_false.IsEmpty()) { - if (!context->SetLiteralToTrue(new_var)) return true; - } else { - ConstraintProto* new_ct = context->working_model->add_constraints(); - new_ct->add_enforcement_literal(new_var); - new_ct->mutable_linear()->add_vars(var); - new_ct->mutable_linear()->add_coeffs(1); - FillDomainInProto(domain_new_var_true, new_ct->mutable_linear()); - new_ct = context->working_model->add_constraints(); - new_ct->add_enforcement_literal(NegatedRef(new_var)); - new_ct->mutable_linear()->add_vars(var); - new_ct->mutable_linear()->add_coeffs(1); - FillDomainInProto(domain_new_var_false, new_ct->mutable_linear()); - } - - // Remove the two literals from the AMO. - int new_size = 0; - for (int i = 0; i < literals.size(); ++i) { - if (literals.Get(i) != lit1 && literals.Get(i) != lit2) { - literals.Set(new_size++, literals.Get(i)); - } - } - literals.Truncate(new_size); - literals.Add(new_var); - context->UpdateNewConstraintsVariableUsage(); - context->UpdateRuleStats( - "variables: detected encoding of a complex domain with multiple " - "linear1"); - } - return true; -} - void CpModelPresolver::DetectEncodedComplexDomains(PresolveContext* context) { PresolveTimer timer(__FUNCTION__, logger_, time_limit_); - // Constraints taking a list of literals that can, under some conditions, - // accept the following substitution: - // constraint(a, b, ...) => constraint(a | b, ...) - // one obvious case is bool_or. But if we can know that a and b cannot be - // both true, we can also apply this to at_most_one and exactly_one. - std::vector constraint_encoding_or; // bool_or, exactly_one, at_most_one + if (context->ModelIsUnsat()) return; + if (time_limit_->LimitReached()) return; - // To make sure this is not too slow, first do a pass to gather all linear1 - // constraints that shares the same variable with other three linear1. - absl::flat_hash_map> var_to_linear1; - for (int i = 0; i < context->working_model->constraints_size(); ++i) { - const ConstraintProto& ct = context->working_model->constraints(i); - if (ct.constraint_case() == ConstraintProto::kBoolOr || - ct.constraint_case() == ConstraintProto::kAtMostOne || - ct.constraint_case() == ConstraintProto::kExactlyOne) { - constraint_encoding_or.push_back(i); - continue; + std::vector local_models = + CreateVariableEncodingLocalModels(context); + for (VariableEncodingLocalModel& local_model : local_models) { + if (time_limit_->LimitReached()) return; + if (!DetectAllEncodedComplexDomain(context, local_model)) { + return; } - if (!ConstraintIsEncodingBound(ct)) { - continue; - } - var_to_linear1[ct.linear().vars(0)].push_back(i); - } - absl::erase_if(var_to_linear1, - [](const auto& p) { return p.second.size() <= 3; }); - // Now that we reduced cheaply our set of "interesting" linear1, let's use the - // variable->constraint graph to restrict it further. - for (auto& [var, linear1_cts] : var_to_linear1) { - int new_size = 0; - for (const int ct : linear1_cts) { - const int ref = - context->working_model->constraints(ct).enforcement_literal(0); - // We want to focus on literals that become removable once we undo the - // encoding, otherwise this whole step might just make the problem harder. - // So we want it to appear in two linear1 and a bool_or/amo/exactly_one. - if (context->VarToConstraints(PositiveRef(ref)).size() <= 3) { - linear1_cts[new_size++] = ct; - } - } - linear1_cts.resize(new_size); - } - absl::erase_if(var_to_linear1, - [](const auto& p) { return p.second.size() <= 3; }); - - if (var_to_linear1.empty()) return; - - // Now we use the linear1 we found to see which bool_or/amo/exactly_one could - // be applied to the heuristic. - Bitset64 booleans_potentially_encoding_domain( - context_->working_model->variables_size()); - for (const auto& [unused, linear1_cts] : var_to_linear1) { - for (const int ct : linear1_cts) { - booleans_potentially_encoding_domain.Set(PositiveRef( - context->working_model->constraints(ct).enforcement_literal(0))); - } - } - int new_encoding_or_count = 0; - for (int i = 0; i < constraint_encoding_or.size(); ++i) { - const int c = constraint_encoding_or[i]; - const ConstraintProto& ct = context->working_model->constraints(c); - const BoolArgumentProto& bool_ct = - ct.constraint_case() == ConstraintProto::kAtMostOne - ? ct.at_most_one() - : (ct.constraint_case() == ConstraintProto::kExactlyOne - ? ct.exactly_one() - : ct.bool_or()); - if (absl::c_count_if( - bool_ct.literals(), - [booleans_potentially_encoding_domain](int ref) { - return booleans_potentially_encoding_domain[PositiveRef(ref)]; - }) < 2) { - continue; - } - constraint_encoding_or[new_encoding_or_count++] = c; - } - constraint_encoding_or.resize(new_encoding_or_count); - - for (const int c : constraint_encoding_or) { - ConstraintProto* ct = context->working_model->mutable_constraints(c); - bool changed = false; - do { - changed = DetectEncodedComplexDomain( - context, ct, booleans_potentially_encoding_domain); - if (changed) { - context->UpdateConstraintVariableUsage(c); - } - } while (changed); } } diff --git a/ortools/sat/cp_model_presolve_test.cc b/ortools/sat/cp_model_presolve_test.cc index f086e60cc5..b3a3e72194 100644 --- a/ortools/sat/cp_model_presolve_test.cc +++ b/ortools/sat/cp_model_presolve_test.cc @@ -7859,9 +7859,11 @@ TEST(PresolveCpModelTest, DetectEncodingFromLinear) { params.set_keep_all_feasible_solutions_in_presolve(true); const CpModelProto presolved_model = PresolveForTest(initial_model, params); + IntegerVariableProto expected_proto; + FillDomainInProto(Domain::FromValues({3, 6, 9, 10, 12}), &expected_proto); // The values are 10, 10-1, 10-7, 10+2, and 10-4. - EXPECT_EQ(ReadDomainFromProto(presolved_model.variables(5)).ToString(), - "[3][6][9,10][12]"); + EXPECT_THAT(presolved_model.variables(), + testing::Contains(testing::EqualsProto(expected_proto))); } TEST(PresolveCpModelTest, ReplaceNonEqual) { diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index 0ab1659014..720ecfb1a3 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -31,6 +31,7 @@ #include #include +#include "absl/base/log_severity.h" #include "absl/base/thread_annotations.h" #include "absl/container/btree_map.h" #include "absl/container/btree_set.h" @@ -97,6 +98,7 @@ #include "ortools/util/random_engine.h" #include "ortools/util/sigint.h" #include "ortools/util/sorted_interval_list.h" +#include "ortools/util/testing_utils.h" #include "ortools/util/time_limit.h" ABSL_FLAG( @@ -2529,8 +2531,8 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) { } #endif // ORTOOLS_TARGET_OS_SUPPORTS_THREADS - if (DEBUG_MODE) { - LOG(WARNING) + if (DEBUG_MODE && !ProbablyRunningInsideUnitTest()) { + LOG_EVERY_N_SEC(WARNING, 0.1) << "WARNING: CP-SAT is running in debug mode. The solver will " "be slow because we will do a lot of extra checks. Compile in " "optimization mode to gain an order of magnitude speedup."; diff --git a/ortools/sat/integer_base.cc b/ortools/sat/integer_base.cc index 46d9996f0d..40eb284a97 100644 --- a/ortools/sat/integer_base.cc +++ b/ortools/sat/integer_base.cc @@ -238,23 +238,6 @@ RelationStatus BestBinaryRelationBounds::GetStatus(LinearExpression2 expr, return RelationStatus::IS_UNKNOWN; } -IntegerValue BestBinaryRelationBounds::GetUpperBound( - LinearExpression2 expr) const { - expr.SimpleCanonicalization(); - const IntegerValue gcd = expr.DivideByGcd(); - const bool negated = expr.NegateForCanonicalization(); - const auto it = best_bounds_.find(expr); - if (it != best_bounds_.end()) { - const auto [known_lb, known_ub] = it->second; - if (negated) { - return CapProdI(gcd, -known_lb); - } else { - return CapProdI(gcd, known_ub); - } - } - return kMaxIntegerValue; -} - std::vector> BestBinaryRelationBounds::GetSortedNonTrivialUpperBounds() const { std::vector> root_relations_sorted; diff --git a/ortools/sat/integer_base.h b/ortools/sat/integer_base.h index 0301f443f5..66a04864bb 100644 --- a/ortools/sat/integer_base.h +++ b/ortools/sat/integer_base.h @@ -514,11 +514,6 @@ class BestBinaryRelationBounds { RelationStatus GetStatus(LinearExpression2 expr, IntegerValue lb, IntegerValue ub) const; - // Return a valid upper-bound on the given LinearExpression2. Note that we - // assume kMaxIntegerValue is always valid and returns it if we don't have an - // entry in the hash-map. - IntegerValue GetUpperBound(LinearExpression2 expr) const; - // Same as GetUpperBound() but assume the expression is already canonicalized. // This is slightly faster. IntegerValue UpperBoundWhenCanonicalized(LinearExpression2 expr) const; diff --git a/ortools/sat/integer_base_test.cc b/ortools/sat/integer_base_test.cc index 2b45a6e206..5285b4e383 100644 --- a/ortools/sat/integer_base_test.cc +++ b/ortools/sat/integer_base_test.cc @@ -94,28 +94,6 @@ TEST(BestBinaryRelationBoundsTest, Basic) { best_bounds.GetStatus(expr, IntegerValue(-5), IntegerValue(3))); } -TEST(BestBinaryRelationBoundsTest, UpperBound) { - LinearExpression2 expr; - expr.vars[0] = IntegerVariable(0); - expr.vars[1] = IntegerVariable(2); - expr.coeffs[0] = IntegerValue(1); - expr.coeffs[1] = IntegerValue(-1); - - using AddResult = BestBinaryRelationBounds::AddResult; - BestBinaryRelationBounds best_bounds; - EXPECT_EQ(best_bounds.Add(expr, IntegerValue(0), IntegerValue(5)), - std::make_pair(AddResult::ADDED, AddResult::ADDED)); - - EXPECT_EQ(best_bounds.GetUpperBound(expr), IntegerValue(5)); - - expr.coeffs[0] *= 3; - expr.coeffs[1] *= 3; - EXPECT_EQ(best_bounds.GetUpperBound(expr), IntegerValue(15)); - - expr.Negate(); - EXPECT_EQ(best_bounds.GetUpperBound(expr), IntegerValue(0)); -} - AffineExpression OtherAffineLowerBound(LinearExpression2 expr, int var_index, IntegerValue expr_lb, IntegerValue other_var_lb) { diff --git a/ortools/sat/presolve_encoding.cc b/ortools/sat/presolve_encoding.cc index 33398ff76b..b11e4f4c87 100644 --- a/ortools/sat/presolve_encoding.cc +++ b/ortools/sat/presolve_encoding.cc @@ -17,17 +17,586 @@ #include #include #include +#include #include #include +#include "absl/algorithm/container.h" +#include "absl/container/flat_hash_map.h" +#include "absl/container/flat_hash_set.h" +#include "absl/container/inlined_vector.h" +#include "absl/log/check.h" #include "absl/log/log.h" +#include "google/protobuf/repeated_field.h" +#include "ortools/base/stl_util.h" #include "ortools/sat/cp_model_utils.h" #include "ortools/sat/presolve_context.h" +#include "ortools/util/bitset.h" #include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { +namespace { +bool ConstraintIsEncodingBound(const ConstraintProto& ct) { + if (ct.constraint_case() != ConstraintProto::kLinear) return false; + if (ct.linear().vars_size() != 1) return false; + if (ct.linear().coeffs(0) != 1) return false; + if (ct.enforcement_literal_size() != 1) return false; + if (PositiveRef(ct.enforcement_literal(0)) == ct.linear().vars(0)) { + return false; + } + return true; +} +} // namespace + +std::vector CreateVariableEncodingLocalModels( + PresolveContext* context) { + // In this function we want to make sure we don't waste too much time on + // problems that do not have many linear1. Thus, the first thing we do is to + // filter out as soon and cheaply as possible the bare minimum of constraints + // that could be relevant to the final output. + + // Constraints taking a list of literals that can, under some conditions, + // accept the following substitution: + // constraint(a, b, ...) => constraint(a | b, ...) + // one obvious case is bool_or. But if we can know that a and b cannot be + // both true, we can also apply this to at_most_one and exactly_one. + // + // Note that in the implementation we might for simplicity refer to the + // constraints we are interested in as "bool_or" but this is just to avoid + // mentioning all the three types over and over. + // TODO(user): this should also work for linear constraints with the two + // booleans having the same coefficient? + std::vector constraint_encoding_or; // bool_or, exactly_one, at_most_one + + // Do a pass to gather all linear1 constraints. + absl::flat_hash_map> var_to_linear1; + for (int i = 0; i < context->working_model->constraints_size(); ++i) { + const ConstraintProto& ct = context->working_model->constraints(i); + if (ct.constraint_case() == ConstraintProto::kBoolOr || + ct.constraint_case() == ConstraintProto::kAtMostOne || + ct.constraint_case() == ConstraintProto::kExactlyOne) { + constraint_encoding_or.push_back(i); + continue; + } + if (!ConstraintIsEncodingBound(ct)) { + continue; + } + var_to_linear1[ct.linear().vars(0)].push_back(i); + } + + // Filter out the variables that do not have an interesting encoding. + absl::erase_if(var_to_linear1, [context](const auto& p) { + if (p.second.size() > 1) return false; + return context->VarToConstraints(p.first).size() > 2; + }); + + if (var_to_linear1.empty()) return {}; + + absl::flat_hash_map> bool_to_var_encodings; + + // Now we use the linear1 we found to see which bool_or/amo/exactly_one are + // linking two encodings of the same variable. But first, since some models + // have a lot of bool_or, we use a simple heuristic to filter out all that are + // not related to the encodings. We use a bitset to keep track of all boolean + // potentially encoding a domain for any variable and we filter out all + // bool_or that are not linked to at least two of these booleans. + Bitset64 booleans_potentially_encoding_domain( + context->working_model->variables_size()); + + for (const auto& [var, linear1_cts] : var_to_linear1) { + for (const int c : linear1_cts) { + const ConstraintProto& ct = context->working_model->constraints(c); + const int bool_var = PositiveRef(ct.enforcement_literal(0)); + booleans_potentially_encoding_domain.Set(bool_var); + bool_to_var_encodings[bool_var].push_back(var); + } + } + for (auto& [bool_var, var_encodings] : bool_to_var_encodings) { + // Remove the potential duplicate for the negation. + gtl::STLSortAndRemoveDuplicates(&var_encodings); + } + int new_encoding_or_count = 0; + for (int i = 0; i < constraint_encoding_or.size(); ++i) { + const int c = constraint_encoding_or[i]; + const ConstraintProto& ct = context->working_model->constraints(c); + const BoolArgumentProto& bool_ct = + ct.constraint_case() == ConstraintProto::kAtMostOne + ? ct.at_most_one() + : (ct.constraint_case() == ConstraintProto::kExactlyOne + ? ct.exactly_one() + : ct.bool_or()); + if (absl::c_count_if( + bool_ct.literals(), + [booleans_potentially_encoding_domain](int ref) { + return booleans_potentially_encoding_domain[PositiveRef(ref)]; + }) < 2) { + continue; + } + constraint_encoding_or[new_encoding_or_count++] = c; + } + constraint_encoding_or.resize(new_encoding_or_count); + + // Track the number of times a given boolean appears in the local model for a + // given variable. + struct VariableAndBoolInfo { + // Can only be 1 or 2 (for negation) if properly presolved. + int linear1_count = 0; + // Number of times the boolean will appear in + // `constraints_linking_two_encoding_booleans`. + int bool_or_count = 0; + }; + absl::flat_hash_map, VariableAndBoolInfo> var_bool_counts; + + // Now that we have a potentially smaller set of bool_or, we actually check + // which of them are linking two encodings of the same variable. + absl::flat_hash_map> var_to_constraints_encoding_or; + + // Map from variable to the bools that appear in a given bool_or. + absl::flat_hash_map> var_to_bools; + + for (const int c : constraint_encoding_or) { + var_to_bools.clear(); + const ConstraintProto& ct = context->working_model->constraints(c); + const BoolArgumentProto& bool_ct = + ct.constraint_case() == ConstraintProto::kAtMostOne + ? ct.at_most_one() + : (ct.constraint_case() == ConstraintProto::kExactlyOne + ? ct.exactly_one() + : ct.bool_or()); + for (const int ref : bool_ct.literals()) { + const int bool_var = PositiveRef(ref); + if (!booleans_potentially_encoding_domain[bool_var]) continue; + for (const int var : bool_to_var_encodings[bool_var]) { + var_to_bools[var].push_back(bool_var); + } + } + for (const auto& [var, bools] : var_to_bools) { + if (bools.size() >= 2) { + // We have two encodings of `var` in the same constraint `c`. Thus `c` + // should be part of the local model for `var`. + var_to_constraints_encoding_or[var].push_back(c); + for (const int bool_var : bools) { + var_bool_counts[{var, bool_var}].bool_or_count++; + } + } + } + } + + std::vector local_models; + // Now that we have all the information, we can create the local models. + for (const auto& [var, linear1_cts] : var_to_linear1) { + VariableEncodingLocalModel& encoding_model = local_models.emplace_back(); + encoding_model.var = var; + encoding_model.linear1_constraints.assign(linear1_cts.begin(), + linear1_cts.end()); + encoding_model.constraints_linking_two_encoding_booleans = + var_to_constraints_encoding_or[var]; + absl::c_sort(encoding_model.constraints_linking_two_encoding_booleans); + encoding_model.var_in_more_than_one_constraint_outside_the_local_model = + (context->VarToConstraints(var).size() - linear1_cts.size() > 1); + for (const int ct : linear1_cts) { + const int bool_var = PositiveRef( + context->working_model->constraints(ct).enforcement_literal(0)); + encoding_model.bools_only_used_inside_the_local_model.insert(bool_var); + var_bool_counts[{var, bool_var}].linear1_count++; + } + absl::erase_if(encoding_model.bools_only_used_inside_the_local_model, + [context, v = var, &var_bool_counts](int bool_var) { + const auto& counts = var_bool_counts[{v, bool_var}]; + return context->VarToConstraints(bool_var).size() != + counts.linear1_count + counts.bool_or_count; + }); + auto it = context->ObjectiveMap().find(var); + if (it != context->ObjectiveMap().end()) { + encoding_model.variable_coeff_in_objective = it->second; + } + } + absl::c_sort(local_models, [](const VariableEncodingLocalModel& a, + const VariableEncodingLocalModel& b) { + return a.var < b.var; + }); + return local_models; +} + +bool BasicPresolveAndGetFullyEncodedDomains( + PresolveContext* context, VariableEncodingLocalModel& local_model, + absl::flat_hash_map* result, bool* changed) { + *changed = false; + absl::flat_hash_map ref_to_linear1; + + // Fill ref_to_linear1 and do some basic presolving. + const Domain var_domain = context->DomainOf(local_model.var); + for (const int ct : local_model.linear1_constraints) { + ConstraintProto* ct_proto = context->working_model->mutable_constraints(ct); + DCHECK(ConstraintIsEncodingBound(*ct_proto)); + const int ref = ct_proto->enforcement_literal(0); + Domain domain = ReadDomainFromProto(ct_proto->linear()); + if (!domain.IsIncludedIn(var_domain)) { + *changed = true; + domain = domain.IntersectionWith(context->DomainOf(local_model.var)); + if (domain.IsEmpty()) { + context->UpdateRuleStats( + "variables: linear1 with domain not included in variable domain"); + if (!context->SetLiteralToFalse(ref)) { + return false; + } + ct_proto->Clear(); + context->UpdateConstraintVariableUsage(ct); + continue; + } + FillDomainInProto(domain, ct_proto->mutable_linear()); + } + auto [it, inserted] = ref_to_linear1.insert({ref, ct}); + if (!inserted) { + *changed = true; + ConstraintProto* old_ct_proto = + context->working_model->mutable_constraints(it->second); + const Domain old_ct_domain = ReadDomainFromProto(old_ct_proto->linear()); + const Domain new_domain = domain.IntersectionWith(old_ct_domain); + ct_proto->Clear(); + context->UpdateConstraintVariableUsage(ct); + if (new_domain.IsEmpty()) { + context->UpdateRuleStats( + "variables: linear1 with same variable and enforcement and " + "non-overlapping domain, setting enforcement to false"); + if (!context->SetLiteralToFalse(ref)) { + return false; + } + old_ct_proto->Clear(); + context->UpdateConstraintVariableUsage(it->second); + ref_to_linear1.erase(ref); + } else { + FillDomainInProto(new_domain, old_ct_proto->mutable_linear()); + context->UpdateRuleStats( + "variables: merged two linear1 with same variable and enforcement"); + } + } + } + + // Remove from the local model anything that was removed in the loop above. + int new_linear1_size = 0; + for (int i = 0; i < local_model.linear1_constraints.size(); ++i) { + const int ct = local_model.linear1_constraints[i]; + const ConstraintProto& ct_proto = context->working_model->constraints(ct); + if (ct_proto.constraint_case() != ConstraintProto::kLinear) continue; + if (context->IsFixed(ct_proto.enforcement_literal(0))) { + continue; + } + DCHECK(ConstraintIsEncodingBound(ct_proto)); + local_model.linear1_constraints[new_linear1_size++] = ct; + } + if (new_linear1_size != local_model.linear1_constraints.size()) { + *changed = true; + local_model.linear1_constraints.resize(new_linear1_size); + // Rerun the presolve loop to recompute ref_to_linear1. + return true; + } + + for (const auto& [ref, ct] : ref_to_linear1) { + auto it = ref_to_linear1.find(NegatedRef(ref)); + if (it == ref_to_linear1.end()) continue; + const ConstraintProto& positive_ct = + context->working_model->constraints(ct); + const ConstraintProto& negative_ct = + context->working_model->constraints(it->second); + const Domain positive_domain = ReadDomainFromProto(positive_ct.linear()); + const Domain negative_domain = ReadDomainFromProto(negative_ct.linear()); + if (!positive_domain.IntersectionWith(negative_domain).IsEmpty()) { + // This is not a fully encoded domain. For example, it could be + // l => x in {-inf,inf} + // ~l => x in {-inf,inf} + // which actually means that `l` doesn't really encode anything. + continue; + } + bool domain_modified = false; + if (!context->IntersectDomainWith( + local_model.var, positive_domain.UnionWith(negative_domain), + &domain_modified)) { + return false; + } + *changed = *changed || domain_modified; + result->insert({ref, positive_domain}); + result->insert({NegatedRef(ref), negative_domain}); + } + + // Now detect a different way of fully encoding a domain: + // l1 => x in D1 + // l2 => x in D2 + // l3 => x in D3 + // ... + // l_n => x in D_n + // bool_or(l1, l2, l3, ..., l_n) + // + // where D1, D2, ..., D_n are non overlapping. This works too for exactly_one. + for (const int ct : local_model.constraints_linking_two_encoding_booleans) { + const ConstraintProto& ct_proto = context->working_model->constraints(ct); + if (ct_proto.constraint_case() != ConstraintProto::kBoolOr && + ct_proto.constraint_case() != ConstraintProto::kExactlyOne) { + continue; + } + if (!ct_proto.enforcement_literal().empty()) continue; + const BoolArgumentProto& bool_or = + ct_proto.constraint_case() == ConstraintProto::kExactlyOne + ? ct_proto.exactly_one() + : ct_proto.bool_or(); + if (bool_or.literals().size() < 2) continue; + bool encoding_detected = true; + Domain non_overlapping_domain; + std::vector> ref_and_domains; + for (const int ref : bool_or.literals()) { + auto it = ref_to_linear1.find(ref); + if (it == ref_to_linear1.end()) { + encoding_detected = false; + break; + } + const Domain domain = ReadDomainFromProto( + context->working_model->constraints(it->second).linear()); + ref_and_domains.push_back({ref, domain}); + if (!non_overlapping_domain.IntersectionWith(domain).IsEmpty()) { + encoding_detected = false; + break; + } + non_overlapping_domain = non_overlapping_domain.UnionWith(domain); + } + if (encoding_detected) { + context->UpdateRuleStats("variables: detected fully encoded domain"); + bool domain_modified = false; + if (!context->IntersectDomainWith(local_model.var, non_overlapping_domain, + &domain_modified)) { + return false; + } + if (domain_modified) { + context->UpdateRuleStats( + "variables: restricted domain to fully encoded domain"); + } + *changed = *changed || domain_modified; + for (const auto& [ref, domain] : ref_and_domains) { + result->insert({ref, domain}); + result->insert({NegatedRef(ref), + var_domain.IntersectionWith(domain.Complement())}); + } + // Promote a bool_or to an exactly_one. + if (ct_proto.constraint_case() == ConstraintProto::kBoolOr) { + context->UpdateRuleStats( + "variables: promoted bool_or to exactly_one for fully encoded " + "domain"); + std::vector new_enforcement_literals(bool_or.literals().begin(), + bool_or.literals().end()); + context->working_model->mutable_constraints(ct)->clear_bool_or(); + context->working_model->mutable_constraints(ct) + ->mutable_exactly_one() + ->mutable_literals() + ->Add(new_enforcement_literals.begin(), + new_enforcement_literals.end()); + *changed = true; + } + } + } + return true; +} + +// Return false on unsat +bool DetectEncodedComplexDomain( + PresolveContext* context, int ct_index, + VariableEncodingLocalModel& local_model, + absl::flat_hash_map* fully_encoded_domains, bool* changed) { + ConstraintProto* ct = context->working_model->mutable_constraints(ct_index); + *changed = false; + + if (context->ModelIsUnsat()) return false; + DCHECK(ct->constraint_case() == ConstraintProto::kAtMostOne || + ct->constraint_case() == ConstraintProto::kExactlyOne || + ct->constraint_case() == ConstraintProto::kBoolOr); + + // Handling exaclty_one, at_most_one and bool_or is pretty similar. If we have + // l1 <=> v \in D1 + // l2 <=> v \in D2 + // + // We built + // l <=> v \in (D1 U D2). + // + // Moreover, if we have exactly_one(l1, l2, ...) or at_most_one(l1, l2, ...), + // we know that v cannot be in the intersection of D1 and D2. Thus, we first + // unconditionally remove (D1 ∩ D2) from the domain of v, making + // (l1=true and l2=true) impossible and allowing us to write our clauses as + // exactly_one(l1 or l2, ...) or at_most_one(l1 or l2, ...). + // + // Thus, other than the domain reduction that should not be done for the + // bool_or, all we need is to create a variable + // (l1 or l2) == l <=> (v \in (D1 U D2)). + google::protobuf::RepeatedField& literals = + ct->constraint_case() == ConstraintProto::kAtMostOne + ? *ct->mutable_at_most_one()->mutable_literals() + : (ct->constraint_case() == ConstraintProto::kExactlyOne + ? *ct->mutable_exactly_one()->mutable_literals() + : *ct->mutable_bool_or()->mutable_literals()); + if (literals.size() <= 1) return true; + + if (!ct->enforcement_literal().empty()) { + // TODO(user): support this case if it any problem needs it. + return true; + } + + // When we have + // lit => var in D1 + // ~lit => var in D2 + // we can represent this on a line: + // + // ----------------D1---------------- + // ----------------D2--------------- + // |+++++++++++|*********************|++++++++++| + // lit=false lit unconstrained lit=true + // + // Handling the case where the variable is unconstrained by the lit is a + // bit of a pain: we want to replace two literals in a exactly_one by a + // single one, and if they are both unconstrained we might be forced to pick + // one arbitrarily to set to true. In any case, this is not a proper + // encoding of a complex domain, so we just ignore it. + // TODO(user): This can be implemented if it turns out to be common. + + std::optional maybe_lit1; + Domain domain_lit1; + std::optional maybe_lit2; + Domain domain_lit2; + for (const int lit_var : literals) { + if (!local_model.bools_only_used_inside_the_local_model.contains( + PositiveRef(lit_var))) { + continue; + } + auto it = fully_encoded_domains->find(lit_var); + if (it == fully_encoded_domains->end()) { + continue; + } + + if (!maybe_lit1) { + maybe_lit1 = lit_var; + domain_lit1 = it->second; + } else { + maybe_lit2 = lit_var; + domain_lit2 = it->second; + break; + } + } + + if (!maybe_lit2.has_value()) return true; + DCHECK(maybe_lit1.has_value()); + const int lit1 = *maybe_lit1; + const int lit2 = *maybe_lit2; + + // We found two literals that each fully encodes an interval and are both only + // used in the encoding and in the bool_or/exactly_one/at_most_one. We can + // thus replace the two literals by their OR. Since this code is already + // rather complex, so we will just simplify a pair of literals at a time, and + // leave for the presolve fixpoint to do the rest. + *changed = true; + + context->UpdateRuleStats( + "variables: detected encoding of a complex domain with multiple " + "linear1"); + + if (ct->constraint_case() != ConstraintProto::kBoolOr) { + // In virtue of the AMO, var must not be in the intersection of the two + // domains where both literals are true. + if (!context->IntersectDomainWith( + local_model.var, + domain_lit2.IntersectionWith(domain_lit1).Complement())) { + return false; + } + } + const Domain var_domain = context->DomainOf(local_model.var); + const Domain domain_new_var_false = var_domain.IntersectionWith( + domain_lit1.Complement().IntersectionWith(domain_lit2.Complement())); + const Domain domain_new_var_true = + var_domain.IntersectionWith(domain_new_var_false.Complement()); + + // Now we want to build a lit3 = (lit1 or lit2) to use in the AMO/bool_or. + const int new_var = context->NewBoolVarWithClause({lit1, lit2}); + + if (domain_new_var_true.IsEmpty()) { + CHECK(context->SetLiteralToFalse(new_var)); + } else if (domain_new_var_false.IsEmpty()) { + CHECK(context->SetLiteralToTrue(new_var)); + } else { + local_model.linear1_constraints.push_back( + context->working_model->constraints_size()); + ConstraintProto* new_ct = context->working_model->add_constraints(); + new_ct->add_enforcement_literal(new_var); + new_ct->mutable_linear()->add_vars(local_model.var); + new_ct->mutable_linear()->add_coeffs(1); + FillDomainInProto(domain_new_var_true, new_ct->mutable_linear()); + local_model.linear1_constraints.push_back( + context->working_model->constraints_size()); + new_ct = context->working_model->add_constraints(); + new_ct->add_enforcement_literal(NegatedRef(new_var)); + new_ct->mutable_linear()->add_vars(local_model.var); + new_ct->mutable_linear()->add_coeffs(1); + FillDomainInProto(domain_new_var_false, new_ct->mutable_linear()); + context->UpdateNewConstraintsVariableUsage(); + } + + // Remove the two literals from the AMO. + int new_size = 0; + for (int i = 0; i < literals.size(); ++i) { + if (literals.Get(i) != lit1 && literals.Get(i) != lit2) { + literals.Set(new_size++, literals.Get(i)); + } + } + literals.Truncate(new_size); + literals.Add(new_var); + context->UpdateConstraintVariableUsage(ct_index); + + // Finally, move the four linear1 to the mapping model. + fully_encoded_domains->insert({new_var, domain_new_var_true}); + fully_encoded_domains->insert({NegatedRef(new_var), domain_new_var_false}); + fully_encoded_domains->erase(lit1); + fully_encoded_domains->erase(lit2); + fully_encoded_domains->erase(NegatedRef(lit1)); + fully_encoded_domains->erase(NegatedRef(lit2)); + context->MarkVariableAsRemoved(PositiveRef(lit1)); + context->MarkVariableAsRemoved(PositiveRef(lit2)); + int new_linear1_size = 0; + for (int i = 0; i < local_model.linear1_constraints.size(); ++i) { + const int ct = local_model.linear1_constraints[i]; + ConstraintProto* ct_proto = context->working_model->mutable_constraints(ct); + if (PositiveRef(ct_proto->enforcement_literal(0)) == PositiveRef(lit1) || + PositiveRef(ct_proto->enforcement_literal(0)) == PositiveRef(lit2)) { + context->NewMappingConstraint(*ct_proto, __FILE__, __LINE__); + ct_proto->Clear(); + context->UpdateConstraintVariableUsage(ct); + continue; + } + local_model.linear1_constraints[new_linear1_size++] = ct; + } + local_model.linear1_constraints.resize(new_linear1_size); + + return true; +} + +bool DetectAllEncodedComplexDomain(PresolveContext* context, + VariableEncodingLocalModel& local_model) { + absl::flat_hash_map fully_encoded_domains; + bool changed_on_basic_presolve = false; + if (!BasicPresolveAndGetFullyEncodedDomains(context, local_model, + &fully_encoded_domains, + &changed_on_basic_presolve)) { + return false; + } + if (local_model.constraints_linking_two_encoding_booleans.size() != 1) { + return true; + } + const int ct = local_model.constraints_linking_two_encoding_booleans[0]; + bool changed = true; + while (changed) { + if (!DetectEncodedComplexDomain(context, ct, local_model, + &fully_encoded_domains, &changed)) { + return false; + } + } + return true; +} + bool MaybeTransferLinear1ToAnotherVariable( VariableEncodingLocalModel& local_model, PresolveContext* context) { if (local_model.var == -1) return true; @@ -131,6 +700,5 @@ bool MaybeTransferLinear1ToAnotherVariable( local_model.var = -1; return true; } - } // namespace sat } // namespace operations_research diff --git a/ortools/sat/presolve_encoding.h b/ortools/sat/presolve_encoding.h index 6dad2318bd..5c0f2d8170 100644 --- a/ortools/sat/presolve_encoding.h +++ b/ortools/sat/presolve_encoding.h @@ -17,7 +17,10 @@ #include #include +#include "absl/container/flat_hash_map.h" +#include "absl/container/flat_hash_set.h" #include "ortools/sat/presolve_context.h" +#include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { @@ -33,6 +36,13 @@ struct VariableEncodingLocalModel { // fulfilling the conditions above will appear here. std::vector linear1_constraints; + // Constraints of the form bool_or/exactly_one/at_most_one that contains at + // least two of the encoding booleans. + std::vector constraints_linking_two_encoding_booleans; + + // Booleans that do not appear on any constraints outside the local model. + absl::flat_hash_set bools_only_used_inside_the_local_model; + // Zero if `var` doesn't appear in the objective. int64_t variable_coeff_in_objective = 0; @@ -44,6 +54,44 @@ struct VariableEncodingLocalModel { int single_constraint_using_the_var_outside_the_local_model = -1; }; +// For performance, this skips variables that appears in a single linear1 and is +// used in more than another constraint, since there is no interesting presolve +// we can do in this case. +std::vector CreateVariableEncodingLocalModels( + PresolveContext* context); + +// Do a few simple presolve rules on the local model: +// - restrict the domain of the linear1 to the domain of the variable. +// - merge linear1 over the same enforcement,var pairs. +// - if we have a linear1 for a literal and another for its negation, do +// not allow both to be true. +// +// Also returns a list of literals that fully encodes a domain for the variable. +// Returns false if we prove unsat. +bool BasicPresolveAndGetFullyEncodedDomains( + PresolveContext* context, VariableEncodingLocalModel& local_model, + absl::flat_hash_map* result, bool* changed); + +// If we have a model containing: +// l1 => var in [0, 10] +// ~l1 => var in [11, 20] +// l2 => var in [50, 60] +// ~l2 => var in [70, 80] +// bool_or(l1, l2, ...) +// +// if moreover `l1` and `l2` are only used in the constraints above, we can +// replace them by: +// l3 => var in [0, 10] U [50, 60] +// ~l3 => var in [11, 20] U [70, 80] +// bool_or(l3, ...) +// +// and remove the variables `l1` and `l2`. This also works if we replace the +// bool_or for an at_most_one or an exactly_one, but requires imposing +// (unconditionally) that the variable cannot be both in the domain encoded by +// `l1` and in the domain encoded by `l2`. +bool DetectAllEncodedComplexDomain(PresolveContext* context, + VariableEncodingLocalModel& local_model); + // If we have a bunch of constraint of the form literal => Y \in domain and // another constraint Y = f(X), we can remove Y, that constraint, and transform // all linear1 from constraining Y to constraining X. diff --git a/ortools/sat/presolve_encoding_test.cc b/ortools/sat/presolve_encoding_test.cc new file mode 100644 index 0000000000..5a9214e5be --- /dev/null +++ b/ortools/sat/presolve_encoding_test.cc @@ -0,0 +1,462 @@ +// 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/presolve_encoding.h" + +#include + +#include "absl/container/flat_hash_map.h" +#include "absl/log/check.h" +#include "gtest/gtest.h" +#include "ortools/base/gmock.h" +#include "ortools/base/parse_test_proto.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/model.h" +#include "ortools/sat/presolve_context.h" +#include "ortools/util/sorted_interval_list.h" + +namespace operations_research { +namespace sat { +namespace { + +using ::google::protobuf::contrib::parse_proto::ParseTestProto; +using ::testing::ElementsAre; +using ::testing::Pair; +using ::testing::UnorderedElementsAre; + +TEST(CreateVariableEncodingLocalModelsTest, TrivialTest) { + CpModelProto model_proto = ParseTestProto(R"pb( + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + constraints { + enforcement_literal: 0 + linear { + vars: [ 1 ] + coeffs: [ 1 ] + domain: [ 0, 1 ] + } + } + )pb"); + Model model; + CpModelProto mapping_model; + PresolveContext context(&model, &model_proto, &mapping_model); + context.InitializeNewDomains(); + context.ReadObjectiveFromProto(); + context.UpdateNewConstraintsVariableUsage(); + const std::vector local_models = + CreateVariableEncodingLocalModels(&context); + ASSERT_EQ(local_models.size(), 1); + ASSERT_EQ(local_models[0].var, 1); + EXPECT_THAT(local_models[0].linear1_constraints, ElementsAre(0)); +} + +TEST(CreateVariableEncodingLocalModelsTest, BasicTest) { + CpModelProto model_proto = ParseTestProto(R"pb( + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 2 ] } + constraints { + enforcement_literal: 0 + linear { + vars: [ 2 ] + coeffs: [ 1 ] + domain: [ 0, 0 ] + } + } + constraints { + enforcement_literal: 1 + linear { + vars: [ 2 ] + coeffs: [ 1 ] + domain: [ 0, 0 ] + } + } + constraints { bool_or { literals: [ 0, 1 ] } } + )pb"); + Model model; + CpModelProto mapping_model; + PresolveContext context(&model, &model_proto, &mapping_model); + context.InitializeNewDomains(); + context.ReadObjectiveFromProto(); + context.UpdateNewConstraintsVariableUsage(); + const std::vector local_models = + CreateVariableEncodingLocalModels(&context); + ASSERT_EQ(local_models.size(), 1); + ASSERT_EQ(local_models[0].var, 2); + EXPECT_THAT(local_models[0].linear1_constraints, ElementsAre(0, 1)); + EXPECT_THAT(local_models[0].constraints_linking_two_encoding_booleans, + ElementsAre(2)); + EXPECT_THAT(local_models[0].bools_only_used_inside_the_local_model, + UnorderedElementsAre(0, 1)); +} + +TEST(CreateVariableEncodingLocalModelsTest, OneBooleanUsedElsewhere) { + CpModelProto model_proto = ParseTestProto(R"pb( + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 2 ] } + constraints { + enforcement_literal: 0 + linear { + vars: [ 3 ] + coeffs: [ 1 ] + domain: [ 0, 0 ] + } + } + constraints { + enforcement_literal: 1 + linear { + vars: [ 3 ] + coeffs: [ 1 ] + domain: [ 1, 1 ] + } + } + constraints { + enforcement_literal: 2 + linear { + vars: [ 3 ] + coeffs: [ 1 ] + domain: [ 2, 2 ] + } + } + constraints { bool_or { literals: [ 0, 1, 2 ] } } + constraints { at_most_one { literals: [ 0, 1, 2 ] } } + constraints { + linear { + vars: [ 2, 3 ] + coeffs: [ 1, 1 ] + domain: [ 0, 3 ] + } + } + objective { + vars: [ 1 ] + coeffs: [ 2 ] + } + )pb"); + Model model; + CpModelProto mapping_model; + PresolveContext context(&model, &model_proto, &mapping_model); + context.InitializeNewDomains(); + context.ReadObjectiveFromProto(); + context.UpdateNewConstraintsVariableUsage(); + const std::vector local_models = + CreateVariableEncodingLocalModels(&context); + ASSERT_EQ(local_models.size(), 1); + ASSERT_EQ(local_models[0].var, 3); + EXPECT_THAT(local_models[0].linear1_constraints, ElementsAre(0, 1, 2)); + EXPECT_THAT(local_models[0].constraints_linking_two_encoding_booleans, + ElementsAre(3, 4)); + EXPECT_THAT(local_models[0].bools_only_used_inside_the_local_model, + UnorderedElementsAre(0)); +} + +TEST(CreateVariableEncodingLocalModelsTest, TwoVars) { + CpModelProto model_proto = ParseTestProto(R"pb( + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 2 ] } + variables { domain: [ 0, 2 ] } + variables { domain: [ 0, 1 ] } + constraints { + enforcement_literal: 0 + linear { + vars: [ 3 ] + coeffs: [ 1 ] + domain: [ 0, 0 ] + } + } + constraints { + enforcement_literal: -1 + linear { + vars: [ 3 ] + coeffs: [ 1 ] + domain: [ 1, 1 ] + } + } + constraints { + enforcement_literal: 1 + linear { + vars: [ 3 ] + coeffs: [ 1 ] + domain: [ 1, 1 ] + } + } + constraints { + enforcement_literal: 1 + linear { + vars: [ 4 ] + coeffs: [ 1 ] + domain: [ 2, 2 ] + } + } + constraints { + enforcement_literal: 2 + linear { + vars: [ 4 ] + coeffs: [ 1 ] + domain: [ 2, 2 ] + } + } + constraints { bool_or { literals: [ 0, 1, 5 ] } } + constraints { at_most_one { literals: [ 0, 1, 2 ] } } + constraints { + linear { + vars: [ 2, 3 ] + coeffs: [ 1, 1 ] + domain: [ 0, 3 ] + } + } + objective { + vars: [ 3 ] + coeffs: [ 2 ] + } + )pb"); + Model model; + CpModelProto mapping_model; + PresolveContext context(&model, &model_proto, &mapping_model); + context.InitializeNewDomains(); + context.ReadObjectiveFromProto(); + context.UpdateNewConstraintsVariableUsage(); + std::vector local_models = + CreateVariableEncodingLocalModels(&context); + ASSERT_EQ(local_models.size(), 2); + ASSERT_EQ(local_models[0].var, 3); + ASSERT_EQ(local_models[1].var, 4); + EXPECT_THAT(local_models[0].linear1_constraints, ElementsAre(0, 1, 2)); + EXPECT_THAT(local_models[1].linear1_constraints, ElementsAre(3, 4)); + EXPECT_THAT(local_models[0].constraints_linking_two_encoding_booleans, + ElementsAre(5, 6)); + EXPECT_THAT(local_models[1].constraints_linking_two_encoding_booleans, + ElementsAre(6)); + EXPECT_THAT(local_models[0].bools_only_used_inside_the_local_model, + UnorderedElementsAre(0)); + EXPECT_THAT(local_models[1].bools_only_used_inside_the_local_model, + UnorderedElementsAre()); + EXPECT_EQ(local_models[0].variable_coeff_in_objective, 2); + EXPECT_EQ(local_models[1].variable_coeff_in_objective, 0); + + absl::flat_hash_map fully_encoded_domains; + bool changed = false; + CHECK(BasicPresolveAndGetFullyEncodedDomains( + &context, local_models[0], &fully_encoded_domains, &changed)); + EXPECT_THAT( + fully_encoded_domains, + UnorderedElementsAre(Pair(0, Domain(0, 0)), Pair(-1, Domain(1, 1)))); +} + +TEST(BasicPresolveAndGetFullyEncodedDomainsTest, EncodingWithBoolOr) { + CpModelProto model_proto = ParseTestProto(R"pb( + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 2 ] } + variables { domain: [ 0, 2 ] } + constraints { + enforcement_literal: 0 + linear { + vars: [ 3 ] + coeffs: [ 1 ] + domain: [ 0, 0 ] + } + } + constraints { + enforcement_literal: 1 + linear { + vars: [ 3 ] + coeffs: [ 1 ] + domain: [ 1, 1 ] + } + } + constraints { + enforcement_literal: 2 + linear { + vars: [ 3 ] + coeffs: [ 1 ] + domain: [ 2, 2 ] + } + } + constraints { + enforcement_literal: 0 + linear { + vars: [ 4 ] + coeffs: [ 1 ] + domain: [ 2, 2 ] + } + } + constraints { bool_or { literals: [ 0, 1, 2 ] } } + constraints { + linear { + vars: [ 2, 3 ] + coeffs: [ 1, 1 ] + domain: [ 0, 3 ] + } + } + objective { + vars: [ 3 ] + coeffs: [ 2 ] + } + )pb"); + Model model; + CpModelProto mapping_model; + PresolveContext context(&model, &model_proto, &mapping_model); + context.InitializeNewDomains(); + context.ReadObjectiveFromProto(); + context.UpdateNewConstraintsVariableUsage(); + std::vector local_models = + CreateVariableEncodingLocalModels(&context); + + absl::flat_hash_map fully_encoded_domains; + bool changed = false; + CHECK(BasicPresolveAndGetFullyEncodedDomains( + &context, local_models[0], &fully_encoded_domains, &changed)); + EXPECT_THAT(fully_encoded_domains, + UnorderedElementsAre(Pair(0, Domain(0)), Pair(1, Domain(1)), + Pair(2, Domain(2)), + Pair(-1, Domain::FromValues({1, 2})), + Pair(-2, Domain::FromValues({0, 2})), + Pair(-3, Domain::FromValues({0, 1})))); + ConstraintProto expected_exactly_one = ParseTestProto(R"pb( + exactly_one { literals: [ 0, 1, 2 ] } + )pb"); + EXPECT_THAT(context.working_model->constraints(), + testing::Contains(testing::EqualsProto(expected_exactly_one))); +} + +TEST(DetectAllEncodedComplexDomainTest, BasicTest) { + CpModelProto model_proto = ParseTestProto(R"pb( + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 5 ] } + variables { domain: [ 0, 2 ] } + constraints { + enforcement_literal: 0 + linear { + vars: [ 3 ] + coeffs: [ 1 ] + domain: [ 0, 1 ] + } + } + constraints { + enforcement_literal: -1 + linear { + vars: [ 3 ] + coeffs: [ 1 ] + domain: [ 2, 5 ] + } + } + # Note that the var=3 is missing from both this encoding and its negation. + constraints { + enforcement_literal: 1 + linear { + vars: [ 3 ] + coeffs: [ 1 ] + domain: [ 1, 2 ] + } + } + constraints { + enforcement_literal: -2 + linear { + vars: [ 3 ] + coeffs: [ 1 ] + domain: [ 0, 0, 4, 5 ] + } + } + constraints { + enforcement_literal: 2 + linear { + vars: [ 3 ] + coeffs: [ 1 ] + domain: [ 2, 2 ] + } + } + constraints { at_most_one { literals: [ 0, 1, 2 ] } } + constraints { + linear { + vars: [ 2, 3 ] + coeffs: [ 1, 1 ] + domain: [ 0, 3 ] + } + } + objective { + vars: [ 3 ] + coeffs: [ 2 ] + } + )pb"); + Model model; + CpModelProto mapping_model; + PresolveContext context(&model, &model_proto, &mapping_model); + context.InitializeNewDomains(); + context.ReadObjectiveFromProto(); + context.UpdateNewConstraintsVariableUsage(); + std::vector local_models = + CreateVariableEncodingLocalModels(&context); + ASSERT_TRUE(DetectAllEncodedComplexDomain(&context, local_models[0])); + context.WriteVariableDomainsToProto(); + const CpModelProto expected_model = ParseTestProto(R"pb( + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + variables { domain: [ 0, 1 ] } + # var=1 is forbidden by the at_most_one + variables { domain: [ 0, 0, 2, 2, 4, 5 ] } + variables { domain: [ 0, 2 ] } + variables { domain: [ 0, 1 ] } + constraints {} + constraints {} + constraints {} + constraints {} + constraints { + enforcement_literal: 2 + linear { + vars: [ 3 ] + coeffs: [ 1 ] + domain: [ 2, 2 ] + } + } + constraints { at_most_one { literals: [ 2, 5 ] } } + constraints { + linear { + vars: [ 2, 3 ] + coeffs: [ 1, 1 ] + domain: [ 0, 3 ] + } + } + constraints { + enforcement_literal: 5 + linear { + vars: [ 3 ] + coeffs: [ 1 ] + domain: [ 0, 0, 2, 2 ] + } + } + constraints { + enforcement_literal: -6 + linear { + vars: [ 3 ] + coeffs: [ 1 ] + domain: [ 4, 5 ] + } + } + objective { + vars: [ 3 ] + coeffs: [ 2 ] + } + )pb"); + EXPECT_THAT(context.working_model, testing::EqualsProto(expected_model)); +} + +} // namespace +} // namespace sat +} // namespace operations_research diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto index b7ebe2454c..56b0741719 100644 --- a/ortools/sat/sat_parameters.proto +++ b/ortools/sat/sat_parameters.proto @@ -24,7 +24,7 @@ option java_multiple_files = true; // Contains the definitions for all the sat algorithm parameters and their // default values. // -// NEXT TAG: 355 +// NEXT TAG: 356 message SatParameters { // In some context, like in a portfolio of search, it makes sense to name a // given parameters set for logging purpose. @@ -153,6 +153,10 @@ message SatParameters { // clause with it. optional int32 eagerly_subsume_last_n_conflicts = 343 [default = 4]; + // If we remove clause that we now are "implied" by others. Note that this + // might not always be good as we might loose some propagation power. + optional bool subsume_during_vivification = 355 [default = true]; + // If true, try to backtrack as little as possible on conflict and re-imply // the clauses later. // This means we discard less propagation than traditional backjumping, but diff --git a/ortools/sat/stat_tables.cc b/ortools/sat/stat_tables.cc index bded127e7f..48190cb5ef 100644 --- a/ortools/sat/stat_tables.cc +++ b/ortools/sat/stat_tables.cc @@ -120,7 +120,8 @@ void SharedStatTables::AddClausesStat(absl::string_view name, Model* model) { if (vivify_table_.empty()) { vivify_table_.push_back({"Vivification", "Clauses", "Decisions", "LitTrue", - "Subsumed", "LitRemoved", "DecisionReused"}); + "Subsumed", "LitRemoved", "DecisionReused", + "Conflicts"}); } vivify_table_.push_back({FormatName(name), FormatCounter(vivify_counters.num_clauses_vivified), @@ -128,7 +129,8 @@ void SharedStatTables::AddClausesStat(absl::string_view name, Model* model) { FormatCounter(vivify_counters.num_true), FormatCounter(vivify_counters.num_subsumed), FormatCounter(vivify_counters.num_removed_literals), - FormatCounter(vivify_counters.num_reused)}); + FormatCounter(vivify_counters.num_reused), + FormatCounter(vivify_counters.num_conflicts)}); // Track reductions of Boolean variables. if (bool_var_table_.empty()) { diff --git a/ortools/sat/vivification.cc b/ortools/sat/vivification.cc index fbfc150005..a0ef539964 100644 --- a/ortools/sat/vivification.cc +++ b/ortools/sat/vivification.cc @@ -18,8 +18,10 @@ #include #include "absl/algorithm/container.h" +#include "absl/cleanup/cleanup.h" #include "absl/container/btree_set.h" #include "absl/log/check.h" +#include "absl/log/log.h" #include "absl/types/span.h" #include "ortools/sat/clause.h" #include "ortools/sat/sat_base.h" @@ -31,7 +33,7 @@ namespace operations_research::sat { bool Vivifier::MinimizeByPropagation(bool log_info, double dtime_budget, bool minimize_new_clauses_only) { PresolveTimer timer("Vivification", logger_, time_limit_); - timer.OverrideLogging(log_info); + timer.OverrideLogging(log_info || VLOG_IS_ON(2)); sat_solver_->AdvanceDeterministicTime(time_limit_); const double threshold = @@ -44,34 +46,34 @@ bool Vivifier::MinimizeByPropagation(bool log_info, double dtime_budget, // Tricky: we don't want TryToMinimizeClause() to delete to_minimize // while we are processing it. sat_solver_->BlockClauseDeletion(true); + absl::Cleanup unblock_clause_deletion = [&] { + sat_solver_->BlockClauseDeletion(false); + }; const auto old_counter = counters_; - int num_resets = 0; - while (!time_limit_->LimitReached() && - time_limit_->GetElapsedDeterministicTime() < threshold) { - SatClause* to_minimize = clause_manager_->NextNewClauseToMinimize(); - if (!minimize_new_clauses_only && to_minimize == nullptr) { - to_minimize = clause_manager_->NextClauseToMinimize(); - } - - if (to_minimize != nullptr) { - if (!TryToMinimizeClause(to_minimize)) { - sat_solver_->BlockClauseDeletion(false); - return false; - } - } else if (minimize_new_clauses_only) { - break; - } else { - ++num_resets; - if (log_info) { - SOLVER_LOG(logger_, - "Minimized all clauses, restarting from first one."); - } - clause_manager_->ResetToMinimizeIndex(); - if (num_resets > 1) break; - } - + const int num_resets = clause_manager_->NumToMinimizeIndexResets(); + while (!time_limit_->LimitReached()) { + // Abort if we used our budget. sat_solver_->AdvanceDeterministicTime(time_limit_); + if (time_limit_->GetElapsedDeterministicTime() >= threshold) break; + + // Also abort if we did more than one loop over all the clause. + if (clause_manager_->NumToMinimizeIndexResets() > num_resets + 1) break; + + // First minimize clauses that where never minimized before. + { + SatClause* to_minimize = clause_manager_->NextNewClauseToMinimize(); + if (to_minimize != nullptr) { + if (!TryToMinimizeClause(to_minimize)) return false; + continue; + } + if (minimize_new_clauses_only) break; // We are done. + } + + SatClause* clause = clause_manager_->NextClauseToMinimize(); + if (clause != nullptr) { + if (!TryToMinimizeClause(clause)) return false; + } } // Note(user): In some corner cases, the function above might find a @@ -85,8 +87,8 @@ bool Vivifier::MinimizeByPropagation(bool log_info, double dtime_budget, counters_.num_removed_literals - old_counter.num_removed_literals; timer.AddCounter("num_vivifed", last_num_vivified_); timer.AddCounter("literals_removed", last_num_literals_removed_); + timer.AddCounter("loops", clause_manager_->NumToMinimizeIndexResets()); - sat_solver_->BlockClauseDeletion(false); clause_manager_->DeleteRemovedClauses(); return result; } @@ -171,6 +173,7 @@ bool Vivifier::SubsumptionIsInteresting(BooleanVariable variable, // that we can reuse the trail from previous calls in case there are overlaps. bool Vivifier::TryToMinimizeClause(SatClause* clause) { CHECK(clause != nullptr); + if (clause->empty()) return true; ++counters_.num_clauses_vivified; // TODO(user): Make sure clause do not contain any redundant literal before @@ -229,8 +232,10 @@ bool Vivifier::TryToMinimizeClause(SatClause* clause) { } CHECK_EQ(candidate.size(), clause->size()); - if (!sat_solver_->BacktrackAndPropagateReimplications(longest_valid_prefix)) + if (!sat_solver_->BacktrackAndPropagateReimplications(longest_valid_prefix)) { return false; + } + absl::btree_set moved_last; while (!sat_solver_->ModelIsUnsat()) { // We want each literal in candidate to appear last once in our propagation @@ -240,8 +245,9 @@ bool Vivifier::TryToMinimizeClause(SatClause* clause) { const int target_level = MoveOneUnprocessedLiteralLast( moved_last, sat_solver_->CurrentDecisionLevel(), &candidate); if (target_level == -1) break; - if (!sat_solver_->BacktrackAndPropagateReimplications(target_level)) + if (!sat_solver_->BacktrackAndPropagateReimplications(target_level)) { return false; + } fixed_false_literals.clear(); fixed_true_literal = kNoLiteralIndex; @@ -273,9 +279,8 @@ bool Vivifier::TryToMinimizeClause(SatClause* clause) { // Replace the clause with the reason for the literal being true, plus // the literal itself. candidate.clear(); - for (Literal lit : sat_solver_->GetDecisionsFixing( - trail_->Reason(literal.Variable()))) { - candidate.push_back(lit.Negated()); + for (const Literal l : sat_solver_->GetDecisionsFixing({literal})) { + candidate.push_back(l.Negated()); } } else { candidate.resize(variable_level); @@ -289,7 +294,8 @@ bool Vivifier::TryToMinimizeClause(SatClause* clause) { // clauses. If we can subsume this clause by making only 1 additional // clause permanent and that clause is no longer than this one, we will // do so. - if (clause_manager_->ReasonClauseOrNull(literal.Variable()) != clause && + if (parameters_.subsume_during_vivification() && + clause_manager_->ReasonClauseOrNull(literal.Variable()) != clause && SubsumptionIsInteresting(literal.Variable(), candidate.size())) { counters_.num_subsumed++; counters_.num_removed_literals += clause->size(); @@ -305,7 +311,10 @@ bool Vivifier::TryToMinimizeClause(SatClause* clause) { sat_solver_->EnqueueDecisionAndBackjumpOnConflict(literal.Negated()); if (sat_solver_->ModelIsUnsat()) return false; if (clause->IsRemoved()) return true; + if (sat_solver_->CurrentDecisionLevel() < level) { + ++counters_.num_conflicts; + // There was a conflict, consider the conflicting literal next so we // should be able to exploit the conflict in the next iteration. // TODO(user): I *think* this is sufficient to ensure pushing @@ -321,6 +330,9 @@ bool Vivifier::TryToMinimizeClause(SatClause* clause) { sat_solver_->NotifyThatModelIsUnsat(); return false; } + + // TODO(user): To use this, we need to proove and rewrite the clause + // on each of its modification. if (!parameters_.inprocessing_minimization_use_all_orderings()) break; moved_last.insert(candidate.back().Index()); } @@ -396,15 +408,11 @@ bool Vivifier::TryToMinimizeClause(SatClause* clause) { sat_solver_->NotifyThatModelIsUnsat(); return false; } - // Adding a unit clause can cause additional propagation, but there is also an - // edge case where binary_clauses_->PropagationIsDone() may return - // false after we add the first binary clause, even if nothing has been added - // to the trail. Either way, we can just check if the implication graph thinks - // it is done to propagate only when required. - if (!binary_clauses_->PropagationIsDone(*trail_)) { - return sat_solver_->FinishPropagation(); - } - return true; + + // Adding a unit clause can cause additional propagation. There is also an + // edge case where we added the first binary clause of the model by + // strenghtening a normal clause. + return sat_solver_->FinishPropagation(); } } // namespace operations_research::sat diff --git a/ortools/sat/vivification.h b/ortools/sat/vivification.h index 63ac4bf9ae..9064f80424 100644 --- a/ortools/sat/vivification.h +++ b/ortools/sat/vivification.h @@ -45,6 +45,7 @@ class Vivifier { trail_(model->GetOrCreate()), binary_clauses_(model->GetOrCreate()), clause_manager_(model->GetOrCreate()), + clause_id_generator_(model->GetOrCreate()), lrat_proof_handler_(model->Mutable()) {} // Minimize a batch of clauses using propagation. @@ -67,6 +68,7 @@ class Vivifier { int64_t num_subsumed = 0; int64_t num_removed_literals = 0; int64_t num_reused = 0; + int64_t num_conflicts = 0; }; Counters counters() const { return counters_; } @@ -92,7 +94,7 @@ class Vivifier { Trail* trail_; BinaryImplicationGraph* binary_clauses_; ClauseManager* clause_manager_; - + ClauseIdGenerator* clause_id_generator_; LratProofHandler* lrat_proof_handler_ = nullptr; Counters counters_; diff --git a/ortools/sat/work_assignment.cc b/ortools/sat/work_assignment.cc index 30b1aa94a2..7cfdb794ff 100644 --- a/ortools/sat/work_assignment.cc +++ b/ortools/sat/work_assignment.cc @@ -301,7 +301,6 @@ bool SharedTreeManager::SyncTree(ProtoTrail& path) { // We don't rely on these being empty, but we expect them to be. DCHECK(to_close_.empty()); DCHECK(to_update_.empty()); - path.NormalizeImplications(); int prev_level = -1; for (const auto& [node, level] : nodes) { if (level == prev_level) { @@ -1367,6 +1366,8 @@ bool SharedTreeWorker::SyncWithSharedTree() { !decision_policy_->GetBestPartialAssignment().empty()) { assigned_tree_.ClearTargetPhase(); for (Literal lit : decision_policy_->GetBestPartialAssignment()) { + // Skip anything assigned at level 0. + if (trail_->Assignment().LiteralIsAssigned(lit)) continue; // If `lit` was last assigned at a shared level, it is implied in the // tree, no need to share its phase. if (trail_->Info(lit.Variable()).level <= assigned_tree_.MaxLevel()) { @@ -1396,6 +1397,12 @@ bool SharedTreeWorker::SyncWithSharedTree() { decision_policy_->SetTargetPolarityIfUnassigned(DecodeDecision(lit)); } decision_policy_->ResetActivitiesToFollowBestPartialAssignment(); + // This seems bizzare after just setting the best partial assignment, + // but this makes phase sharing work even when there is no stable phase in + // the restart strategy, and makes no real difference if there is, since + // the first dive will still try to follow this assignment until the first + // conflict regardless of the restart strategy. + decision_policy_->ClearBestPartialAssignment(); } } // If we commit to this subtree, keep it for at least 1s of dtime. diff --git a/ortools/util/logging.cc b/ortools/util/logging.cc index e063fc2f1f..669deff392 100644 --- a/ortools/util/logging.cc +++ b/ortools/util/logging.cc @@ -112,6 +112,8 @@ void SolverLogger::FlushPendingThrottledLogs(bool ignore_rates) { PresolveTimer::~PresolveTimer() { time_limit_->AdvanceDeterministicTime(work_); + const double dtime = + time_limit_->GetElapsedDeterministicTime() - dtime_at_start_; std::string counter_string; for (const auto& [counter_name, count] : counters_) { @@ -124,7 +126,7 @@ PresolveTimer::~PresolveTimer() { logger_->LogInfo( __FILE__, __LINE__, absl::StrCat(absl::StrFormat(" %.2es", timer_.Get()), - absl::StrFormat(" %.2ed", work_), + absl::StrFormat(" %.2ed", dtime), (WorkLimitIsReached() ? " *" : " "), "[", name_, "]", counter_string, " ", absl::StrJoin(extra_infos_, " "))); } diff --git a/ortools/util/logging.h b/ortools/util/logging.h index 4516a3628e..0884b39010 100644 --- a/ortools/util/logging.h +++ b/ortools/util/logging.h @@ -127,7 +127,10 @@ class SolverLogger { class PresolveTimer { public: PresolveTimer(std::string name, SolverLogger* logger, TimeLimit* time_limit) - : name_(std::move(name)), logger_(logger), time_limit_(time_limit) { + : name_(std::move(name)), + dtime_at_start_(time_limit->GetElapsedDeterministicTime()), + logger_(logger), + time_limit_(time_limit) { timer_.Start(); } @@ -164,6 +167,7 @@ class PresolveTimer { private: const std::string name_; + const double dtime_at_start_; WallTimer timer_; SolverLogger* logger_;