From bc2ab43d036f50e00826ae1847fc17c244e0bb66 Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Mon, 27 Sep 2021 19:40:36 +0200 Subject: [PATCH] [CP-SAT] various fixes for corner cases in presolve, checker; added some presolve for all_diff and bool_xor; internal cleanup --- ortools/sat/cp_model_checker.cc | 4 +- ortools/sat/cp_model_presolve.cc | 119 ++++++++++++++++++++++++++----- ortools/sat/cp_model_solver.cc | 18 ++--- ortools/sat/presolve_context.cc | 15 +++- ortools/sat/presolve_context.h | 18 +++-- ortools/sat/sat_parameters.proto | 14 ++-- ortools/sat/synchronization.cc | 2 +- ortools/sat/synchronization.h | 4 +- 8 files changed, 148 insertions(+), 46 deletions(-) diff --git a/ortools/sat/cp_model_checker.cc b/ortools/sat/cp_model_checker.cc index 893a3ef728..1d846f5448 100644 --- a/ortools/sat/cp_model_checker.cc +++ b/ortools/sat/cp_model_checker.cc @@ -1445,7 +1445,9 @@ bool SolutionIsFeasible(const CpModelProto& model, const CpModelProto* mapping_proto, const std::vector* postsolve_mapping) { if (variable_values.size() != model.variables_size()) { - VLOG(1) << "Wrong number of variables in the solution vector"; + VLOG(1) << "Wrong number of variables (" << variable_values.size() + << ") in the solution vector. It should be " + << model.variables_size() << "."; return false; } diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index 44d076221d..e3d3610992 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/ortools/sat/cp_model_presolve.cc @@ -170,11 +170,41 @@ bool CpModelPresolver::PresolveBoolXor(ConstraintProto* ct) { ct->mutable_bool_xor()->set_literals(new_size++, literal); } - if (new_size == 1) { - context_->UpdateRuleStats("TODO bool_xor: one active literal"); - } else if (new_size == 2) { - context_->UpdateRuleStats("TODO bool_xor: two active literals"); + + if (new_size == 0) { + if (num_true_literals % 2 == 0) { + return context_->NotifyThatModelIsUnsat("bool_xor: always false"); + } else { + context_->UpdateRuleStats("bool_xor: always true"); + return RemoveConstraint(ct); + } + } else if (new_size == 1) { // We can fix the only active literal. + if (num_true_literals % 2 == 0) { + if (!context_->SetLiteralToTrue(ct->bool_xor().literals(0))) { + return context_->NotifyThatModelIsUnsat( + "bool_xor: cannot fix last literal"); + } + } else { + if (!context_->SetLiteralToFalse(ct->bool_xor().literals(0))) { + return context_->NotifyThatModelIsUnsat( + "bool_xor: cannot fix last literal"); + } + } + context_->UpdateRuleStats("bool_xor: one active literal"); + return RemoveConstraint(ct); + } else if (new_size == 2) { // We can simplify the bool_xor. + const int a = ct->bool_xor().literals(0); + const int b = ct->bool_xor().literals(1); + if (num_true_literals % 2 == 0) { // a == not(b). + context_->StoreBooleanEqualityRelation(a, NegatedRef(b)); + } else { // a == b. + context_->StoreBooleanEqualityRelation(a, b); + } + context_->UpdateNewConstraintsVariableUsage(); + context_->UpdateRuleStats("bool_xor: two active literals"); + return RemoveConstraint(ct); } + if (num_true_literals % 2 == 1) { CHECK_NE(true_literal, std::numeric_limits::min()); ct->mutable_bool_xor()->set_literals(new_size++, true_literal); @@ -1658,8 +1688,12 @@ bool CpModelPresolver::RemoveSingletonInLinear(ConstraintProto* ct) { "could be improved."; continue; } + if (!context_->SubstituteVariableInObjective(var, coeff, *ct)) { + if (context_->ModelIsUnsat()) return true; + continue; + } + context_->UpdateRuleStats("linear: singleton column define objective."); - context_->SubstituteVariableInObjective(var, coeff, *ct); context_->MarkVariableAsRemoved(var); *(context_->mapping_model->add_constraints()) = *ct; return RemoveConstraint(ct); @@ -1668,7 +1702,10 @@ bool CpModelPresolver::RemoveSingletonInLinear(ConstraintProto* ct) { // Update the objective and remove the variable from its equality // constraint by expanding its rhs. This might fail if the new linear // objective expression can lead to overflow. - if (!context_->SubstituteVariableInObjective(var, coeff, *ct)) continue; + if (!context_->SubstituteVariableInObjective(var, coeff, *ct)) { + if (context_->ModelIsUnsat()) return true; + continue; + } context_->UpdateRuleStats( "linear: singleton column in equality and in objective."); @@ -1779,7 +1816,9 @@ bool CpModelPresolver::PresolveSmallLinear(ConstraintProto* ct) { if (linear.domain_size() == 2 && linear.domain(0) == linear.domain(1)) { const int64_t value = RefIsPositive(ref) ? linear.domain(0) * coeff : -linear.domain(0) * coeff; - if (context_->StoreLiteralImpliesVarEqValue(literal, var, value)) { + if (!context_->DomainOf(var).Contains(value)) { + if (!context_->SetLiteralToFalse(literal)) return false; + } else if (context_->StoreLiteralImpliesVarEqValue(literal, var, value)) { // The domain is not actually modified, but we want to rescan the // constraints linked to this variable. See TODO below. context_->modified_domains.Set(var); @@ -2659,6 +2698,16 @@ void CpModelPresolver::AddLinearConstraintFromInterval( new_ct->mutable_linear()->add_vars(end); new_ct->mutable_linear()->add_coeffs(-1); CanonicalizeLinear(new_ct); + + if (context_->MinOf(size) < 0) { + CHECK(!ct.enforcement_literal().empty()); + ConstraintProto* positive = context_->working_model->add_constraints(); + *(positive->mutable_enforcement_literal()) = ct.enforcement_literal(); + positive->mutable_linear()->add_domain(0); + positive->mutable_linear()->add_domain(context_->MaxOf(size)); + positive->mutable_linear()->add_vars(size); + positive->mutable_linear()->add_coeffs(1); + } context_->UpdateNewConstraintsVariableUsage(); } @@ -3300,12 +3349,29 @@ bool CpModelPresolver::PresolveAllDiff(ConstraintProto* ct) { } } - std::sort(new_variables.begin(), new_variables.end()); + std::sort(new_variables.begin(), new_variables.end(), + [](int ref_a, int ref_b) { + const int var_a = PositiveRef(ref_a); + const int var_b = PositiveRef(ref_b); + return std::tie(var_a, ref_a) < std::tie(var_b, ref_b); + }); for (int i = 1; i < new_variables.size(); ++i) { if (new_variables[i] == new_variables[i - 1]) { return context_->NotifyThatModelIsUnsat( "Duplicate variable in all_diff"); } + if (new_variables[i] == NegatedRef(new_variables[i - 1])) { + bool domain_modified = false; + if (!context_->IntersectDomainWith(PositiveRef(new_variables[i]), + Domain(0).Complement(), + &domain_modified)) { + return false; + } + if (domain_modified) { + context_->UpdateRuleStats( + "all_diff: remove 0 from variable appearing with its opposite."); + } + } } if (new_variables.size() < all_diff.vars_size()) { @@ -4123,6 +4189,7 @@ bool CpModelPresolver::PresolveRoutes(ConstraintProto* ct) { if (HasEnforcementLiteral(*ct)) return false; RoutesConstraintProto& proto = *ct->mutable_routes(); + const int old_size = proto.literals_size(); int new_size = 0; std::vector has_incoming_or_outgoing_arcs; const int num_arcs = proto.literals_size(); @@ -4147,6 +4214,15 @@ bool CpModelPresolver::PresolveRoutes(ConstraintProto* ct) { has_incoming_or_outgoing_arcs[tail] = true; has_incoming_or_outgoing_arcs[head] = true; } + + if (old_size > 0 && new_size == 0) { + // A routes constraint cannot have a self loop on 0. Therefore, if there + // were arcs, it means it contains non zero nodes. Without arc, the + // constraint is unfeasible. + return context_->NotifyThatModelIsUnsat( + "routes: graph with nodes and no arcs"); + } + if (new_size < num_arcs) { proto.mutable_literals()->Truncate(new_size); proto.mutable_tails()->Truncate(new_size); @@ -4690,6 +4766,8 @@ void CpModelPresolver::ExtractBoolAnd() { } } +// TODO(user): It might make sense to run this in parallel. The same apply for +// other expansive and self-contains steps like symmetry detection, etc... void CpModelPresolver::Probe() { if (context_->ModelIsUnsat()) return; @@ -4977,7 +5055,7 @@ void CpModelPresolver::PresolvePureSatPart() { void CpModelPresolver::ExpandObjective() { if (context_->ModelIsUnsat()) return; - // The objective is already loaded in the constext, but we re-canonicalize + // The objective is already loaded in the context, but we re-canonicalize // it with the latest information. if (!context_->CanonicalizeObjective()) { (void)context_->NotifyThatModelIsUnsat(); @@ -5120,16 +5198,19 @@ void CpModelPresolver::ExpandObjective() { } if (expanded_linear_index != -1) { - context_->UpdateRuleStats("objective: expanded objective constraint."); - // Update the objective map. Note that the division is possible because // currently we only expand with coeff with a magnitude of 1. CHECK_EQ(std::abs(objective_coeff_in_expanded_constraint), 1); const ConstraintProto& ct = context_->working_model->constraints(expanded_linear_index); - context_->SubstituteVariableInObjective( - objective_var, objective_coeff_in_expanded_constraint, ct, - &new_vars_in_objective); + if (!context_->SubstituteVariableInObjective( + objective_var, objective_coeff_in_expanded_constraint, ct, + &new_vars_in_objective)) { + if (context_->ModelIsUnsat()) return; + continue; + } + + context_->UpdateRuleStats("objective: expanded objective constraint."); // Add not yet processed new variables. for (const int var : new_vars_in_objective) { @@ -5426,13 +5507,13 @@ bool CpModelPresolver::PresolveOneConstraint(int c) { // PropagateDomainsInLinear(). // // TODO(user): The move in only one direction code is redundant with the - // dual bound strengthening code. So maybe we don't need both. Especially - // since the implementation here is a bit hacky. + // dual bound strengthening code. So maybe we don't need both. for (const int ref : ct->linear().vars()) { const int var = PositiveRef(ref); context_->var_to_lb_only_constraints[var].erase(c); context_->var_to_ub_only_constraints[var].erase(c); } + if (CanonicalizeLinear(ct)) { context_->UpdateConstraintVariableUsage(c); } @@ -5458,7 +5539,7 @@ bool CpModelPresolver::PresolveOneConstraint(int c) { if (PresolveLinearOnBooleans(ct)) { context_->UpdateConstraintVariableUsage(c); } - if (ct->constraint_case() == ConstraintProto::ConstraintCase::kLinear) { + if (ct->constraint_case() == ConstraintProto::kLinear) { const int old_num_enforcement_literals = ct->enforcement_literal_size(); ExtractEnforcementLiteralFromLinearConstraint(c, ct); if (ct->constraint_case() == @@ -7202,7 +7283,7 @@ std::vector> FindDuplicateConstraints( // We use a map hash: serialized_constraint_proto hash -> constraint index. ConstraintProto copy; - absl::flat_hash_map equiv_constraints; + absl::flat_hash_map equiv_constraints; std::string s; const int num_constraints = model_proto.constraints().size(); @@ -7218,7 +7299,7 @@ std::vector> FindDuplicateConstraints( copy = CopyConstraintForDuplicateDetection(model_proto.constraints(c)); s = copy.SerializeAsString(); - const int64_t hash = absl::Hash()(s); + const uint64_t hash = absl::Hash()(s); const auto [it, inserted] = equiv_constraints.insert({hash, c}); if (!inserted) { // Already present! diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index f349f7d749..44882b9d78 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -103,12 +103,12 @@ ABSL_FLAG(bool, cp_model_dump_models, false, "DEBUG ONLY. When set to true, SolveCpModel() will dump its model " "protos (original model, presolved model, mapping model) in text " "format to 'FLAGS_cp_model_dump_prefix'{model|presolved_model|" - "mapping_model}.pbtxt."); + "mapping_model}.pb.txt."); ABSL_FLAG(bool, cp_model_dump_lns, false, "DEBUG ONLY. When set to true, solve will dump all " "lns models proto in text format to " - "'FLAGS_cp_model_dump_prefix'lns_xxx.pbtxt."); + "'FLAGS_cp_model_dump_prefix'lns_xxx.pb.txt."); ABSL_FLAG( bool, cp_model_dump_problematic_lns, false, @@ -118,7 +118,7 @@ ABSL_FLAG( ABSL_FLAG(bool, cp_model_dump_response, false, "DEBUG ONLY. If true, the final response of each solve will be " - "dumped to 'FLAGS_cp_model_dump_prefix'response.pbtxt"); + "dumped to 'FLAGS_cp_model_dump_prefix'response.pb.txt"); ABSL_FLAG(std::string, cp_model_params, "", "This is interpreted as a text SatParameters proto. The " @@ -2449,7 +2449,7 @@ class LnsSolver : public SubSolver { // TODO(user): export the delta too if needed. const std::string lns_name = absl::StrCat(absl::GetFlag(FLAGS_cp_model_dump_prefix), - lns_fragment.name(), ".pbtxt"); + lns_fragment.name(), ".pb.txt"); LOG(INFO) << "Dumping LNS model to '" << lns_name << "'."; CHECK_OK(file::SetTextProto(lns_name, lns_fragment, file::Defaults())); } @@ -2551,7 +2551,7 @@ class LnsSolver : public SubSolver { if (absl::GetFlag(FLAGS_cp_model_dump_problematic_lns)) { const std::string name = absl::StrCat(absl::GetFlag(FLAGS_cp_model_dump_prefix), - debug_copy.name(), ".pbtxt"); + debug_copy.name(), ".pb.txt"); LOG(INFO) << "Dumping problematic LNS model to '" << name << "'."; CHECK_OK(file::SetTextProto(name, debug_copy, file::Defaults())); } @@ -2907,7 +2907,7 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) { // Dump initial model? if (absl::GetFlag(FLAGS_cp_model_dump_models)) { const std::string file = - absl::StrCat(absl::GetFlag(FLAGS_cp_model_dump_prefix), "model.pbtxt"); + absl::StrCat(absl::GetFlag(FLAGS_cp_model_dump_prefix), "model.pb.txt"); LOG(INFO) << "Dumping cp model proto to '" << file << "'."; CHECK_OK(file::SetTextProto(file, model_proto, file::Defaults())); } @@ -3143,7 +3143,7 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) { for (int i = 0; i < model_proto.solution_hint().vars_size(); ++i) { const int ref = model_proto.solution_hint().vars(i); const int64_t value = model_proto.solution_hint().values(i); - solution[PositiveRef(ref)] = RefIsPositive(ref) ? value : CapOpp(value); + solution[PositiveRef(ref)] = RefIsPositive(ref) ? value : -value; } if (SolutionIsFeasible(model_proto, solution)) { SOLVER_LOG(context->logger(), @@ -3293,14 +3293,14 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) { #if !defined(__PORTABLE_PLATFORM__) if (absl::GetFlag(FLAGS_cp_model_dump_models)) { const std::string presolved_file = absl::StrCat( - absl::GetFlag(FLAGS_cp_model_dump_prefix), "presolved_model.pbtxt"); + absl::GetFlag(FLAGS_cp_model_dump_prefix), "presolved_model.pb.txt"); LOG(INFO) << "Dumping presolved cp model proto to '" << presolved_file << "'."; CHECK_OK(file::SetTextProto(presolved_file, new_cp_model_proto, file::Defaults())); const std::string mapping_file = absl::StrCat( - absl::GetFlag(FLAGS_cp_model_dump_prefix), "mapping_model.pbtxt"); + absl::GetFlag(FLAGS_cp_model_dump_prefix), "mapping_model.pb.txt"); LOG(INFO) << "Dumping mapping cp model proto to '" << mapping_file << "'."; CHECK_OK(file::SetTextProto(mapping_file, mapping_proto, file::Defaults())); } diff --git a/ortools/sat/presolve_context.cc b/ortools/sat/presolve_context.cc index 4c77f4bee0..eab3934e15 100644 --- a/ortools/sat/presolve_context.cc +++ b/ortools/sat/presolve_context.cc @@ -1127,10 +1127,14 @@ void PresolveContext::CanonicalizeDomainOfSizeTwo(int var) { void PresolveContext::InsertVarValueEncodingInternal(int literal, int var, int64_t value, bool add_constraints) { + CHECK(RefIsPositive(var)); CHECK(!VariableWasRemoved(literal)); CHECK(!VariableWasRemoved(var)); absl::flat_hash_map& var_map = encoding_[var]; + // The code below is not 100% correct if this is not the case. + DCHECK(DomainOf(var).Contains(value)); + // Ticky and rare: I have only observed this on the LNS of // radiation_m18_12_05_sat.fzn. The value was encoded, but maybe we never // used the involved variables / constraints, so it was removed (with the @@ -1159,6 +1163,8 @@ void PresolveContext::InsertVarValueEncodingInternal(int literal, int var, } if (DomainOf(var).Size() == 2) { + // TODO(user): There is a bug here if the var == value was not in the + // domain, it will just be ignored. CanonicalizeDomainOfSizeTwo(var); } else { VLOG(2) << "Insert lit(" << literal << ") <=> var(" << var @@ -1213,12 +1219,15 @@ bool PresolveContext::CanonicalizeEncoding(int* ref, int64_t* value) { return true; } -void PresolveContext::InsertVarValueEncoding(int literal, int ref, +bool PresolveContext::InsertVarValueEncoding(int literal, int ref, int64_t value) { - if (!RemapEncodingMaps()) return; - if (!CanonicalizeEncoding(&ref, &value)) return; + if (!RemapEncodingMaps()) return false; + if (!CanonicalizeEncoding(&ref, &value)) { + return SetLiteralToFalse(literal); + } literal = GetLiteralRepresentative(literal); InsertVarValueEncodingInternal(literal, ref, value, /*add_constraints=*/true); + return true; } bool PresolveContext::StoreLiteralImpliesVarEqValue(int literal, int var, diff --git a/ortools/sat/presolve_context.h b/ortools/sat/presolve_context.h index f32ac99c69..75ef957987 100644 --- a/ortools/sat/presolve_context.h +++ b/ortools/sat/presolve_context.h @@ -70,8 +70,7 @@ class SavedVariable { // in-memory domain of each variables and the constraint variable graph. class PresolveContext { public: - explicit PresolveContext(Model* model, CpModelProto* cp_model, - CpModelProto* mapping) + PresolveContext(Model* model, CpModelProto* cp_model, CpModelProto* mapping) : working_model(cp_model), mapping_model(mapping), logger_(model->GetOrCreate()), @@ -80,6 +79,9 @@ 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. int NewIntVar(const Domain& domain); int NewBoolVar(); int GetOrCreateConstantVar(int64_t cst); @@ -269,7 +271,13 @@ class PresolveContext { // Important: This does not update the constraint<->variable graph, so // ConstraintVariableGraphIsUpToDate() will be false until // UpdateNewConstraintsVariableUsage() is called. - void InsertVarValueEncoding(int literal, int ref, int64_t value); + // + // Returns false if the model become UNSAT. + // + // TODO(user): This function is not always correct if + // !context->DomainOf(ref).contains(value), we could make it correct but it + // might be a bit expansive to do so. For now we just have a DCHECK(). + bool InsertVarValueEncoding(int literal, int ref, int64_t value); // Gets the associated literal if it is already created. Otherwise // create it, add the corresponding constraints and returns it. @@ -337,7 +345,7 @@ class PresolveContext { // satisfy our overflow preconditions. Note that this can only happen if the // substitued variable is not implied free (i.e. if its domain is smaller than // the implied domain from the equality). - bool SubstituteVariableInObjective( + ABSL_MUST_USE_RESULT bool SubstituteVariableInObjective( int var_in_equality, int64_t coeff_in_equality, const ConstraintProto& equality, std::vector* new_vars_in_objective = nullptr); @@ -476,7 +484,7 @@ class PresolveContext { // Makes sure we only insert encoding about the current representative. // // Returns false if ref cannot take the given value (it might not have been - // propagated yed). + // propagated yet). bool CanonicalizeEncoding(int* ref, int64_t* value); // Inserts an half reified var value encoding (literal => var ==/!= value). diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto index ab2cd67f2d..42a2d56e9b 100644 --- a/ortools/sat/sat_parameters.proto +++ b/ortools/sat/sat_parameters.proto @@ -842,12 +842,12 @@ message SatParameters { optional bool optimize_with_max_hs = 85 [default = false]; // Whether we enumerate all solutions of a problem without objective. Note - // that setting this to true automatically disable the presolve. This is - // because the presolve rules only guarantee the existence of one feasible - // solution to the presolved problem. + // that setting this to true automatically disable some presolve reduction + // that can remove feasible solution. That is it has the same effect as + // setting keep_all_feasible_solutions_in_presolve. // - // TODO(user): Do not disable the presolve and let the user choose what - // behavior is best by setting keep_all_feasible_solutions_in_presolve. + // TODO(user): Do not do that and let the user choose what behavior is best by + // setting keep_all_feasible_solutions_in_presolve ? optional bool enumerate_all_solutions = 87 [default = false]; // If true, we disable the presolve reductions that remove feasible solutions @@ -868,7 +868,9 @@ message SatParameters { optional bool fill_tightened_domains_in_response = 132 [default = false]; // If true, the solver will add a default integer branching strategy to the - // already defined search strategy. + // already defined search strategy. If not, some variable might still not be + // fixed at the end of the search. For now we assume these variable can just + // be set to their lower bound. optional bool instantiate_all_variables = 106 [default = true]; // If true, then the precedences propagator try to detect for each variable if diff --git a/ortools/sat/synchronization.cc b/ortools/sat/synchronization.cc index 99a1adbfcc..7443aeb46e 100644 --- a/ortools/sat/synchronization.cc +++ b/ortools/sat/synchronization.cc @@ -534,7 +534,7 @@ void SharedResponseManager::NewSolution(const CpSolverResponse& response, // another solution manager, and we do not want to dump those. if (absl::GetFlag(FLAGS_cp_model_dump_solutions)) { const std::string file = - absl::StrCat(dump_prefix_, "solution_", num_solutions_, ".pbtxt"); + absl::StrCat(dump_prefix_, "solution_", num_solutions_, ".pb.txt"); LOG(INFO) << "Dumping solution to '" << file << "'."; CHECK_OK(file::SetTextProto(file, best_response_, file::Defaults())); } diff --git a/ortools/sat/synchronization.h b/ortools/sat/synchronization.h index 9a49f8e8c1..28c031c3f3 100644 --- a/ortools/sat/synchronization.h +++ b/ortools/sat/synchronization.h @@ -59,7 +59,7 @@ class SharedSolutionRepository { // this rank is actually the unscaled internal minimization objective. // Remove this assumptions by simply recomputing this value since it is not // too costly to do so. - int64_t rank; + int64_t rank = 0; std::vector variable_values; @@ -536,7 +536,7 @@ void SharedSolutionRepository::Synchronize() { // We use a stable sort to keep the num_selected count for the already // existing solutions. // - // TODO(user): Intoduce a notion of orthogonality to diversify the pool? + // TODO(user): Introduce a notion of orthogonality to diversify the pool? gtl::STLStableSortAndRemoveDuplicates(&solutions_); if (solutions_.size() > num_solutions_to_keep_) { solutions_.resize(num_solutions_to_keep_);