diff --git a/ortools/sat/BUILD.bazel b/ortools/sat/BUILD.bazel index afe3fd67f5..efc5e01fdc 100644 --- a/ortools/sat/BUILD.bazel +++ b/ortools/sat/BUILD.bazel @@ -336,6 +336,8 @@ cc_library( "//ortools/util:sorted_interval_list", "//ortools/util:strong_integers", "@com_google_absl//absl/container:flat_hash_map", + "@com_google_absl//absl/random", + "@com_google_absl//absl/random:bit_gen_ref", ], ) diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index 7e30f0098a..50870bef74 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/ortools/sat/cp_model_presolve.cc @@ -6146,13 +6146,12 @@ void CpModelPresolver::PresolvePureSatPart() { } if (ct.constraint_case() == ConstraintProto::kBoolAnd) { - // We currently preserve these "complex" bool_and since their linear - // relaxation can be stronger than the part. - // - // TODO(user): Find a way to presolve that here but recover them later - // from their clause representation? - if (ct.enforcement_literal().size() > 1 && - ct.bool_and().literals().size() > 1) { + // We currently do not expand "complex" bool_and that would result + // in too many literals. + const int left_size = ct.enforcement_literal().size(); + const int right_size = ct.bool_and().literals().size(); + if (left_size > 1 && right_size > 1 && + (left_size + 1) * right_size > 1000) { continue; } @@ -9503,6 +9502,106 @@ void CopyEverythingExceptVariablesAndConstraintsFieldsIntoContext( } } +// TODO(user): Use better heuristic where we look at at most one. +void CpModelPresolver::MergeClauses() { + if (context_->ModelIsUnsat()) return; + ClauseWithOneMissingHasher hasher(*context_->random()); + + WallTimer wall_timer; + wall_timer.Start(); + int64_t work_done = 0; + const int64_t work_limit = 1e8; + + std::vector to_clean; + + int64_t num_collisions = 0; + int64_t num_merges = 0; + int64_t num_saved_literals = 0; + + absl::flat_hash_map> detector_map; + const int num_constraints = context_->working_model->constraints_size(); + for (int c = 0; c < num_constraints; ++c) { + ConstraintProto* ct = context_->working_model->mutable_constraints(c); + if (ct->constraint_case() != ConstraintProto::kBoolOr) continue; + + // Both of these test shouldn't happen, but we have them to be safe. + if (!ct->enforcement_literal().empty()) continue; + if (ct->bool_or().literals().size() <= 2) continue; + + std::sort(ct->mutable_bool_or()->mutable_literals()->begin(), + ct->mutable_bool_or()->mutable_literals()->end()); + hasher.RegisterClause(c, ct->bool_or().literals()); + + bool merged = false; + work_done += ct->bool_or().literals().size(); + if (work_done > work_limit) break; + for (const int ref : ct->bool_or().literals()) { + const uint64_t hash = hasher.HashWithout(c, ref); + const auto it = detector_map.find(hash); + if (it != detector_map.end()) { + ++num_collisions; + const int base_c = it->second.first; + auto* and_ct = context_->working_model->mutable_constraints(base_c); + if (ClauseIsEnforcementImpliesLiteral( + ct->bool_or().literals(), and_ct->enforcement_literal(), ref)) { + ++num_merges; + num_saved_literals += ct->bool_or().literals().size() - 1; + merged = true; + and_ct->mutable_bool_and()->add_literals(ref); + ct->Clear(); + context_->UpdateConstraintVariableUsage(c); + break; + } + } + } + + if (!merged) { + // Stupid heuristic: take first literal. + const int ref = ct->bool_or().literals(0); + const uint64_t hash = hasher.HashWithout(c, ref); + const auto [_, inserted] = detector_map.insert({hash, {c, ref}}); + if (inserted) { + to_clean.push_back(c); + context_->tmp_literals.clear(); + for (const int lit : ct->bool_or().literals()) { + if (lit == ref) continue; + context_->tmp_literals.push_back(NegatedRef(lit)); + } + ct->Clear(); + ct->mutable_enforcement_literal()->Assign( + context_->tmp_literals.begin(), context_->tmp_literals.end()); + ct->mutable_bool_and()->add_literals(ref); + } + } + } + + // Retransform to bool_or bool_and with a single rhs. + for (const int c : to_clean) { + ConstraintProto* ct = context_->working_model->mutable_constraints(c); + if (ct->bool_and().literals().size() > 1) { + context_->UpdateConstraintVariableUsage(c); + continue; + } + + // We have a single bool_and, lets transform it back to single bool_or. + context_->tmp_literals.clear(); + context_->tmp_literals.push_back(ct->bool_and().literals(0)); + for (const int ref : ct->enforcement_literal()) { + context_->tmp_literals.push_back(NegatedRef(ref)); + } + ct->Clear(); + ct->mutable_bool_or()->mutable_literals()->Assign( + context_->tmp_literals.begin(), context_->tmp_literals.end()); + } + + if (num_merges > 0) { + SOLVER_LOG(logger_, "[MergeClauses]", " #num_collisions=", num_collisions, + " #num_merges=", num_merges, + " #num_saved_literals=", num_saved_literals, " work=", work_done, + "/", work_limit, " time=", wall_timer.Get(), "s"); + } +} + // ============================================================================= // Public API. // ============================================================================= @@ -9710,6 +9809,13 @@ CpSolverStatus CpModelPresolver::Presolve() { ProcessSetPPC(); if (context_->ModelIsUnsat()) return InfeasibleStatus(); + // We do that after the duplicate, SAT and SetPPC constraints. + if (!context_->time_limit()->LimitReached()) { + // Merge clauses that differ in just one literal. + // Heuristic use at_most_one to try to tighten the initial LP Relaxation. + MergeClauses(); + } + // TODO(user): Decide where is the best place for this. Fow now we do it // after max clique to get all the bool_and converted to at most ones. if (context_->params().symmetry_level() > 0 && !context_->ModelIsUnsat() && diff --git a/ortools/sat/cp_model_presolve.h b/ortools/sat/cp_model_presolve.h index 831ceed91e..f43c0160ed 100644 --- a/ortools/sat/cp_model_presolve.h +++ b/ortools/sat/cp_model_presolve.h @@ -253,6 +253,19 @@ class CpModelPresolver { void MergeNoOverlapConstraints(); + // Heuristic to merge clauses that differ in only one literal. + // The idea is to regroup a bunch of clauses into a single bool_and. + // This serves a bunch of purpose: + // - Smaller model. + // - Stronger dual reasoning since less locks. + // - If the negation of the rhs of the bool_and are in at most one, we will + // have a stronger LP relaxation. + // + // TODO(user): If the merge procedure is successful we might want to develop + // a custom propagators for such bool_and. It should in theory be more + // efficient than the two watcher literal scheme for clauses. Investigate! + void MergeClauses(); + // Boths function are responsible for dealing with affine relations. // The second one returns false on UNSAT. void EncodeAllAffineRelations(); diff --git a/ortools/sat/cuts.cc b/ortools/sat/cuts.cc index 85090419b9..0b73ff1649 100644 --- a/ortools/sat/cuts.cc +++ b/ortools/sat/cuts.cc @@ -658,7 +658,8 @@ void IntegerRoundingCutHelper::ComputeCut( best_cut_.max_magnitude = std::max(best_cut_.max_magnitude, IntTypeAbs(new_coeff)); } - best_cut_.max_magnitude = std::max(best_cut_.max_magnitude, best_cut_.rhs); + best_cut_.max_magnitude = + std::max(best_cut_.max_magnitude, IntTypeAbs(best_cut_.rhs)); // Create the base super-additive function f(). const IntegerValue rhs_remainder = diff --git a/ortools/sat/lp_utils.cc b/ortools/sat/lp_utils.cc index f9085ef1de..84c9e0a3e0 100644 --- a/ortools/sat/lp_utils.cc +++ b/ortools/sat/lp_utils.cc @@ -270,7 +270,9 @@ void RemoveNearZeroTerms(const SatParameters& params, MPModelProto* mp_model, const int var = ct->var_index(i); const double coeff = ct->coefficient(i); if (std::abs(coeff) * max_bounds[var] < threshold) { - largest_removed = std::max(largest_removed, std::abs(coeff)); + if (max_bounds[var] != 0) { + largest_removed = std::max(largest_removed, std::abs(coeff)); + } continue; } ct->set_var_index(new_size, var); @@ -282,6 +284,23 @@ void RemoveNearZeroTerms(const SatParameters& params, MPModelProto* mp_model, ct->mutable_coefficient()->Truncate(new_size); } + // We also do the same for the objective coefficient. + if (num_variables > 0) { + const double threshold = + params.mip_wanted_precision() / static_cast(num_variables); + for (int var = 0; var < num_variables; ++var) { + const double coeff = mp_model->variable(var).objective_coefficient(); + if (coeff == 0.0) continue; + if (std::abs(coeff) * max_bounds[var] < threshold) { + ++num_removed; + if (max_bounds[var] != 0) { + largest_removed = std::max(largest_removed, std::abs(coeff)); + } + mp_model->mutable_variable(var)->clear_objective_coefficient(); + } + } + } + if (num_removed > 0) { // Note that when a variable is fixed to zero, the code here remove all its // coefficients, so the largest magnitude can be quite large. diff --git a/ortools/sat/presolve_util.cc b/ortools/sat/presolve_util.cc index 8f895db1ea..1f2ac82244 100644 --- a/ortools/sat/presolve_util.cc +++ b/ortools/sat/presolve_util.cc @@ -564,5 +564,21 @@ bool ActivityBoundHelper::PresolveEnforcement( return true; } +void ClauseWithOneMissingHasher::RegisterClause(int c, + absl::Span clause) { + uint64_t hash = 0; + for (const int ref : clause) { + const Index index = IndexFromLiteral(ref); + while (index >= literal_to_hash_.size()) { + // We use random value for a literal hash. + literal_to_hash_.push_back(absl::Uniform(random_)); + } + hash ^= literal_to_hash_[index]; + } + + if (c >= clause_to_hash_.size()) clause_to_hash_.resize(c + 1, 0); + clause_to_hash_[c] = hash; +} + } // namespace sat } // namespace operations_research diff --git a/ortools/sat/presolve_util.h b/ortools/sat/presolve_util.h index 240ec1071b..5d5dd9f644 100644 --- a/ortools/sat/presolve_util.h +++ b/ortools/sat/presolve_util.h @@ -21,6 +21,8 @@ #include #include "absl/container/flat_hash_map.h" +#include "absl/random/bit_gen_ref.h" +#include "absl/random/random.h" #include "absl/strings/string_view.h" #include "absl/types/span.h" #include "ortools/base/integral_types.h" @@ -201,6 +203,54 @@ class ActivityBoundHelper { absl::flat_hash_set triggered_amo_; }; +// Class to help detects clauses that differ on a single literal. +class ClauseWithOneMissingHasher { + public: + explicit ClauseWithOneMissingHasher(absl::BitGenRef random) + : random_(random) {} + + // We use the proto encoding of literals here. + void RegisterClause(int c, absl::Span clause); + + // Get a hash of the clause with index c and literal ref removed. + // This assumes that ref was part of the clause. Work in O(1). + uint64_t HashWithout(int c, int ref) const { + return clause_to_hash_[c] ^ literal_to_hash_[IndexFromLiteral(ref)]; + } + + private: + DEFINE_STRONG_INDEX_TYPE(Index); + Index IndexFromLiteral(int ref) const { + return Index(ref >= 0 ? 2 * ref : -2 * ref - 1); + } + + absl::BitGenRef random_; + absl::StrongVector literal_to_hash_; + std::vector clause_to_hash_; +}; + +// Specific function. Returns true if the negation of all literals in clause +// except literal is exactly equal to the literal of enforcement. +// +// We assumes that enforcement and negated(clause) are sorted lexicographically +// Or negated(enforcement) and clause. Both option works. If not, we will only +// return false more often. When we return true, the property is enforced. +// +// TODO(user): For the same complexity, we do not need to specify literal and +// can recover it. +inline bool ClauseIsEnforcementImpliesLiteral(absl::Span clause, + absl::Span enforcement, + int literal) { + if (clause.size() != enforcement.size() + 1) return false; + int j = 0; + for (int i = 0; i < clause.size(); ++i) { + if (clause[i] == literal) continue; + if (clause[i] != NegatedRef(enforcement[j])) return false; + ++j; + } + return true; +} + } // namespace sat } // namespace operations_research