From f611dea03bc90cdc06699245cf77b191d584e18d Mon Sep 17 00:00:00 2001 From: "lperron@google.com" Date: Fri, 21 Mar 2014 18:02:17 +0000 Subject: [PATCH] tune sat solver --- src/sat/sat_parameters.proto | 4 ++-- src/sat/sat_solver.cc | 33 +++++++++++++++++---------------- src/sat/sat_solver.h | 2 +- 3 files changed, 20 insertions(+), 19 deletions(-) diff --git a/src/sat/sat_parameters.proto b/src/sat/sat_parameters.proto index d5ca67bcce..c4c7cb0095 100644 --- a/src/sat/sat_parameters.proto +++ b/src/sat/sat_parameters.proto @@ -82,7 +82,7 @@ message SatParameters { // Each time the learned clause database is cleaned, we want the target size // of the next cleaning to be equals to the current database after it has just // been cleaned plus this parameter. - optional double clause_cleanup_increment = 11 [default = 2000]; + optional double clause_cleanup_increment = 11 [default = 1500]; // Deletes this ratio of clauses during each cleanup. optional double clause_cleanup_ratio = 13 [default = 0.5]; @@ -122,7 +122,7 @@ message SatParameters { // To try to reward good variables, Glucose bumps again the variable from the // last decision level and with a learned reason of smaller LBD than the 1 UIP // conflict. This needs use_lbd() to be true. - optional bool use_glucose_bump_again_strategy = 21 [ default = true]; + optional bool use_glucose_bump_again_strategy = 21 [ default = false]; // Frequecy of periodic restart if > 0. A negative value indicates // no restart. diff --git a/src/sat/sat_solver.cc b/src/sat/sat_solver.cc index 3008fd222f..bcf77f508a 100644 --- a/src/sat/sat_solver.cc +++ b/src/sat/sat_solver.cc @@ -370,7 +370,8 @@ int SatSolver::EnqueueDecisionAndBackjumpOnConflict(Literal true_literal) { // Minimizing the conflict with binary clauses first has two advantages. // First, there is no need to compute a reason for the variables eliminated // this way. Second, more variables may be marked (in is_marked_) and - // MinimizeConflict() can take advantage of that. + // MinimizeConflict() can take advantage of that. Because of this, the + // LBD of the learned conflict can change. if (binary_implication_graph_.NumberOfImplications() != 0 && parameters_.binary_minimization_algorithm() == SatParameters::BINARY_MINIMIZATION_FIRST) { @@ -380,14 +381,7 @@ int SatSolver::EnqueueDecisionAndBackjumpOnConflict(Literal true_literal) { } // Minimize the learned conflict. -#ifndef NDEBUG - const int initial_lbd = ComputeLbd(learned_conflict_); -#endif MinimizeConflict(&learned_conflict_, &reason_used_to_infer_the_conflict_); -#ifndef NDEBUG - DCHECK(IsConflictValid(learned_conflict_)); - DCHECK_EQ(initial_lbd, ComputeLbd(learned_conflict_)); -#endif // Minimize it further with binary clauses? if (binary_implication_graph_.NumberOfImplications() != 0) { @@ -568,6 +562,7 @@ SatSolver::Status SatSolver::Solve() { if (parameters_.log_search_progress()) { LOG(INFO) << "The time limit has been reached. Aborting."; LOG(INFO) << RunningStatisticsString(); + LOG(INFO) << StatusString(LIMIT_REACHED); } return LIMIT_REACHED; } @@ -575,6 +570,7 @@ SatSolver::Status SatSolver::Solve() { if (parameters_.log_search_progress()) { LOG(INFO) << "The conflict limit has been reached. Aborting."; LOG(INFO) << RunningStatisticsString(); + LOG(INFO) << StatusString(LIMIT_REACHED); } return LIMIT_REACHED; } @@ -589,6 +585,7 @@ SatSolver::Status SatSolver::Solve() { if (IsMemoryLimitReached()) { if (parameters_.log_search_progress()) { LOG(INFO) << "The memory limit has been reached. Aborting."; + LOG(INFO) << StatusString(LIMIT_REACHED); } return LIMIT_REACHED; } @@ -604,7 +601,7 @@ SatSolver::Status SatSolver::Solve() { if (trail_.Index() == num_variables_.value()) { // At a leaf. if (parameters_.log_search_progress()) { LOG(INFO) << RunningStatisticsString(); - LOG(INFO) << "SAT \n" << StatusString(); + LOG(INFO) << StatusString(MODEL_SAT); } return MODEL_SAT; } @@ -625,7 +622,7 @@ SatSolver::Status SatSolver::Solve() { } if (EnqueueDecisionAndBackjumpOnConflict(next_branch) == -1) { if (parameters_.log_search_progress()) { - LOG(INFO) << "UNSAT \n" << StatusString(); + LOG(INFO) << StatusString(MODEL_UNSAT); } return MODEL_UNSAT; } @@ -634,7 +631,7 @@ SatSolver::Status SatSolver::Solve() { // given the assumption. if (CurrentDecisionLevel() < assumption_level) { if (parameters_.log_search_progress()) { - LOG(INFO) << "ASSUMPTIONS_UNSAT\n" << StatusString(); + LOG(INFO) << StatusString(ASSUMPTIONS_UNSAT); } // TODO(user): Reapply the assumptions that are still valid so it is // easier for a client to see what was incompatible? @@ -762,10 +759,13 @@ int SatSolver::ComputeBacktrackLevel(const std::vector& literals) { } template -int SatSolver::ComputeLbd(const LiteralList& literals) { +int SatSolver::ComputeLbd(const LiteralList& conflict) { SCOPED_TIME_STAT(&stats_); - is_level_marked_.ClearAndResize(SatDecisionLevel(CurrentDecisionLevel() + 1)); - for (const Literal literal : literals) { + // We know that the first literal of the conflict is always of the highest + // level. + is_level_marked_.ClearAndResize(SatDecisionLevel( + DecisionLevel(conflict.begin()->Variable()) + 1)); + for (const Literal literal : conflict) { const SatDecisionLevel level(DecisionLevel(literal.Variable())); DCHECK_GE(level, 0); if (level > 0 && !is_level_marked_[level]) { @@ -775,9 +775,10 @@ int SatSolver::ComputeLbd(const LiteralList& literals) { return is_level_marked_.NumberOfSetCallsWithDifferentArguments(); } -std::string SatSolver::StatusString() const { +std::string SatSolver::StatusString(Status status) const { const double time_in_s = timer_.Get(); - return StringPrintf(" time: %fs\n", time_in_s) + + return StringPrintf("\n status: %s\n", SatStatusString(status).c_str()) + + StringPrintf(" time: %fs\n", time_in_s) + StringPrintf(" memory: %s\n", MemoryUsage().c_str()) + StringPrintf(" num failures: %" GG_LL_FORMAT "d (%.0f /sec)\n", counters_.num_failures, diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 920344c8bb..0fdbe87fa4 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -413,7 +413,7 @@ class SatSolver { void InitRestart(); std::string DebugString(const SatClause& clause) const; - std::string StatusString() const; + std::string StatusString(Status status) const; std::string RunningStatisticsString() const; VariableIndex num_variables_;