From ad194e85fbb5d98c61823bbf78124d8306d9d0f9 Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Thu, 19 Nov 2020 18:12:18 +0100 Subject: [PATCH] polish probing code --- ortools/sat/cp_model_search.cc | 1 + ortools/sat/cp_model_solver.cc | 8 +-- ortools/sat/integer_search.cc | 68 +++++++++++++----------- ortools/sat/probing.cc | 88 ++++++++++++++++---------------- ortools/sat/probing.h | 83 ++++++++++++++++-------------- ortools/sat/sat_parameters.proto | 2 +- ortools/sat/synchronization.cc | 10 ++-- 7 files changed, 139 insertions(+), 121 deletions(-) diff --git a/ortools/sat/cp_model_search.cc b/ortools/sat/cp_model_search.cc index 3ea4419989..e7ca1d88f5 100644 --- a/ortools/sat/cp_model_search.cc +++ b/ortools/sat/cp_model_search.cc @@ -342,6 +342,7 @@ std::vector GetDiverseSetOfParameters( SatParameters new_params = base_params; new_params.set_search_branching(SatParameters::AUTOMATIC_SEARCH); new_params.set_use_probing_search(true); + new_params.set_linearization_level(0); strategies["probing"] = new_params; } diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index 5279d5eac8..cdb169c1c3 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -1554,11 +1554,13 @@ void SolveLoadedCpModel(const CpModelProto& model_proto, std::vector bool_vars; std::vector int_vars; IntegerTrail* integer_trail = model->GetOrCreate(); + absl::flat_hash_set visited; for (int v = 0; v < model_proto.variables_size(); ++v) { if (mapping.IsBoolean(v)) { - const Literal literal = mapping.Literal(v); - if (literal.IsPositive()) { - bool_vars.push_back(literal.Variable()); + const BooleanVariable bool_var = mapping.Literal(v).Variable(); + if (!visited.contains(bool_var)) { + visited.insert(bool_var); + bool_vars.push_back(bool_var); } } else { IntegerVariable var = mapping.Integer(v); diff --git a/ortools/sat/integer_search.cc b/ortools/sat/integer_search.cc index e4f9d8314c..d23d34e7c0 100644 --- a/ortools/sat/integer_search.cc +++ b/ortools/sat/integer_search.cc @@ -783,10 +783,9 @@ SatSolver::Status SolveIntegerProblem(Model* model) { ++num_decisions_without_probing >= sat_parameters.probing_period_at_root()) { num_decisions_without_probing = 0; - // TODO(user): Be smarter about what variables we probe, we can also - // do more than one. - if (!prober->ClearStatisticsAndResetSearch() || - !prober->ProbeOneVariable(Literal(decision).Variable())) { + // TODO(user,user): Be smarter about what variables we probe, we can + // also do more than one. + if (!prober->ProbeOneVariable(Literal(decision).Variable())) { return SatSolver::INFEASIBLE; } DCHECK_EQ(sat_solver->CurrentDecisionLevel(), 0); @@ -936,7 +935,7 @@ SatSolver::Status ContinuousProbing( int loop = 0; while (!time_limit->LimitReached()) { - VLOG(1) << "Loop " << loop++; + VLOG(1) << "Probing loop " << loop++; // Sync the bounds first. auto SyncBounds = [solver, &level_zero_callbacks]() { @@ -956,28 +955,39 @@ SatSolver::Status ContinuousProbing( return SatSolver::INFEASIBLE; } + // TODO(user): Explore fast probing methods. + + // Probe each Boolean variable at most once per loop. + absl::flat_hash_set probed; + // Probe variable bounds. + // TODO(user,user): Probe optional variables. for (const IntegerVariable int_var : int_vars) { if (integer_trail->IsFixed(int_var) || integer_trail->IsOptional(int_var)) { continue; } - IntegerLiteral fix_to_lb = IntegerLiteral::LowerOrEqual( - int_var, integer_trail->LowerBound(int_var)); - const Literal shave_lb = encoder->GetOrCreateAssociatedLiteral(fix_to_lb); - if (shave_lb.IsPositive()) { - if (!prober->ClearStatisticsAndResetSearch() || - !prober->ProbeOneVariable(shave_lb.Variable())) { + + const BooleanVariable shave_lb = + encoder + ->GetOrCreateAssociatedLiteral(IntegerLiteral::LowerOrEqual( + int_var, integer_trail->LowerBound(int_var))) + .Variable(); + if (!probed.contains(shave_lb)) { + probed.insert(shave_lb); + if (!prober->ProbeOneVariable(shave_lb)) { return SatSolver::INFEASIBLE; } } - IntegerLiteral fix_to_ub = IntegerLiteral::GreaterOrEqual( - int_var, integer_trail->UpperBound(int_var)); - const Literal shave_ub = encoder->GetOrCreateAssociatedLiteral(fix_to_ub); - if (shave_ub.IsPositive()) { - if (!prober->ClearStatisticsAndResetSearch() || - !prober->ProbeOneVariable(shave_ub.Variable())) { + const BooleanVariable shave_ub = + encoder + ->GetOrCreateAssociatedLiteral(IntegerLiteral::GreaterOrEqual( + int_var, integer_trail->UpperBound(int_var))) + .Variable(); + if (!probed.contains(shave_ub)) { + probed.insert(shave_ub); + if (!prober->ProbeOneVariable(shave_ub)) { return SatSolver::INFEASIBLE; } } @@ -985,25 +995,25 @@ SatSolver::Status ContinuousProbing( if (!SyncBounds()) { return SatSolver::INFEASIBLE; } + if (time_limit->LimitReached()) { + return SatSolver::LIMIT_REACHED; + } } // Probe Boolean variables from the model. - int count = 0; for (const BooleanVariable& bool_var : bool_vars) { - if (!solver->Assignment().LiteralIsAssigned(Literal(bool_var, true))) { - if (!prober->ClearStatisticsAndResetSearch() || - !prober->ProbeOneVariable(bool_var)) { - return SatSolver::INFEASIBLE; - } + if (solver->Assignment().VariableIsAssigned(bool_var)) continue; + if (time_limit->LimitReached()) { + return SatSolver::LIMIT_REACHED; } - if (++count > 10) { - count = 0; - if (!SyncBounds()) { + if (!SyncBounds()) { + return SatSolver::INFEASIBLE; + } + if (!probed.contains(bool_var)) { + probed.insert(bool_var); + if (!prober->ProbeOneVariable(bool_var)) { return SatSolver::INFEASIBLE; } - if (time_limit->LimitReached()) { - return SatSolver::LIMIT_REACHED; - } } } } diff --git a/ortools/sat/probing.cc b/ortools/sat/probing.cc index 53d98890b9..76fc863828 100644 --- a/ortools/sat/probing.cc +++ b/ortools/sat/probing.cc @@ -29,17 +29,13 @@ namespace operations_research { namespace sat { Prober::Prober(Model* model) - : model_(model), - trail_(model->GetOrCreate()), + : trail_(*model->GetOrCreate()), + assignment_(model->GetOrCreate()->Assignment()), integer_trail_(model->GetOrCreate()), implied_bounds_(model->GetOrCreate()), sat_solver_(model->GetOrCreate()), - implication_graph_(model->GetOrCreate()), time_limit_(model->GetOrCreate()), - num_new_holes_(0), - num_new_binary_(0), - num_new_integer_bounds_(0), - id_(implication_graph_->PropagatorId()) {} + implication_graph_(model->GetOrCreate()) {} bool Prober::ProbeBooleanVariables(const double deterministic_time_limit, bool log_info) { @@ -55,26 +51,24 @@ bool Prober::ProbeBooleanVariables(const double deterministic_time_limit, return ProbeBooleanVariables(deterministic_time_limit, bool_vars, log_info); } -bool Prober::ProbeOneVariable(BooleanVariable b) { +bool Prober::ProbeOneVariableInternal(BooleanVariable b) { new_integer_bounds_.clear(); propagated_.SparseClearAll(); for (const Literal decision : {Literal(b, true), Literal(b, false)}) { - if (sat_solver_->Assignment().LiteralIsAssigned(decision)) continue; + if (assignment_.LiteralIsAssigned(decision)) continue; CHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0); - const int saved_index = trail_->Index(); + const int saved_index = trail_.Index(); sat_solver_->EnqueueDecisionAndBackjumpOnConflict(decision); sat_solver_->AdvanceDeterministicTime(time_limit_); if (sat_solver_->IsModelUnsat()) return false; if (sat_solver_->CurrentDecisionLevel() == 0) continue; - if (integer_trail_ != nullptr) { - implied_bounds_->ProcessIntegerTrail(decision); - integer_trail_->AppendNewBounds(&new_integer_bounds_); - } - for (int i = saved_index + 1; i < trail_->Index(); ++i) { - const Literal l = (*trail_)[i]; + implied_bounds_->ProcessIntegerTrail(decision); + integer_trail_->AppendNewBounds(&new_integer_bounds_); + for (int i = saved_index + 1; i < trail_.Index(); ++i) { + const Literal l = trail_[i]; // We mark on the first run (b.IsPositive()) and check on the second. if (decision.IsPositive()) { @@ -88,7 +82,8 @@ bool Prober::ProbeOneVariable(BooleanVariable b) { // Anything not propagated by the BinaryImplicationGraph is a "new" // binary clause. This is becaue the BinaryImplicationGraph has the // highest priority of all propagators. - if (trail_->AssignmentType(l.Variable()) != id_) { + if (trail_.AssignmentType(l.Variable()) != + implication_graph_->PropagatorId()) { new_binary_clauses_.push_back({decision.Negated(), l}); } } @@ -176,9 +171,25 @@ bool Prober::ProbeOneVariable(BooleanVariable b) { } } - // We might have updates some integer domain, lets propagate. - if (!sat_solver_->FinishPropagation()) return false; - return true; + // We might have updated some integer domain, let's propagate. + return sat_solver_->FinishPropagation(); +} + +bool Prober::ProbeOneVariable(BooleanVariable b) { + // Reset statistics. + num_new_binary_ = 0; + num_new_holes_ = 0; + num_new_integer_bounds_ = 0; + + // Resize the propagated sparse bitset. + const int num_variables = sat_solver_->NumVariables(); + propagated_.ClearAndResize(LiteralIndex(2 * num_variables)); + + // Reset the solver in case it was already used. + sat_solver_->SetAssumptionLevel(0); + if (!sat_solver_->RestoreSolverToAssumptionLevel()) return false; + + return ProbeOneVariableInternal(b); } bool Prober::ProbeBooleanVariables(const double deterministic_time_limit, @@ -188,10 +199,18 @@ bool Prober::ProbeBooleanVariables(const double deterministic_time_limit, WallTimer wall_timer; wall_timer.Start(); + // Reset statistics. + num_new_binary_ = 0; + num_new_holes_ = 0; + num_new_integer_bounds_ = 0; + + // Resize the propagated sparse bitset. + const int num_variables = sat_solver_->NumVariables(); + propagated_.ClearAndResize(LiteralIndex(2 * num_variables)); + // Reset the solver in case it was already used. - if (!ClearStatisticsAndResetSearch()) { - return SatSolver::INFEASIBLE; - } + sat_solver_->SetAssumptionLevel(0); + if (!sat_solver_->RestoreSolverToAssumptionLevel()) return false; const int initial_num_fixed = sat_solver_->LiteralTrail().Index(); const double initial_deterministic_time = @@ -217,7 +236,7 @@ bool Prober::ProbeBooleanVariables(const double deterministic_time_limit, // Propagate b=1 and then b=0. ++num_probed; - if (!ProbeOneVariable(b)) { + if (!ProbeOneVariableInternal(b)) { return false; } } @@ -247,27 +266,6 @@ bool Prober::ProbeBooleanVariables(const double deterministic_time_limit, return true; } -bool Prober::ClearStatisticsAndResetSearch() { - // For the new direct implication detected. - num_new_binary_ = 0; - - // This is used to tighten the integer variable bounds. - num_new_holes_ = 0; - num_new_integer_bounds_ = 0; - new_integer_bounds_.clear(); - - // To detect literal x that must be true because b => x and not(b) => x. - // When probing b, we add all propagated literal to propagated, and when - // probing not(b) we check if any are already there. - const int num_variables = sat_solver_->NumVariables(); - propagated_.ClearAndResize(LiteralIndex(2 * num_variables)); - - sat_solver_->SetAssumptionLevel(0); - if (!sat_solver_->RestoreSolverToAssumptionLevel()) return false; - - return true; -} - bool LookForTrivialSatSolution(double deterministic_time_limit, Model* model, bool log_info) { log_info |= VLOG_IS_ON(1); diff --git a/ortools/sat/probing.h b/ortools/sat/probing.h index 9e9cdce999..5a57278459 100644 --- a/ortools/sat/probing.h +++ b/ortools/sat/probing.h @@ -73,30 +73,38 @@ class Prober { bool ProbeOneVariable(BooleanVariable b); - bool ClearStatisticsAndResetSearch(); - private: - Model* model_; - SparseBitset propagated_; - std::vector new_integer_bounds_; - Trail* trail_; + bool ProbeOneVariableInternal(BooleanVariable b); + + // Model owned classes. + const Trail& trail_; + const VariablesAssignment& assignment_; IntegerTrail* integer_trail_; ImpliedBounds* implied_bounds_; SatSolver* sat_solver_; - BinaryImplicationGraph* implication_graph_; TimeLimit* time_limit_; + BinaryImplicationGraph* implication_graph_; + + // To detect literal x that must be true because b => x and not(b) => x. + // When probing b, we add all propagated literal to propagated, and when + // probing not(b) we check if any are already there. + SparseBitset propagated_; + + // Modifications found during probing. std::vector to_fix_at_true_; - int num_new_holes_; - int num_new_binary_; - int num_new_integer_bounds_; + std::vector new_integer_bounds_; std::vector> new_binary_clauses_; - int id_; + + // Probing statistics. + int num_new_holes_ = 0; + int num_new_binary_ = 0; + int num_new_integer_bounds_ = 0; }; // Try to randomly tweak the search and stop at the first conflict each time. -// This can sometimes find feasible solution, but more importantly, it is a -// form of probing that can sometimes find small and interesting conflicts or -// fix variables. This seems to work well on the SAT14/app/rook-* problems and +// This can sometimes find feasible solution, but more importantly, it is a form +// of probing that can sometimes find small and interesting conflicts or fix +// variables. This seems to work well on the SAT14/app/rook-* problems and // do fix more variables if run before probing. // // If a feasible SAT solution is found (i.e. all Boolean assigned), then this @@ -116,20 +124,19 @@ struct ProbingOptions { // else can be deduced and everything has been probed until fix-point. The // fix point depend on the extract_binay_clauses option: // - If false, we will just stop when no more failed literal can be found. - // - If true, we will do more work and stop when all failed literal have - // been + // - If true, we will do more work and stop when all failed literal have been // found and all hyper binary resolution have been performed. // // TODO(user): We can also provide a middle ground and probe all failed // literal but do not extract all binary clauses. // - // Note that the fix-point is unique, modulo the equivalent literal - // detection we do. And if we add binary clauses, modulo the transitive - // reduction of the binary implication graph. + // Note that the fix-point is unique, modulo the equivalent literal detection + // we do. And if we add binary clauses, modulo the transitive reduction of the + // binary implication graph. // - // To be fast, we only use the binary clauses in the binary implication - // graph for the equivalence detection. So the power of the equivalence - // detection changes if the extract_binay_clauses option is true or not. + // To be fast, we only use the binary clauses in the binary implication graph + // for the equivalence detection. So the power of the equivalence detection + // changes if the extract_binay_clauses option is true or not. // // TODO(user): The fix point is not yet reached since we don't currently // simplify non-binary clauses with these equivalence, but we will. @@ -144,24 +151,22 @@ struct ProbingOptions { // With these extra clause the power of the equivalence literal detection // using only the binary implication graph with increase. Note that it is // possible to do exactly the same thing without adding these binary clause - // first. This is what is done by yet another probing algorithm (currently - // in simplification.cc). + // first. This is what is done by yet another probing algorithm (currently in + // simplification.cc). // // TODO(user): Note that adding binary clause before/during the SAT presolve - // is currently not always a good idea. This is because we don't simplify - // the other clause as much as we could. Also, there can be up to a - // quadratic number of clauses added this way, which might slow down things - // a lot. But then because of the deterministic limit, we usually cannot add - // too much clauses, even for huge problems, since we will reach the limit - // before that. + // is currently not always a good idea. This is because we don't simplify the + // other clause as much as we could. Also, there can be up to a quadratic + // number of clauses added this way, which might slow down things a lot. But + // then because of the deterministic limit, we usually cannot add too much + // clauses, even for huge problems, since we will reach the limit before that. bool extract_binary_clauses = false; - // Use a version of the "Tree look" algorithm as explained in the paper - // above. This is usually faster and more efficient. Note that when - // extracting binary clauses it might currently produce more "redundant" one - // in the sense that a transitive reduction of the binary implication graph - // after all hyper binary resolution have been performed may need to do more - // work. + // Use a version of the "Tree look" algorithm as explained in the paper above. + // This is usually faster and more efficient. Note that when extracting binary + // clauses it might currently produce more "redundant" one in the sense that a + // transitive reduction of the binary implication graph after all hyper binary + // resolution have been performed may need to do more work. bool use_tree_look = true; // There is two sligthly different implementation of the tree-look algo. @@ -171,9 +176,9 @@ struct ProbingOptions { bool use_queue = true; // If we detect as we probe that a new binary clause subsumes one of the - // non-binary clause, we will replace the long clause by the binary one. - // This is orthogonal to the extract_binary_clauses parameters which will - // add all binary clauses but not neceassirly check for subsumption. + // non-binary clause, we will replace the long clause by the binary one. This + // is orthogonal to the extract_binary_clauses parameters which will add all + // binary clauses but not neceassirly check for subsumption. bool subsume_with_binary_clause = true; // We assume this is also true if --v 1 is activated. diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto index 8d44a16ce6..c9012f4765 100644 --- a/ortools/sat/sat_parameters.proto +++ b/ortools/sat/sat_parameters.proto @@ -756,7 +756,7 @@ message SatParameters { // every root node. optional int64 probing_period_at_root = 142 [default = 0]; - // If true, this worker will continuously probe Boolean variables, and integer + // If true, search will continuously probe Boolean variables, and integer // variable bounds. optional bool use_probing_search = 176 [default = false]; diff --git a/ortools/sat/synchronization.cc b/ortools/sat/synchronization.cc index e29c9e5195..a44271755e 100644 --- a/ortools/sat/synchronization.cc +++ b/ortools/sat/synchronization.cc @@ -593,10 +593,12 @@ void SharedBoundsManager::ReportPotentialNewBounds( changed_variables_since_last_synchronize_.Set(var); num_improvements++; } - // TODO(user): remove LOG_IF and display number of bound improvements - // propagated per workers. - VLOG_IF(2, num_improvements > 0) - << worker_name << " exports " << num_improvements << " modifications"; + // TODO(user): Display number of bound improvements cumulatively per + // workers at the end of the search. + if (num_improvements > 0) { + VLOG(2) << worker_name << " exports " << num_improvements + << " modifications"; + } } void SharedBoundsManager::Synchronize() {