From d38c6a97f2d81fd4eacf86fc39df055ee1c6671d Mon Sep 17 00:00:00 2001 From: "lperron@google.com" Date: Fri, 7 Nov 2014 14:30:26 +0000 Subject: [PATCH] improvements to the sat/maxsat solvers --- src/sat/boolean_problem.cc | 333 +++++++++++++++++++++------- src/sat/boolean_problem.h | 41 +++- src/sat/boolean_problem.proto | 31 ++- src/sat/clause.cc | 39 ++-- src/sat/clause.h | 36 +-- src/sat/optimization.cc | 7 +- src/sat/pb_constraint.cc | 46 +++- src/sat/pb_constraint.h | 29 +++ src/sat/sat_base.h | 9 +- src/sat/sat_parameters.proto | 205 ++++++++++++----- src/sat/sat_solver.cc | 405 ++++++++++++++++++++++++++-------- src/sat/sat_solver.h | 77 +++++-- src/sat/simplification.cc | 345 +++++++++++++++++++++++------ src/sat/simplification.h | 113 ++++++++-- 14 files changed, 1311 insertions(+), 405 deletions(-) diff --git a/src/sat/boolean_problem.cc b/src/sat/boolean_problem.cc index 65b09d46bd..ce0b3536c4 100644 --- a/src/sat/boolean_problem.cc +++ b/src/sat/boolean_problem.cc @@ -45,50 +45,93 @@ namespace { // Used by BooleanProblemIsValid() to test that there is no duplicate literals, // that they are all within range and that there is no zero coefficient. +// +// A non-empty std::string indicates an error. template -bool IsValid(const LinearTerms& terms, std::vector* variable_seen) { +std::string ValidateLinearTerms(const LinearTerms& terms, + std::vector* variable_seen) { + // variable_seen already has all items false and is reset before return. + std::string err_str; + int num_errs = 0; + const int max_num_errs = 100; for (int i = 0; i < terms.literals_size(); ++i) { if (terms.literals(i) == 0) { - LOG(INFO) << "Zero literal at position " << i; - return false; + if (++num_errs <= max_num_errs) + err_str += StringPrintf("Zero literal at position %d\n", i); } if (terms.coefficients(i) == 0) { - LOG(INFO) << "Literal " << terms.literals(i) << " has a zero coefficient"; - return false; + if (++num_errs <= max_num_errs) + err_str += StringPrintf("Literal %d has a zero coefficient\n", + terms.literals(i)); } const int var = Literal(terms.literals(i)).Variable().value(); if (var >= variable_seen->size()) { - LOG(INFO) << "Out of bound variable " << var; - return false; + if (++num_errs <= max_num_errs) + err_str += StringPrintf("Out of bound variable %d\n", var); } if ((*variable_seen)[var]) { - LOG(INFO) << "Duplicated variable " << var; - return false; + if (++num_errs <= max_num_errs) + err_str += StringPrintf("Duplicated variable %d\n", var); } (*variable_seen)[var] = true; } + for (int i = 0; i < terms.literals_size(); ++i) { const int var = Literal(terms.literals(i)).Variable().value(); (*variable_seen)[var] = false; } - return true; + if (num_errs) { + if (num_errs <= max_num_errs) { + err_str = StringPrintf("%d validation errors:\n", num_errs) + err_str; + } else { + err_str = StringPrintf("%d validation errors; here are the first %d:\n", + num_errs, max_num_errs) + err_str; + } + } + return err_str; +} + +// Converts a linear expression from the protocol buffer format to a vector +// of LiteralWithCoeff. +template +std::vector ConvertLinearExpression(const ProtoFormat& input) { + std::vector cst; + for (int i = 0; i < input.literals_size(); ++i) { + const Literal literal(input.literals(i)); + cst.push_back(LiteralWithCoeff(literal, input.coefficients(i))); + } + return cst; } } // namespace -bool BooleanProblemIsValid(const LinearBooleanProblem& problem) { +util::Status ValidateBooleanProblem(const LinearBooleanProblem& problem) { std::vector variable_seen(problem.num_variables(), false); - for (const LinearBooleanConstraint& constraint : problem.constraints()) { - if (!IsValid(constraint, &variable_seen)) { - LOG(INFO) << "Invalid constraint " << constraint.name(); - return false; + for (int i = 0; i < problem.constraints_size(); ++i) { + const LinearBooleanConstraint& constraint = problem.constraints(i); + const std::string error = ValidateLinearTerms(constraint, &variable_seen); + if (!error.empty()) { + return util::Status(util::error::INVALID_ARGUMENT, + StringPrintf("Invalid constraint %i: ", i) + error); } } - if (!IsValid(problem.objective(), &variable_seen)) { - LOG(INFO) << "Invalid objective."; - return false; + const std::string error = ValidateLinearTerms(problem.objective(), &variable_seen); + if (!error.empty()) { + return util::Status(util::error::INVALID_ARGUMENT, + StringPrintf("Invalid objective: ") + error); + } + return util::Status::OK; +} + +void ChangeOptimizationDirection(LinearBooleanProblem* problem) { + LinearObjective* objective = problem->mutable_objective(); + objective->set_scaling_factor(-objective->scaling_factor()); + objective->set_offset(-objective->offset()); + // We need 'auto' here to keep the open-source compilation happy + // (it uses the public protobuf release). + for (auto& coefficients_ref : *objective->mutable_coefficients()) { + coefficients_ref = -coefficients_ref; } - return true; } bool LoadBooleanProblem(const LinearBooleanProblem& problem, @@ -97,8 +140,10 @@ bool LoadBooleanProblem(const LinearBooleanProblem& problem, // constraints with duplicate variables, so we just output a warning if the // problem is not "valid". Make this a strong check once we have some // preprocessing step to remove duplicates variable in the constraints. - if (!BooleanProblemIsValid(problem)) { - LOG(WARNING) << "The given problem is invalid!"; + const util::Status status = ValidateBooleanProblem(problem); + if (!status.ok()) { + // LOG(WARNING) << "The given problem is invalid! " << status.error_message(); + LOG(WARNING) << "The given problem is invalid! "; } if (solver->parameters().log_search_progress()) { @@ -109,19 +154,20 @@ bool LoadBooleanProblem(const LinearBooleanProblem& problem, solver->SetNumVariables(problem.num_variables()); std::vector cst; int64 num_terms = 0; + int num_constraints = 0; for (const LinearBooleanConstraint& constraint : problem.constraints()) { - cst.clear(); num_terms += constraint.literals_size(); - for (int i = 0; i < constraint.literals_size(); ++i) { - const Literal literal(constraint.literals(i)); - cst.push_back(LiteralWithCoeff(literal, constraint.coefficients(i))); - } + cst = ConvertLinearExpression(constraint); if (!solver->AddLinearConstraint( constraint.has_lower_bound(), Coefficient(constraint.lower_bound()), constraint.has_upper_bound(), Coefficient(constraint.upper_bound()), &cst)) { + LOG(INFO) << "Problem detected to be UNSAT when " + << "adding the constraint #" << num_constraints + << " with name '" << constraint.name() << "'"; return false; } + ++num_constraints; } if (solver->parameters().log_search_progress()) { LOG(INFO) << "The problem contains " << num_terms << " terms."; @@ -131,48 +177,36 @@ bool LoadBooleanProblem(const LinearBooleanProblem& problem, void UseObjectiveForSatAssignmentPreference(const LinearBooleanProblem& problem, SatSolver* solver) { - // Initialize the heuristic to look for a good solution. - if (problem.type() == LinearBooleanProblem::MINIMIZATION || - problem.type() == LinearBooleanProblem::MAXIMIZATION) { - const int sign = - (problem.type() == LinearBooleanProblem::MAXIMIZATION) ? -1 : 1; - const LinearObjective& objective = problem.objective(); - double max_weight = 0; - for (int i = 0; i < objective.literals_size(); ++i) { - max_weight = - std::max(max_weight, fabs(static_cast(objective.coefficients(i)))); - } - for (int i = 0; i < objective.literals_size(); ++i) { - const double weight = - fabs(static_cast(objective.coefficients(i))) / max_weight; - if (sign * objective.coefficients(i) > 0) { - solver->SetAssignmentPreference( - Literal(objective.literals(i)).Negated(), weight); - } else { - solver->SetAssignmentPreference(Literal(objective.literals(i)), weight); - } + const LinearObjective& objective = problem.objective(); + double max_weight = 0; + for (int i = 0; i < objective.literals_size(); ++i) { + max_weight = + std::max(max_weight, fabs(static_cast(objective.coefficients(i)))); + } + for (int i = 0; i < objective.literals_size(); ++i) { + const double weight = + fabs(static_cast(objective.coefficients(i))) / max_weight; + if (objective.coefficients(i) > 0) { + solver->SetAssignmentPreference(Literal(objective.literals(i)).Negated(), + weight); + } else { + solver->SetAssignmentPreference(Literal(objective.literals(i)), weight); } } } +bool AddObjectiveUpperBound(const LinearBooleanProblem& problem, + Coefficient upper_bound, SatSolver* solver) { + std::vector cst = ConvertLinearExpression(problem.objective()); + return solver->AddLinearConstraint(false, Coefficient(0), true, upper_bound, + &cst); +} + bool AddObjectiveConstraint(const LinearBooleanProblem& problem, bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, SatSolver* solver) { - if (problem.type() != LinearBooleanProblem::MINIMIZATION && - problem.type() != LinearBooleanProblem::MAXIMIZATION) { - return true; - } - std::vector cst; - const LinearObjective& objective = problem.objective(); - for (int i = 0; i < objective.literals_size(); ++i) { - const Literal literal(objective.literals(i)); - if (literal.Variable() >= problem.num_variables()) { - LOG(WARNING) << "Literal out of bound: " << literal; - return false; - } - cst.push_back(LiteralWithCoeff(literal, objective.coefficients(i))); - } + std::vector cst = ConvertLinearExpression(problem.objective()); return solver->AddLinearConstraint(use_lower_bound, lower_bound, use_upper_bound, upper_bound, &cst); } @@ -223,7 +257,7 @@ bool IsAssignmentValid(const LinearBooleanProblem& problem, // form >= 1) and all objective weights must be strictly positive. std::string LinearBooleanProblemToCnfString(const LinearBooleanProblem& problem) { std::string output; - const bool is_wcnf = (problem.type() == LinearBooleanProblem::MINIMIZATION); + const bool is_wcnf = (problem.objective().coefficients_size() > 0); const LinearObjective& objective = problem.objective(); // Hack: We know that all the variables with index greater than this have been @@ -375,11 +409,7 @@ Graph* GenerateGraphForSymmetryDetection( CanonicalBooleanLinearProblem canonical_problem; std::vector cst; for (const LinearBooleanConstraint& constraint : problem.constraints()) { - cst.clear(); - for (int i = 0; i < constraint.literals_size(); ++i) { - const Literal literal(constraint.literals(i)); - cst.push_back(LiteralWithCoeff(literal, constraint.coefficients(i))); - } + cst = ConvertLinearExpression(constraint); CHECK(canonical_problem.AddLinearConstraint( constraint.has_lower_bound(), Coefficient(constraint.lower_bound()), constraint.has_upper_bound(), Coefficient(constraint.upper_bound()), @@ -414,25 +444,18 @@ Graph* GenerateGraphForSymmetryDetection( id_generator.GetId(NodeType::LITERAL_NODE, Coefficient(0))); // Literals with different objective coeffs shouldn't be in the same class. - if (problem.type() == LinearBooleanProblem::MINIMIZATION || - problem.type() == LinearBooleanProblem::MAXIMIZATION) { - // We need to canonicalize the objective to regroup literals corresponding - // to the same variables. - std::vector expr; - const LinearObjective& objective = problem.objective(); - for (int i = 0; i < objective.literals_size(); ++i) { - const Literal literal(objective.literals(i)); - expr.push_back(LiteralWithCoeff(literal, objective.coefficients(i))); - } - // Note that we don't care about the offset or optimization direction here, - // we just care about literals with the same canonical coefficient. - Coefficient shift; - Coefficient max_value; - ComputeBooleanLinearExpressionCanonicalForm(&expr, &shift, &max_value); - for (LiteralWithCoeff term : expr) { - (*initial_equivalence_classes)[term.literal.Index().value()] = - id_generator.GetId(NodeType::LITERAL_NODE, term.coefficient); - } + // + // We need to canonicalize the objective to regroup literals corresponding + // to the same variables. Note that we don't care about the offset or + // optimization direction here, we just care about literals with the same + // canonical coefficient. + Coefficient shift; + Coefficient max_value; + std::vector expr = ConvertLinearExpression(problem.objective()); + ComputeBooleanLinearExpressionCanonicalForm(&expr, &shift, &max_value); + for (LiteralWithCoeff term : expr) { + (*initial_equivalence_classes)[term.literal.Index().value()] = + id_generator.GetId(NodeType::LITERAL_NODE, term.coefficient); } // Then, for each constraint, we will have one or more nodes. @@ -587,5 +610,145 @@ void FindLinearBooleanProblemSymmetries( LOG(INFO) << "Average support size: " << average_support_size; } +void ApplyLiteralMappingToBooleanProblem( + const ITIVector& mapping, + LinearBooleanProblem* problem) { + Coefficient bound_shift; + Coefficient max_value; + std::vector cst; + + // First the objective. + cst = ConvertLinearExpression(problem->objective()); + ApplyLiteralMapping(mapping, &cst, &bound_shift, &max_value); + LinearObjective* mutable_objective = problem->mutable_objective(); + mutable_objective->clear_literals(); + mutable_objective->clear_coefficients(); + mutable_objective->set_offset(mutable_objective->offset() - + bound_shift.value()); + for (const LiteralWithCoeff& entry : cst) { + mutable_objective->add_literals(entry.literal.SignedValue()); + mutable_objective->add_coefficients(entry.coefficient.value()); + } + + // Now the clauses. + for (LinearBooleanConstraint& constraint : *problem->mutable_constraints()) { + cst = ConvertLinearExpression(constraint); + constraint.clear_literals(); + constraint.clear_coefficients(); + ApplyLiteralMapping(mapping, &cst, &bound_shift, &max_value); + + // Add bound_shift to the bounds and remove a bound if it is now trivial. + if (constraint.has_upper_bound()) { + constraint.set_upper_bound(constraint.upper_bound() + + bound_shift.value()); + if (max_value <= constraint.upper_bound()) { + constraint.clear_upper_bound(); + } + } + if (constraint.has_lower_bound()) { + constraint.set_lower_bound(constraint.lower_bound() + + bound_shift.value()); + // This is because ApplyLiteralMapping make all coefficient positive. + if (constraint.lower_bound() <= 0) { + constraint.clear_lower_bound(); + } + } + + // If the constraint is always true, we just leave it empty. + if (constraint.has_lower_bound() || constraint.has_upper_bound()) { + for (const LiteralWithCoeff& entry : cst) { + constraint.add_literals(entry.literal.SignedValue()); + constraint.add_coefficients(entry.coefficient.value()); + } + } + } + + // Remove empty constraints. + int new_index = 0; + const int num_constraints = problem->constraints_size(); + for (int i = 0; i < num_constraints; ++i) { + if (!(problem->constraints(i).literals_size() == 0)) { + problem->mutable_constraints()->SwapElements(i, new_index); + ++new_index; + } + } + problem->mutable_constraints()->DeleteSubrange(new_index, + num_constraints - new_index); + + // Computes the new number of variables and set it. + int num_vars = 0; + for (LiteralIndex index : mapping) { + if (index >= 0) { + num_vars = std::max(num_vars, Literal(index).Variable().value() + 1); + } + } + problem->set_num_variables(num_vars); + + // TODO(user): The names is currently all scrambled. Do something about it + // so that non-fixed variables keep their names. + problem->mutable_var_names()->DeleteSubrange( + num_vars, problem->var_names_size() - num_vars); +} + +// A simple preprocessing step that does basic probing and removes the +// equivalent literals. +void ProbeAndSimplifyProblem(SatPostsolver* postsolver, + LinearBooleanProblem* problem) { + // TODO(user): expose the number of iterations as a parameter. + for (int iter = 0; iter < 6; ++iter) { + SatSolver solver; + if (!LoadBooleanProblem(*problem, &solver)) { + LOG(INFO) << "UNSAT when loading the problem."; + } + + ITIVector equiv_map; + ProbeAndFindEquivalentLiteral(&solver, postsolver, &equiv_map); + + // We can abort if no information is learned. + if (equiv_map.empty() && solver.LiteralTrail().Index() == 0) break; + + if (equiv_map.empty()) { + const int num_literals = 2 * solver.NumVariables(); + for (LiteralIndex index(0); index < num_literals; ++index) { + equiv_map.push_back(index); + } + } + + // Fix fixed variables in the equivalence map and in the postsolver. + solver.Backtrack(0); + for (int i = 0; i < solver.LiteralTrail().Index(); ++i) { + const Literal l = solver.LiteralTrail()[i]; + equiv_map[l.Index()] = kTrueLiteralIndex; + equiv_map[l.NegatedIndex()] = kFalseLiteralIndex; + postsolver->FixVariable(l); + } + + // Remap the variables into a dense set. All the variables for which the + // equiv_map is not the identity are no longer needed. + VariableIndex new_var(0); + ITIVector var_map; + for (VariableIndex var(0); var < solver.NumVariables(); ++var) { + if (equiv_map[Literal(var, true).Index()] == Literal(var, true).Index()) { + var_map.push_back(new_var); + ++new_var; + } else { + var_map.push_back(VariableIndex(-1)); + } + } + + // Apply the variable mapping. + postsolver->ApplyMapping(var_map); + for (LiteralIndex index(0); index < equiv_map.size(); ++index) { + if (equiv_map[index] >= 0) { + const Literal l(equiv_map[index]); + const VariableIndex image = var_map[l.Variable()]; + CHECK_NE(image, VariableIndex(-1)); + equiv_map[index] = Literal(image, l.IsPositive()).Index(); + } + } + ApplyLiteralMappingToBooleanProblem(equiv_map, problem); + } +} + } // namespace sat } // namespace operations_research diff --git a/src/sat/boolean_problem.h b/src/sat/boolean_problem.h index 2dbb0e58de..16e1a50f62 100644 --- a/src/sat/boolean_problem.h +++ b/src/sat/boolean_problem.h @@ -16,19 +16,35 @@ #include "sat/boolean_problem.pb.h" #include "sat/sat_solver.h" +#include "sat/simplification.h" #include "algorithms/sparse_permutation.h" +#include "base/status.h" namespace operations_research { namespace sat { +// Adds the offset and returns the scaled version of the given objective value. +inline double AddOffsetAndScaleObjectiveValue( + const LinearBooleanProblem& problem, Coefficient v) { + return (static_cast(v.value()) + problem.objective().offset()) * + problem.objective().scaling_factor(); +} + +// Keeps the same objective but change the optimization direction from a +// minimization problem to a maximization problem. +// +// Ex: if the problem was to minimize 2 + x, the new problem will be to maximize +// 2 + x subject to exactly the same constraints. +void ChangeOptimizationDirection(LinearBooleanProblem* problem); + // Copies the assignment from the solver into the given Boolean vector. Note // that variables with a greater index that the given num_variables are ignored. void ExtractAssignment(const LinearBooleanProblem& problem, const SatSolver& solver, std::vector* assignment); // Tests the preconditions of the given problem (as described in the proto) and -// returns true iff they are all satisfied. -bool BooleanProblemIsValid(const LinearBooleanProblem& problem); +// returns an error if they are not all satisfied. +util::Status ValidateBooleanProblem(const LinearBooleanProblem& problem); // Loads a BooleanProblem into a given SatSolver instance. bool LoadBooleanProblem(const LinearBooleanProblem& problem, SatSolver* solver); @@ -38,6 +54,10 @@ bool LoadBooleanProblem(const LinearBooleanProblem& problem, SatSolver* solver); void UseObjectiveForSatAssignmentPreference(const LinearBooleanProblem& problem, SatSolver* solver); +// Adds the constraint that the objective is smaller than the given upper bound. +bool AddObjectiveUpperBound(const LinearBooleanProblem& problem, + Coefficient upper_bound, SatSolver* solver); + // Adds the constraint that the objective is smaller or equals to the given // upper bound. bool AddObjectiveConstraint(const LinearBooleanProblem& problem, @@ -80,6 +100,23 @@ void MakeAllLiteralsPositive(LinearBooleanProblem* problem); void FindLinearBooleanProblemSymmetries( const LinearBooleanProblem& problem, std::vector>* generators); +// Maps all the literals of the problem. Note that this converts the cost of a +// variable correctly, that is if a variable with cost is mapped to another, the +// cost of the later is updated. +// +// Preconditions: the mapping must map l and not(l) to the same variable and be +// of the correct size. It can also map a literal index to kTrueLiteralIndex +// or kFalseLiteralIndex in order to fix the variable. +void ApplyLiteralMappingToBooleanProblem( + const ITIVector& mapping, + LinearBooleanProblem* problem); + +// A simple preprocessing step that does basic probing and removes the fixed and +// equivalent variables. Note that the variable indices will also be remapped in +// order to be dense. The given postsolver will be updated with the information +// needed during postsolve. +void ProbeAndSimplifyProblem(SatPostsolver* postsolver, + LinearBooleanProblem* problem); } // namespace sat } // namespace operations_research diff --git a/src/sat/boolean_problem.proto b/src/sat/boolean_problem.proto index b5dc55e8ce..64537bfb32 100644 --- a/src/sat/boolean_problem.proto +++ b/src/sat/boolean_problem.proto @@ -43,22 +43,24 @@ message LinearBooleanConstraint { optional string name = 5 [default = ""]; } -// The objective of an optimization problem. The goal will be to minimize (resp. -// maximize) this linear Boolean formula. The direction is given by the problem -// type (see below). +// The objective of an optimization problem. message LinearObjective { + // The goal is always to minimize the linear Boolean formula defined by these + // two fields: sum_i literal_i * coefficient_i where literal_i is 1 iff + // literal_i is true in a given assignment. + // // Note that the same variable shouldn't appear twice and that zero // coefficients are not allowed. repeated int32 literals = 1; repeated int64 coefficients = 2; - // For a given variable assignment, the problem objective value is - // 'scaling_factor * (sum literal * coefficient) + offset' - // where literal_i is 1 iff literal_i is true. + // For a given variable assignment, the "real" problem objective value is + // 'scaling_factor * (minimization_objective + offset)' where + // 'minimization_objective is the one defined just above. // - // Note: the scaling_factor must be positive. This is important because the - // solver just minimize (resp. maximize) the expression - // 'sum literal * coefficient'. + // Note that this is not what we minimize, but it is what we display. + // In particular if scaling_factor is negative, then the "real" problem is + // a maximization problem, even if the "internal" objective is minimized. optional double offset = 3 [default = 0.0]; optional double scaling_factor = 4 [default = 1.0]; } @@ -77,14 +79,6 @@ message LinearBooleanProblem { // The name of the problem. optional string name = 1 [default = ""]; - // The type of the problem. - enum ProblemType { - SATISFIABILITY = 0; - MAXIMIZATION = 1; - MINIMIZATION = 2; - } - optional ProblemType type = 2 [default = SATISFIABILITY]; - // The number of variables in the problem. // All the signed representation of the problem literals must be in // [-num_variables, num_variables], excluding 0. @@ -93,7 +87,8 @@ message LinearBooleanProblem { // The constraints of the problem. repeated LinearBooleanConstraint constraints = 4; - // The objective of the problem (for the MINIMIZATION or MAXIMIZATION types). + // The objective of the problem. + // If left empty, we just have a satisfiability problem. optional LinearObjective objective = 5; // The names of the problem variables. The variables index are 0-based and diff --git a/src/sat/clause.cc b/src/sat/clause.cc index 80b53d0cad..62417de381 100644 --- a/src/sat/clause.cc +++ b/src/sat/clause.cc @@ -60,6 +60,7 @@ bool CleanUpPredicate(const Watcher& watcher) { LiteralWatchers::LiteralWatchers() : is_clean_(true), num_inspected_clauses_(0), + num_inspected_clause_literals_(0), num_watched_clauses_(0), stats_("LiteralWatchers") {} @@ -70,7 +71,7 @@ LiteralWatchers::~LiteralWatchers() { void LiteralWatchers::Resize(int num_variables) { DCHECK(is_clean_); watchers_on_false_.resize(num_variables << 1); - needs_cleaning_.resize(num_variables << 1, false); + needs_cleaning_.Resize(LiteralIndex(num_variables << 1)); statistics_.resize(num_variables); } @@ -100,6 +101,7 @@ bool LiteralWatchers::PropagateOnFalse(Literal false_literal, Trail* trail) { *new_it++ = *it; continue; } + ++num_inspected_clauses_; // If the other watched literal is true, just change the blocking literal. Literal* literals = it->clause->literals(); @@ -108,6 +110,7 @@ bool LiteralWatchers::PropagateOnFalse(Literal false_literal, Trail* trail) { if (other_watched_literal != it->blocking_literal && assignment.IsLiteralTrue(other_watched_literal)) { *new_it++ = Watcher(it->clause, other_watched_literal); + ++num_inspected_clause_literals_; continue; } @@ -116,6 +119,7 @@ bool LiteralWatchers::PropagateOnFalse(Literal false_literal, Trail* trail) { int i = 2; const int size = it->clause->Size(); while (i < size && assignment.IsLiteralFalse(literals[i])) ++i; + num_inspected_clause_literals_ += i; if (i < size) { // literal[i] is undefined or true, it's now the new literal to watch. // Note that by convention, we always keep the two watched literals at @@ -135,7 +139,7 @@ bool LiteralWatchers::PropagateOnFalse(Literal false_literal, Trail* trail) { trail->SetFailingSatClause( ClauseRef(it->clause->begin(), it->clause->end()), it->clause); trail->SetFailingResolutionNode(it->clause->ResolutionNodePointer()); - num_inspected_clauses_ += it - watchers.begin() + 1; + num_inspected_clause_literals_ += it - watchers.begin() + 1; watchers.erase(new_it, it); return false; } else { @@ -149,7 +153,7 @@ bool LiteralWatchers::PropagateOnFalse(Literal false_literal, Trail* trail) { *new_it++ = *it; } } - num_inspected_clauses_ += watchers.size(); + num_inspected_clause_literals_ += watchers.size(); watchers.erase(new_it, watchers.end()); return true; } @@ -166,7 +170,7 @@ bool LiteralWatchers::AttachAndPropagate(SatClause* clause, Trail* trail) { // Find a better way for the "initial" polarity choice and tie breaking // between literal choices. Note that it seems none of the modern SAT solver // relies on this. - if (clause->MustBeKept()) UpdateStatistics(*clause, /*added=*/true); + if (!clause->IsRedundant()) UpdateStatistics(*clause, /*added=*/true); clause->SortLiterals(statistics_, parameters_); return clause->AttachAndEnqueuePotentialUnitPropagation(trail, this); } @@ -174,22 +178,21 @@ bool LiteralWatchers::AttachAndPropagate(SatClause* clause, Trail* trail) { void LiteralWatchers::LazyDetach(SatClause* clause) { SCOPED_TIME_STAT(&stats_); --num_watched_clauses_; - if (clause->MustBeKept()) UpdateStatistics(*clause, /*added=*/false); + if (!clause->IsRedundant()) UpdateStatistics(*clause, /*added=*/false); clause->LazyDetach(); is_clean_ = false; - needs_cleaning_[clause->FirstLiteral().Index()] = true; - needs_cleaning_[clause->SecondLiteral().Index()] = true; + needs_cleaning_.Set(clause->FirstLiteral().Index()); + needs_cleaning_.Set(clause->SecondLiteral().Index()); } void LiteralWatchers::CleanUpWatchers() { SCOPED_TIME_STAT(&stats_); - for (int i = 0; i < needs_cleaning_.size(); ++i) { - if (needs_cleaning_[LiteralIndex(i)]) { - RemoveIf(&(watchers_on_false_[LiteralIndex(i)]), - CleanUpPredicate); - needs_cleaning_[LiteralIndex(i)] = false; - } + for (LiteralIndex index : needs_cleaning_.PositionsSetAtLeastOnce()) { + DCHECK(needs_cleaning_[index]); + RemoveIf(&(watchers_on_false_[index]), CleanUpPredicate); + needs_cleaning_.Clear(index); } + needs_cleaning_.NotifyAllClear(); is_clean_ = true; } @@ -237,6 +240,12 @@ void BinaryImplicationGraph::AddBinaryConflict(Literal a, Literal b, bool BinaryImplicationGraph::PropagateOnTrue(Literal true_literal, Trail* trail) { SCOPED_TIME_STAT(&stats_); + + // Note(user): This update is not exactly correct because in case of conflict + // we don't inspect that much clauses. But doing ++num_inspections_ inside the + // loop does slow down the code by a few percent. + num_inspections_ += implications_[true_literal.Index()].size(); + const VariablesAssignment& assignment = trail->Assignment(); for (Literal literal : implications_[true_literal.Index()]) { if (assignment.IsLiteralTrue(literal)) { @@ -464,7 +473,7 @@ void BinaryImplicationGraph::RemoveFixedVariables( // ----- SatClause ----- // static -SatClause* SatClause::Create(const std::vector& literals, ClauseType type, +SatClause* SatClause::Create(const std::vector& literals, bool is_redundant, ResolutionNode* node) { CHECK_GE(literals.size(), 2); SatClause* clause = reinterpret_cast( @@ -473,7 +482,7 @@ SatClause* SatClause::Create(const std::vector& literals, ClauseType ty for (int i = 0; i < literals.size(); ++i) { clause->literals_[i] = literals[i]; } - clause->must_be_kept_ = (type == PROBLEM_CLAUSE); + clause->is_redundant_ = is_redundant; clause->is_attached_ = false; clause->activity_ = 0.0; clause->lbd_ = 0; diff --git a/src/sat/clause.h b/src/sat/clause.h index 0155722185..e462db3884 100644 --- a/src/sat/clause.h +++ b/src/sat/clause.h @@ -61,13 +61,10 @@ struct VariableInfo { // the solver needs to keep a few extra fields attached to each clause. class SatClause { public: - // Creates a sat clause. There must be at least 2 literals. - // Smaller clause are treated separatly and never constructed. - enum ClauseType { - PROBLEM_CLAUSE, - LEARNED_CLAUSE, - }; - static SatClause* Create(const std::vector& literals, ClauseType type, + // Creates a sat clause. There must be at least 2 literals. Smaller clause are + // treated separatly and never constructed. A redundant clause can be removed + // without changing the problem. + static SatClause* Create(const std::vector& literals, bool is_redundant, ResolutionNode* node); // Number of literals in the clause. @@ -101,10 +98,10 @@ class SatClause { bool RemoveFixedLiteralsAndTestIfTrue(const VariablesAssignment& assignment, std::vector* removed_literals); - // True if the clause must be kept for the problem to remain the same. Usually - // the clause we learn during the search can be deleted if needed, so this - // will be false for them. - bool MustBeKept() const { return must_be_kept_; } + // True if the clause can be safely removed without changing the current + // problem. Usually the clause we learn during the search are redundant since + // the original clauses are enough to define the problem. + bool IsRedundant() const { return is_redundant_; } // Returns true if the clause is satisfied for the given assignment. Note that // the assignment may be partial, so false does not mean that the clause can't @@ -153,7 +150,7 @@ class SatClause { // Note that the max lbd is the maximum depth of the search tree (decision // levels), so it should fit easily in 30 bits. Note that we can also upper // bound it without hurting too much the clause cleaning heuristic. - bool must_be_kept_ : 1; + bool is_redundant_ : 1; bool is_attached_ : 1; int lbd_ : 30; int size_ : 32; @@ -205,6 +202,9 @@ class LiteralWatchers { // Total number of clauses inspected during calls to PropagateOnFalse(). int64 num_inspected_clauses() const { return num_inspected_clauses_; } + int64 num_inspected_clause_literals() const { + return num_inspected_clause_literals_; + } // Number of clauses currently watched. int64 num_watched_clauses() const { return num_watched_clauses_; } @@ -237,12 +237,13 @@ class LiteralWatchers { // Indicates if the corresponding watchers_on_false_ list need to be // cleaned. The boolean is_clean_ is just used in DCHECKs. - ITIVector needs_cleaning_; + SparseBitset needs_cleaning_; bool is_clean_; ITIVector statistics_; SatParameters parameters_; int64 num_inspected_clauses_; + int64 num_inspected_clause_literals_; int64 num_watched_clauses_; mutable StatsGroup stats_; DISALLOW_COPY_AND_ASSIGN(LiteralWatchers); @@ -281,11 +282,7 @@ class BinaryClauseManager { void ClearNewlyAdded() { newly_added_.clear(); } private: -#if defined(_MSC_VER) - hash_set, PairIntHasher> set_; -#else hash_set> set_; -#endif std::vector newly_added_; DISALLOW_COPY_AND_ASSIGN(BinaryClauseManager); }; @@ -327,6 +324,7 @@ class BinaryImplicationGraph { BinaryImplicationGraph() : num_implications_(0), num_propagations_(0), + num_inspections_(0), num_minimization_(0), num_literals_removed_(0), num_redundant_implications_(0), @@ -377,6 +375,9 @@ class BinaryImplicationGraph { // Number of literal propagated by this class (including conflicts). int64 num_propagations() const { return num_propagations_; } + // Number of literals inspected by this class during propagation. + int64 num_inspections() const { return num_inspections_; } + // MinimizeClause() stats. int64 num_minimization() const { return num_minimization_; } int64 num_literals_removed() const { return num_literals_removed_; } @@ -412,6 +413,7 @@ class BinaryImplicationGraph { // Some stats. int64 num_propagations_; + int64 num_inspections_; int64 num_minimization_; int64 num_literals_removed_; int64 num_redundant_implications_; diff --git a/src/sat/optimization.cc b/src/sat/optimization.cc index da04e82787..b29ba8370d 100644 --- a/src/sat/optimization.cc +++ b/src/sat/optimization.cc @@ -46,8 +46,7 @@ class Logger { std::string CnfObjectiveLine(const LinearBooleanProblem& problem, Coefficient objective) { const double scaled_objective = - objective.value() * problem.objective().scaling_factor() + - problem.objective().offset(); + AddOffsetAndScaleObjectiveValue(problem, objective); return StringPrintf("o %lld", static_cast(scaled_objective)); } @@ -224,7 +223,6 @@ SatSolver::Status SolveWithFuMalik(LogBehavior log, SatSolver* solver, std::vector* solution) { Logger logger(log); FuMalikSymmetryBreaker symmetry; - CHECK_EQ(problem.type(), LinearBooleanProblem::MINIMIZATION); // blocking_clauses will contains a set of clauses that are currently added to // the initial problem. @@ -418,7 +416,6 @@ SatSolver::Status SolveWithWPM1(LogBehavior log, SatSolver* solver, std::vector* solution) { Logger logger(log); FuMalikSymmetryBreaker symmetry; - CHECK_EQ(problem.type(), LinearBooleanProblem::MINIMIZATION); // The curent lower_bound on the cost. // It will be correct after the initialization. @@ -734,7 +731,6 @@ SatSolver::Status SolveWithRandomParameters(LogBehavior log, int num_times, SatSolver* solver, std::vector* solution) { Logger logger(log); - CHECK_EQ(problem.type(), LinearBooleanProblem::MINIMIZATION); const SatParameters initial_parameters = solver->parameters(); MTRandom random("A random seed."); @@ -815,7 +811,6 @@ SatSolver::Status SolveWithLinearScan(LogBehavior log, SatSolver* solver, std::vector* solution) { Logger logger(log); - CHECK_EQ(problem.type(), LinearBooleanProblem::MINIMIZATION); // This has a big positive impact on most problems. UseObjectiveForSatAssignmentPreference(problem, solver); diff --git a/src/sat/pb_constraint.cc b/src/sat/pb_constraint.cc index 2b33fe1f27..7fec8fe0d6 100644 --- a/src/sat/pb_constraint.cc +++ b/src/sat/pb_constraint.cc @@ -93,6 +93,39 @@ bool ComputeBooleanLinearExpressionCanonicalForm(std::vector* return true; } +bool ApplyLiteralMapping(const ITIVector& mapping, + std::vector* cst, + Coefficient* bound_shift, Coefficient* max_value) { + int index = 0; + Coefficient shift_due_to_fixed_variables(0); + for (const LiteralWithCoeff& entry : *cst) { + if (mapping[entry.literal.Index()] >= 0) { + VLOG(0) << entry.literal << " -> " + << Literal(mapping[entry.literal.Index()]); + (*cst)[index] = LiteralWithCoeff(Literal(mapping[entry.literal.Index()]), + entry.coefficient); + ++index; + } else if (mapping[entry.literal.Index()] == kTrueLiteralIndex) { + if (!SafeAddInto(-entry.coefficient, &shift_due_to_fixed_variables)) { + return false; + } + } else { + // Nothing to do if the literal is false. + DCHECK_EQ(mapping[entry.literal.Index()], kFalseLiteralIndex); + } + } + cst->resize(index); + if (cst->empty()) { + *bound_shift = shift_due_to_fixed_variables; + *max_value = 0; + return true; + } + const bool result = + ComputeBooleanLinearExpressionCanonicalForm(cst, bound_shift, max_value); + if (!SafeAddInto(shift_due_to_fixed_variables, bound_shift)) return false; + return result; +} + // TODO(user): Also check for no duplicates literals + unit tests. bool BooleanLinearExpressionIsCanonical(const std::vector& cst) { Coefficient previous(1); @@ -865,20 +898,23 @@ bool PbConstraints::PropagateNext() { thresholds_[update.index] - update.coefficient; thresholds_[update.index] = threshold; if (threshold < 0 && !conflict) { + UpperBoundedLinearConstraint* const cst = + constraints_[update.index.value()].get(); update.need_untrail_inspection = true; ++num_constraint_lookups_; - if (!constraints_[update.index.value()]->Propagate( - order, &thresholds_[update.index], trail_, - &conflict_scratchpad_)) { + const int old_value = cst->already_propagated_end(); + if (!cst->Propagate(order, &thresholds_[update.index], trail_, + &conflict_scratchpad_)) { trail_->SetFailingClause(ClauseRef(conflict_scratchpad_)); - trail_->SetFailingResolutionNode( - constraints_[update.index.value()]->ResolutionNodePointer()); + trail_->SetFailingResolutionNode(cst->ResolutionNodePointer()); conflicting_constraint_index_ = update.index; conflict = true; // We bump the activity of the conflict. BumpActivity(constraints_[update.index.value()].get()); } + num_inspected_constraint_literals_ += + old_value - cst->already_propagated_end(); } } return !conflict; diff --git a/src/sat/pb_constraint.h b/src/sat/pb_constraint.h index 4d6da6bdf8..a81b6a5fa1 100644 --- a/src/sat/pb_constraint.h +++ b/src/sat/pb_constraint.h @@ -69,6 +69,22 @@ bool ComputeBooleanLinearExpressionCanonicalForm(std::vector* Coefficient* bound_shift, Coefficient* max_value); +// Maps all the literals of the given constraint using the given mapping. The +// mapping may map a literal index to kTrueLiteralIndex or kFalseLiteralIndex in +// which case the literal will be considered fixed to the appropriate value. +// +// Note that this function also canonicalizes the constraint and updates +// bound_shift and max_value like ComputeBooleanLinearExpressionCanonicalForm() +// does. +// +// Finally, this will return false if some integer overflow or underflow occured +// during the constraint simplification. +const LiteralIndex kTrueLiteralIndex(-1); +const LiteralIndex kFalseLiteralIndex(-2); +bool ApplyLiteralMapping(const ITIVector& mapping, + std::vector* cst, + Coefficient* bound_shift, Coefficient* max_value); + // From a constraint 'expr <= ub' and the result (bound_shift, max_value) of // calling ComputeBooleanLinearExpressionCanonicalForm() on 'expr', this returns // a new rhs such that 'canonical expression <= rhs' is an equivalent @@ -421,6 +437,10 @@ class UpperBoundedLinearConstraint { // This is used for duplicate detection. int64 hash() const { return hash_; } + // This is used to get statistics of the number of literals inspected by a + // Propagate() call. + int already_propagated_end() const { return already_propagated_end_; } + private: Coefficient GetSlackFromThreshold(Coefficient threshold) { return (index_ < 0) ? threshold : coeffs_[index_] + threshold; @@ -471,6 +491,7 @@ class PbConstraints { constraint_activity_increment_(1.0), stats_("PbConstraints"), num_constraint_lookups_(0), + num_inspected_constraint_literals_(0), num_threshold_updates_(0) {} ~PbConstraints() { IF_STATS_ENABLED({ @@ -557,6 +578,13 @@ class PbConstraints { DeleteConstraintMarkedForDeletion(); } + // Some statistics. + int64 num_constraint_lookups() const { return num_constraint_lookups_; } + int64 num_inspected_constraint_literals() const { + return num_inspected_constraint_literals_; + } + int64 num_threshold_updates() const { return num_threshold_updates_; } + private: // Same function as the clause related one is SatSolver(). // TODO(user): Remove duplication. @@ -628,6 +656,7 @@ class PbConstraints { // Some statistics. mutable StatsGroup stats_; int64 num_constraint_lookups_; + int64 num_inspected_constraint_literals_; int64 num_threshold_updates_; DISALLOW_COPY_AND_ASSIGN(PbConstraints); }; diff --git a/src/sat/sat_base.h b/src/sat/sat_base.h index 1a1bcf4a52..19dbe246eb 100644 --- a/src/sat/sat_base.h +++ b/src/sat/sat_base.h @@ -125,6 +125,9 @@ class VariablesAssignment { bool IsLiteralTrue(Literal literal) const { return assignment_.IsSet(literal.Index()); } + bool IsLiteralAssigned(Literal literal) const { + return assignment_.AreOneOfTwoBitsSet(literal.Index()); + } // Returns true iff the given variable is assigned. bool IsVariableAssigned(VariableIndex var) const { @@ -378,7 +381,11 @@ class Trail { int Index() const { return trail_index_; } const Literal operator[](int index) const { return trail_[index]; } const VariablesAssignment& Assignment() const { return assignment_; } - const AssignmentInfo& Info(VariableIndex var) const { return info_[var]; } + const AssignmentInfo& Info(VariableIndex var) const { + DCHECK_GE(var, 0); + DCHECK_LT(var, info_.size()); + return info_[var]; + } // Sets the new resolution node for a variable that is fixed. void SetFixedVariableInfo(VariableIndex var, ResolutionNode* node) { diff --git a/src/sat/sat_parameters.proto b/src/sat/sat_parameters.proto index 3a2cfa8cc3..51a33f0a7f 100644 --- a/src/sat/sat_parameters.proto +++ b/src/sat/sat_parameters.proto @@ -17,7 +17,13 @@ package operations_research.sat; // Contains the definitions for all the sat algorithm parameters and their // default values. +// +// NEXT TAG: 68 message SatParameters { + // ========================================================================== + // Branching and polarity + // ========================================================================== + // Variables without activity (i.e. at the beginning of the search) will be // tried in this preferred order. enum VariableOrder { @@ -66,6 +72,11 @@ message SatParameters { // initially and then always taking this choice. optional double random_polarity_ratio = 45 [default = 0.0]; + // A number between 0 and 1 that indicates the proportion of branching + // variables that are selected randomly instead of choosing the first variable + // from the given variable_ordering strategy. + optional double random_branches_ratio = 32 [default = 0]; + // Specifies how literals should be initially sorted in a clause. enum LiteralOrdering { // Do nothing and keep literals in their current order. @@ -79,6 +90,10 @@ message SatParameters { } optional LiteralOrdering literal_ordering = 3 [default = LITERAL_IN_ORDER]; + // ========================================================================== + // Conflict analysis + // ========================================================================== + // Do we try to minimize conflicts (greedily) when creating them. enum ConflictMinimizationAlgorithm { NONE = 0; @@ -89,20 +104,63 @@ message SatParameters { optional ConflictMinimizationAlgorithm minimization_algorithm = 4 [default = RECURSIVE]; - // 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 = 1500]; + // Whether to expoit the binary clause to minimize learned clauses further. + // This will have an effect only if treat_binary_clauses_separately is true. + enum BinaryMinizationAlgorithm { + NO_BINARY_MINIMIZATION = 0; + BINARY_MINIMIZATION_FIRST = 1; + BINARY_MINIMIZATION_WITH_REACHABILITY = 2; + EXPERIMENTAL_BINARY_MINIMIZATION = 3; + } + optional BinaryMinizationAlgorithm binary_minimization_algorithm = 34 + [default = BINARY_MINIMIZATION_FIRST]; - // Deletes this ratio of clauses during each cleanup. + // At a really low cost, during the 1-UIP conflict computation, it is easy to + // detect if some of the involved reasons are subsumed by the current + // conflict. When this is true, such clauses are detached and later removed + // from the problem. + optional bool subsumption_during_conflict_analysis = 56 [default = true]; + + // ========================================================================== + // Clause database management + // ========================================================================== + + // During a cleanup, we will always keep that number of "deletable" clauses. + // Note that this only influences the start of the search if + // clause_cleanup_increment is not zero. + optional int32 clause_cleanup_min_target = 58 [default = 15000]; + + // Each time the learned clause database is cleaned, we want to keep this + // number of extra "deletable" clauses after the next cleaning. + optional int32 clause_cleanup_increment = 11 [default = 0]; + + // All the clauses with a LBD (literal blocks distance) lower or equal to this + // parameters will always be kept. + optional int32 clause_cleanup_lbd_bound = 59 [default = 5]; + + // The next cleanup phase will happen when the number of new "deletable" + // clause goes over 1 / ratio times the target number. optional double clause_cleanup_ratio = 13 [default = 0.5]; + // The clauses that will be kept during a cleanup are the ones that come + // first under this order. + enum ClauseOrdering { + // Order clause by decreasing activity. + CLAUSE_ACTIVITY = 0; + // Order clause by increasing LBD, then by decreasing activity. + CLAUSE_LBD = 1; + } + optional ClauseOrdering clause_cleanup_ordering = 60 + [default = CLAUSE_ACTIVITY]; + // Same as for the clauses, but for the learned pseudo-Boolean constraints. optional double pb_cleanup_increment = 46 [default = 200]; optional double pb_cleanup_ratio = 47 [default = 0.5]; - // Variable activity parameters. - // + // ========================================================================== + // Variable and clause activities + // ========================================================================== + // Each time a conflict is found, the activities of some variables are // increased by one. Then, the activity of all variables are multiplied by // variable_activity_decay. @@ -127,61 +185,69 @@ message SatParameters { optional double clause_activity_decay = 17 [default = 0.999]; optional double max_clause_activity_value = 18 [default = 1e20]; - // Whether or not we take the LBD (literal blocks distance) into account - // during the conflict cleaning phase. If true, then clauses with an LBD of - // 2 will not be deleted and clauses will be ordered by increasing LBD first - // with a tie breaking given by decreasing activity. - optional bool use_lbd = 20 [default = true]; - // 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 = false]; - // Frequecy of periodic restart if > 0. A negative value indicates - // no restart. - optional int32 restart_period = 30 [default = 100]; + // ========================================================================== + // Restart + // ========================================================================== - // At the beginning of each solve, the random number generator used in some - // part of the solver is reinitialized to this seed. If you change the random - // seed, the solver may make different choices during the solving process. + // Restart algorithms. // - // For some problems, the running time may vary a lot depending on small - // change in the solving algorithm. Running the solver with different seeds - // enables to have more robust benchmarks when evaluating new features. - optional int32 random_seed = 31 [default = 1]; + // A reference for the more advanced ones is: + // Gilles Audemard, Laurent Simon, "Refining Restarts Strategies for SAT + // and UNSAT", Principles and Practice of Constraint Programming Lecture + // Notes in Computer Science 2012, pp 118-126 + enum RestartAlgorithm { + NO_RESTART = 0; - // A number between 0 and 1 that indicates the proportion of branching - // variables that are selected randomly instead of choosing the first variable - // from the given variable_ordering strategy. - optional double random_branches_ratio = 32 [default = 0]; + // Just follow a Luby sequence times luby_restart_period. + LUBY_RESTART = 1; - // If true, the binary clauses are treated separately from the others. This - // should be faster and uses less memory. However it changes the propagation - // order. - optional bool treat_binary_clauses_separately = 33 [default = true]; + // Moving average restart based on the decision level of conflicts. + DL_MOVING_AVERAGE_RESTART = 2; - // Whether to expoit the binary clause to minimize learned clauses further. - // This will have an effect only if treat_binary_clauses_separately is true. - enum BinaryMinizationAlgorithm { - NO_BINARY_MINIMIZATION = 0; - BINARY_MINIMIZATION_FIRST = 1; - BINARY_MINIMIZATION_WITH_REACHABILITY = 2; - EXPERIMENTAL_BINARY_MINIMIZATION = 3; + // Moving average restart based on the LBD of conflicts. + LBD_MOVING_AVERAGE_RESTART = 3; } - optional BinaryMinizationAlgorithm binary_minimization_algorithm = 34 - [default = BINARY_MINIMIZATION_FIRST]; + optional RestartAlgorithm restart_algorithm = 61 + [default = DL_MOVING_AVERAGE_RESTART]; - // For an optimization problem, whether we follow some hints in order to find - // a better first solution. For a variable with hint, the solver will always - // try to follow the hint. It will revert to the variable_branching default - // otherwise. - optional bool use_optimization_hints = 35 [default = true]; + // Multiplier for the LUBY_RESTART algorithm. + optional int32 luby_restart_period = 30 [default = 100]; + + // Size of the window for the moving average restarts. + optional int32 restart_running_window_size = 62 [default = 50]; + + // In the moving average restart algorithms, a restart is triggered if the + // window average times this ratio is greater that the global average. + optional double restart_average_ratio = 63 [default = 1.0]; + + // Block a moving restart algorithm if the trail size of the current conflict + // is greater than the multiplier times the moving average of the trail size + // at the previous conflicts. + optional bool use_blocking_restart = 64 [default = false]; + optional int32 blocking_restart_window_size = 65 [default = 5000]; + optional double blocking_restart_multiplier = 66 [default = 1.4]; + + // ========================================================================== + // Limits + // ========================================================================== // Maximum time allowed in seconds to solve a problem. - // The counter will starts as soon as Solve() is called. + // The counter will starts as soon as SetParameters() or SolveWithTimeLimit() + // is called. optional double max_time_in_seconds = 36 [default = inf]; + // Maximum time allowed in deterministic time to solve a problem. + // The deterministic time should be correlated with the real time used by the + // solver, the time unit being as close as possible to a second. + // The counter will starts as soon as SetParameters() or SolveWithTimeLimit() + // is called. + optional double max_deterministic_time = 67 [default = inf]; + // Maximum number of conflicts allowed to solve a problem. optional int64 max_number_of_conflicts = 37 [default = 0x7FFFFFFFFFFFFFFF]; // kint64max @@ -192,6 +258,24 @@ message SatParameters { // much over. optional int64 max_memory_in_mb = 40 [default = 6000]; + // ========================================================================== + // Other parameters + // ========================================================================== + + // If true, the binary clauses are treated separately from the others. This + // should be faster and uses less memory. However it changes the propagation + // order. + optional bool treat_binary_clauses_separately = 33 [default = true]; + + // At the beginning of each solve, the random number generator used in some + // part of the solver is reinitialized to this seed. If you change the random + // seed, the solver may make different choices during the solving process. + // + // For some problems, the running time may vary a lot depending on small + // change in the solving algorithm. Running the solver with different seeds + // enables to have more robust benchmarks when evaluating new features. + optional int32 random_seed = 31 [default = 1]; + // Whether the solver should log the search progress to LOG(INFO). optional bool log_search_progress = 41 [default = false]; @@ -224,15 +308,32 @@ message SatParameters { // in Computer Science Volume 7962, 2013, pp 309-317. optional bool count_assumption_levels_in_lbd = 49 [default = true]; - // During presolve, only try to perform the bounded variable elimination of a - // variable x if the number of occurences of x times the number of occurences - // of not(x) is not greater than this parameter. - optional int32 presolve_bce_threshold = 54 [default = 100]; + // ========================================================================== + // Presolve + // ========================================================================== + + // During presolve, only try to perform the bounded variable elimination (BVE) + // of a variable x if the number of occurences of x times the number of + // occurences of not(x) is not greater than this parameter. + optional int32 presolve_bve_threshold = 54 [default = 500]; + + // During presolve, we apply BVE only if this weight times the number of + // clauses plus the number of clause literals is not increased. + optional int32 presolve_bve_clause_weight = 55 [default = 3]; + + // The "deterministic" time limit to spend in probing. + optional double presolve_probing_deterministic_time_limit = 57 [default = 10]; // ========================================================================== - // Max-sat parameters. + // Max-sat parameters // ========================================================================== + // For an optimization problem, whether we follow some hints in order to find + // a better first solution. For a variable with hint, the solver will always + // try to follow the hint. It will revert to the variable_branching default + // otherwise. + optional bool use_optimization_hints = 35 [default = true]; + // Whether we use a simple heuristic to try to minimize an UNSAT core. optional bool minimize_core = 50 [default = true]; @@ -249,7 +350,7 @@ message SatParameters { // max_sat_assumption_order. optional bool max_sat_reverse_assumption_order = 52 [default = false]; - // What stratification algorithm we use in the presence of weigth. + // What stratification algorithm we use in the presence of weight. enum MaxSatStratificationAlgorithm { // No stratification of the problem. STRATIFICATION_NONE = 0; diff --git a/src/sat/sat_solver.cc b/src/sat/sat_solver.cc index 67f7a79124..cc0f61c48d 100644 --- a/src/sat/sat_solver.cc +++ b/src/sat/sat_solver.cc @@ -51,6 +51,9 @@ SatSolver::SatSolver() restart_count_(0), same_reason_identifier_(trail_), is_relevant_for_core_computation_(true), + time_limit_(new TimeLimit(std::numeric_limits::infinity(), + std::numeric_limits::infinity())), + deterministic_time_at_last_advanced_time_limit_(0.0), stats_("SatSolver") { SetParameters(parameters_); } @@ -81,6 +84,7 @@ SatSolver::~SatSolver() { void SatSolver::SetNumVariables(int num_variables) { SCOPED_TIME_STAT(&stats_); + DCHECK(!is_model_unsat_); CHECK_GE(num_variables, num_variables_); num_variables_ = num_variables; binary_implication_graph_.Resize(num_variables); @@ -115,6 +119,23 @@ int64 SatSolver::num_propagations() const { return trail_.NumberOfEnqueues() - counters_.num_branches; } +double SatSolver::deterministic_time() const { + // Each of these counters mesure really basic operations. + // The weight are just an estimate of the operation complexity. + // + // TODO(user): Find a better procedure to fix the weight than just educated + // guess. + return 1e-8 * (8.0 * trail_.NumberOfEnqueues() + + 1.0 * binary_implication_graph_.num_inspections() + + 4.0 * watched_clauses_.num_inspected_clauses() + + 1.0 * watched_clauses_.num_inspected_clause_literals() + + + // Here there is a factor 2 because of the untrail. + 20.0 * pb_constraints_.num_constraint_lookups() + + 2.0 * pb_constraints_.num_threshold_updates() + + 1.0 * pb_constraints_.num_inspected_constraint_literals()); +} + const SatParameters& SatSolver::parameters() const { SCOPED_TIME_STAT(&stats_); return parameters_; @@ -128,7 +149,12 @@ void SatSolver::SetParameters(const SatParameters& parameters) { trail_.SetNeedFixedLiteralsInReason(parameters.unsat_proof()); random_.Reset(parameters_.random_seed()); InitRestart(); - time_limit_.reset(new TimeLimit(parameters_.max_time_in_seconds())); + time_limit_.reset(new TimeLimit(parameters_.max_time_in_seconds(), + parameters_.max_deterministic_time())); + dl_running_average_.Reset(parameters_.restart_running_window_size()); + lbd_running_average_.Reset(parameters_.restart_running_window_size()); + trail_size_running_average_.Reset(parameters_.blocking_restart_window_size()); + deterministic_time_at_last_advanced_time_limit_ = deterministic_time(); } std::string SatSolver::Indent() const { @@ -147,7 +173,7 @@ bool SatSolver::IsMemoryLimitReached() const { return memory_usage > kMegaByte * parameters_.max_memory_in_mb(); } -bool SatSolver::ModelUnsat() { +bool SatSolver::SetModelUnsat() { is_model_unsat_ = true; return false; } @@ -155,11 +181,12 @@ bool SatSolver::ModelUnsat() { bool SatSolver::AddUnitClause(Literal true_literal) { SCOPED_TIME_STAT(&stats_); CHECK_EQ(CurrentDecisionLevel(), 0); - if (trail_.Assignment().IsLiteralFalse(true_literal)) return ModelUnsat(); + if (is_model_unsat_) return false; + if (trail_.Assignment().IsLiteralFalse(true_literal)) return SetModelUnsat(); if (trail_.Assignment().IsLiteralTrue(true_literal)) return true; trail_.EnqueueWithUnitReason(true_literal, CreateRootResolutionNode()); ++num_constraints_; - if (!Propagate()) return ModelUnsat(); + if (!Propagate()) return SetModelUnsat(); return true; } @@ -225,13 +252,13 @@ bool SatSolver::AddProblemClauseInternal(const std::vector& literals, } // Create a new clause. std::unique_ptr clause( - SatClause::Create(literals, SatClause::PROBLEM_CLAUSE, node)); + SatClause::Create(literals, /*is_redundant=*/false, node)); if (parameters_.treat_binary_clauses_separately() && clause->Size() == 2) { AddBinaryClauseInternal(clause->FirstLiteral(), clause->SecondLiteral()); } else { if (!watched_clauses_.AttachAndPropagate(clause.get(), &trail_)) { - return ModelUnsat(); + return SetModelUnsat(); } clauses_.push_back(clause.release()); } @@ -243,7 +270,7 @@ bool SatSolver::AddLinearConstraintInternal(const std::vector& Coefficient max_value) { SCOPED_TIME_STAT(&stats_); DCHECK(BooleanLinearExpressionIsCanonical(cst)); - if (rhs < 0) return ModelUnsat(); // Unsatisfiable constraint. + if (rhs < 0) return SetModelUnsat(); // Unsatisfiable constraint. if (rhs >= max_value) return true; // Always satisfied constraint. // Create the associated resolution node. @@ -323,7 +350,8 @@ bool SatSolver::AddLinearConstraint(bool use_lower_bound, if (use_upper_bound) { const Coefficient rhs = ComputeCanonicalRhs(upper_bound, bound_shift, max_value); - if (!AddLinearConstraintInternal(*cst, rhs, max_value)) return ModelUnsat(); + if (!AddLinearConstraintInternal(*cst, rhs, max_value)) + return SetModelUnsat(); } if (use_lower_bound) { // We transform the constraint into an upper-bounded one. @@ -332,41 +360,48 @@ bool SatSolver::AddLinearConstraint(bool use_lower_bound, } const Coefficient rhs = ComputeNegatedCanonicalRhs(lower_bound, bound_shift, max_value); - if (!AddLinearConstraintInternal(*cst, rhs, max_value)) return ModelUnsat(); + if (!AddLinearConstraintInternal(*cst, rhs, max_value)) + return SetModelUnsat(); } ++num_constraints_; - if (!Propagate()) return ModelUnsat(); + if (!Propagate()) return SetModelUnsat(); return true; } void SatSolver::AddLearnedClauseAndEnqueueUnitPropagation( - const std::vector& literals, ResolutionNode* node) { + const std::vector& literals, bool is_redundant, ResolutionNode* node) { SCOPED_TIME_STAT(&stats_); if (literals.size() == 1) { // A length 1 clause fix a literal for all the search. // ComputeBacktrackLevel() should have returned 0. CHECK_EQ(CurrentDecisionLevel(), 0); trail_.EnqueueWithUnitReason(literals[0], node); - } else { - if (parameters_.treat_binary_clauses_separately() && literals.size() == 2) { - if (track_binary_clauses_) { - CHECK(binary_clauses_.Add(BinaryClause(literals[0], literals[1]))); - } - binary_implication_graph_.AddBinaryConflict(literals[0], literals[1], - &trail_); - } else { - SatClause* clause = - SatClause::Create(literals, SatClause::LEARNED_CLAUSE, node); - CompressLearnedClausesIfNeeded(); - --num_learned_clause_before_cleanup_; - clauses_.emplace_back(clause); - BumpClauseActivity(clause); - - // Important: Even though the only literal at the last decision level has - // been unassigned, its level was not modified, so ComputeLbd() works. - clause->SetLbd(parameters_.use_lbd() ? ComputeLbd(*clause) : 0); - CHECK(watched_clauses_.AttachAndPropagate(clause, &trail_)); + lbd_running_average_.Add(1); + } else if (literals.size() == 2 && + parameters_.treat_binary_clauses_separately()) { + if (track_binary_clauses_) { + CHECK(binary_clauses_.Add(BinaryClause(literals[0], literals[1]))); } + binary_implication_graph_.AddBinaryConflict(literals[0], literals[1], + &trail_); + lbd_running_average_.Add(2); + } else { + CleanClauseDatabaseIfNeeded(); + SatClause* clause = SatClause::Create(literals, is_redundant, node); + clauses_.emplace_back(clause); + BumpClauseActivity(clause); + + // Important: Even though the only literal at the last decision level has + // been unassigned, its level was not modified, so ComputeLbd() works. + clause->SetLbd(ComputeLbd(*clause)); + if (!ClauseShouldBeKept(clause)) { + --num_learned_clause_before_cleanup_; + } + + // Maintain the lbd average for the restart policy. + lbd_running_average_.Add(clause->Lbd()); + + CHECK(watched_clauses_.AttachAndPropagate(clause, &trail_)); } } @@ -429,10 +464,27 @@ bool SatSolver::PBConstraintIsValidUnderDebugAssignment( return sum <= rhs; } +namespace { + +// Returns true iff 'b' is subsumed by a (i.e 'a' is included in 'b'). +// This is slow and only meant to be used in DCHECKs. +bool ClauseSubsumption(const std::vector& a, SatClause* b) { + std::vector superset(b->begin(), b->end()); + std::vector subset(a.begin(), a.end()); + std::sort(superset.begin(), superset.end()); + std::sort(subset.begin(), subset.end()); + return std::includes(superset.begin(), subset.end(), subset.begin(), + subset.end()); +} + +} // namespace + int SatSolver::EnqueueDecisionAndBackjumpOnConflict(Literal true_literal) { SCOPED_TIME_STAT(&stats_); CHECK_EQ(propagation_trail_index_, trail_.Index()); + if (is_model_unsat_) return kUnsatTrailIndex; + // We are back at level 0. This can happen because of a restart, or because // we proved that some variables must take a given value in any satisfiable // assignment. Trigger a simplification of the clauses if there is new fixed @@ -451,6 +503,22 @@ int SatSolver::EnqueueDecisionAndBackjumpOnConflict(Literal true_literal) { NewDecision(true_literal); while (!Propagate()) { ++counters_.num_failures; + dl_running_average_.Add(current_decision_level_); + trail_size_running_average_.Add(trail_.Index()); + + // Block the restart. + // Note(user): glucose only activate this after 10000 conflicts. + if (parameters_.use_blocking_restart()) { + if (lbd_running_average_.IsWindowFull() && + dl_running_average_.IsWindowFull() && + trail_size_running_average_.IsWindowFull() && + trail_.Index() > parameters_.blocking_restart_multiplier() * + trail_size_running_average_.WindowAverage()) { + dl_running_average_.ClearWindow(); + lbd_running_average_.ClearWindow(); + } + } + const int max_trail_index = ComputeMaxTrailIndex(trail_.FailingClause()); // Optimization. All the activity of the variables assigned after the trail @@ -460,9 +528,9 @@ int SatSolver::EnqueueDecisionAndBackjumpOnConflict(Literal true_literal) { // A conflict occured, compute a nice reason for this failure. same_reason_identifier_.Clear(); - ComputeFirstUIPConflict(trail_.FailingClause(), max_trail_index, - &learned_conflict_, - &reason_used_to_infer_the_conflict_); + ComputeFirstUIPConflict(max_trail_index, &learned_conflict_, + &reason_used_to_infer_the_conflict_, + &subsumed_clauses_); // An empty conflict means that the problem is UNSAT. if (learned_conflict_.empty()) { @@ -476,10 +544,9 @@ int SatSolver::EnqueueDecisionAndBackjumpOnConflict(Literal true_literal) { // Also update the activity of the last level variables expanded (and // thus discarded) during the first UIP computation. Note that both // sets are disjoint. - const int lbd_limit = - parameters_.use_lbd() && parameters_.use_glucose_bump_again_strategy() - ? ComputeLbd(learned_conflict_) - : 0; + const int lbd_limit = parameters_.use_glucose_bump_again_strategy() + ? ComputeLbd(learned_conflict_) + : 0; BumpVariableActivities(learned_conflict_, lbd_limit); BumpVariableActivities(reason_used_to_infer_the_conflict_, lbd_limit); @@ -589,6 +656,7 @@ int SatSolver::EnqueueDecisionAndBackjumpOnConflict(Literal true_literal) { // Continue with the normal clause flow, but use the PB conflict clause // if it has a lower backjump level. if (pb_backjump_level < ComputeBacktrackLevel(learned_conflict_)) { + subsumed_clauses_.clear(); // Because the conflict changes. learned_conflict_.clear(); is_marked_.ClearAndResize(num_variables_); int max_level = 0; @@ -666,9 +734,25 @@ int SatSolver::EnqueueDecisionAndBackjumpOnConflict(Literal true_literal) { counters_.num_literals_learned += learned_conflict_.size(); Backtrack(ComputeBacktrackLevel(learned_conflict_)); first_propagation_index = trail_.Index(); - DCHECK(ClauseIsValidUnderDebugAssignement(learned_conflict_)); - AddLearnedClauseAndEnqueueUnitPropagation(learned_conflict_, node); + + // Detach any subsumed clause. They will actually be deleted on the next + // clause cleanup phase. + bool is_redundant = true; + if (!subsumed_clauses_.empty() && + parameters_.subsumption_during_conflict_analysis()) { + for (SatClause* clause : subsumed_clauses_) { + DCHECK(ClauseSubsumption(learned_conflict_, clause)); + watched_clauses_.LazyDetach(clause); + if (!clause->IsRedundant()) is_redundant = false; + } + watched_clauses_.CleanUpWatchers(); + counters_.num_subsumed_clauses += subsumed_clauses_.size(); + } + + // Create and attach the new learned clause. + AddLearnedClauseAndEnqueueUnitPropagation(learned_conflict_, is_redundant, + node); } return first_propagation_index; } @@ -714,6 +798,8 @@ SatSolver::Status SatSolver::ReapplyDecisionsUpTo( int SatSolver::EnqueueDecisionAndBacktrackOnConflict(Literal true_literal) { SCOPED_TIME_STAT(&stats_); CHECK_EQ(propagation_trail_index_, trail_.Index()); + + if (is_model_unsat_) return kUnsatTrailIndex; decisions_[CurrentDecisionLevel()].literal = true_literal; int first_propagation_index = trail_.Index(); ReapplyDecisionsUpTo(CurrentDecisionLevel(), &first_propagation_index); @@ -723,6 +809,8 @@ int SatSolver::EnqueueDecisionAndBacktrackOnConflict(Literal true_literal) { bool SatSolver::EnqueueDecisionIfNotConflicting(Literal true_literal) { SCOPED_TIME_STAT(&stats_); CHECK_EQ(propagation_trail_index_, trail_.Index()); + + if (is_model_unsat_) return kUnsatTrailIndex; const int current_level = CurrentDecisionLevel(); NewDecision(true_literal); if (Propagate()) { @@ -735,6 +823,9 @@ bool SatSolver::EnqueueDecisionIfNotConflicting(Literal true_literal) { void SatSolver::Backtrack(int target_level) { SCOPED_TIME_STAT(&stats_); + // TODO(user): The backtrack method should not be called when the model is + // unsat. Add a DCHECK to prevent that, but before fix the + // bop::BopOptimizerBase architecture. // Do nothing if the CurrentDecisionLevel() is already correct. // This is needed, otherwise target_trail_index below will remain at zero and @@ -763,11 +854,11 @@ bool SatSolver::AddBinaryClauses(const std::vector& clauses) { for (BinaryClause c : clauses) { if (trail_.Assignment().IsLiteralFalse(c.a) && trail_.Assignment().IsLiteralFalse(c.b)) { - return ModelUnsat(); + return SetModelUnsat(); } AddBinaryClauseInternal(c.a, c.b); } - if (!Propagate()) return ModelUnsat(); + if (!Propagate()) return SetModelUnsat(); return true; } @@ -788,6 +879,7 @@ int NextMultipleOf(int64 value, int64 interval) { void SatSolver::SetAssignmentPreference(Literal literal, double weight) { SCOPED_TIME_STAT(&stats_); + DCHECK(!is_model_unsat_); if (!is_decision_heuristic_initialized_) ResetDecisionHeuristic(); if (!parameters_.use_optimization_hints()) return; DCHECK_GE(weight, 0.0); @@ -804,13 +896,14 @@ void SatSolver::SetAssignmentPreference(Literal literal, double weight) { SatSolver::Status SatSolver::ResetAndSolveWithGivenAssumptions( const std::vector& assumptions) { SCOPED_TIME_STAT(&stats_); + DCHECK(!is_model_unsat_); CHECK_LE(assumptions.size(), num_variables_); Backtrack(0); for (int i = 0; i < assumptions.size(); ++i) { decisions_[i].literal = assumptions[i]; } assumption_level_ = assumptions.size(); - return Solve(); + return SolveInternal(time_limit_.get()); } SatSolver::Status SatSolver::StatusWithLog(Status status) { @@ -822,12 +915,17 @@ SatSolver::Status SatSolver::StatusWithLog(Status status) { } void SatSolver::SetAssumptionLevel(int assumption_level) { + DCHECK(!is_model_unsat_); CHECK_GE(assumption_level, 0); CHECK_LE(assumption_level, CurrentDecisionLevel()); assumption_level_ = assumption_level; } SatSolver::Status SatSolver::Solve() { + return SolveInternal(time_limit_.get()); +} + +SatSolver::Status SatSolver::SolveInternal(TimeLimit* time_limit) { SCOPED_TIME_STAT(&stats_); if (is_model_unsat_) return MODEL_UNSAT; timer_.Restart(); @@ -870,11 +968,19 @@ SatSolver::Status SatSolver::Solve() { // Starts search. for (;;) { // Test if a limit is reached. - if (time_limit_ != nullptr && time_limit_->LimitReached()) { - if (parameters_.log_search_progress()) { - LOG(INFO) << "The time limit has been reached. Aborting."; + if (time_limit != nullptr) { + const double current_deterministic_time = deterministic_time(); + time_limit->AdvanceDeterministicTime( + current_deterministic_time - + deterministic_time_at_last_advanced_time_limit_); + deterministic_time_at_last_advanced_time_limit_ = + current_deterministic_time; + if (time_limit->LimitReached()) { + if (parameters_.log_search_progress()) { + LOG(INFO) << "The time limit has been reached. Aborting."; + } + return StatusWithLog(LIMIT_REACHED); } - return StatusWithLog(LIMIT_REACHED); } if (num_failures() >= kFailureLimit) { if (parameters_.log_search_progress()) { @@ -919,11 +1025,39 @@ SatSolver::Status SatSolver::Solve() { return StatusWithLog(MODEL_SAT); } - // Trigger the restart policy? - if (conflicts_until_next_restart_ == 0) { + // Restart? + bool restart = false; + switch (parameters_.restart_algorithm()) { + case SatParameters::NO_RESTART: + break; + case SatParameters::LUBY_RESTART: + if (conflicts_until_next_restart_ == 0) { + restart = true; + conflicts_until_next_restart_ = + parameters_.luby_restart_period() * SUniv(restart_count_ + 1); + } + break; + case SatParameters::DL_MOVING_AVERAGE_RESTART: + if (dl_running_average_.IsWindowFull() && + dl_running_average_.GlobalAverage() < + parameters_.restart_average_ratio() * + dl_running_average_.WindowAverage()) { + restart = true; + dl_running_average_.ClearWindow(); + } + break; + case SatParameters::LBD_MOVING_AVERAGE_RESTART: + if (lbd_running_average_.IsWindowFull() && + lbd_running_average_.GlobalAverage() < + parameters_.restart_average_ratio() * + lbd_running_average_.WindowAverage()) { + restart = true; + lbd_running_average_.ClearWindow(); + } + break; + } + if (restart) { restart_count_++; - conflicts_until_next_restart_ = - parameters_.restart_period() * SUniv(restart_count_ + 1); Backtrack(assumption_level_); } @@ -936,9 +1070,9 @@ SatSolver::Status SatSolver::Solve() { } } -SatSolver::Status SatSolver::SolveWithTimeLimit(double max_time_in_seconds) { - time_limit_.reset(new TimeLimit(max_time_in_seconds)); - return Solve(); +SatSolver::Status SatSolver::SolveWithTimeLimit(TimeLimit* time_limit) { + deterministic_time_at_last_advanced_time_limit_ = deterministic_time(); + return SolveInternal(time_limit); } std::vector SatSolver::GetLastIncompatibleDecisions() { @@ -954,12 +1088,15 @@ std::vector SatSolver::GetLastIncompatibleDecisions() { is_marked_.Set(false_assumption.Variable()); int trail_index = trail_.Info(false_assumption.Variable()).trail_index; + const int limit = + CurrentDecisionLevel() > 0 ? decisions_[0].trail_index : trail_.Index(); + CHECK_LT(trail_index, trail_.Index()); while (true) { // Find next marked literal to expand from the trail. while (trail_index >= 0 && !is_marked_[trail_[trail_index].Variable()]) { --trail_index; } - if (trail_index < 0) break; + if (trail_index < limit) break; const Literal marked_literal = trail_[trail_index]; --trail_index; @@ -992,7 +1129,7 @@ void SatSolver::BumpVariableActivities(const std::vector& literals, if (level == 0) continue; if (level == CurrentDecisionLevel() && trail_.Info(var).type == AssignmentInfo::CLAUSE_PROPAGATION && - !trail_.Info(var).sat_clause->MustBeKept() && + trail_.Info(var).sat_clause->IsRedundant() && trail_.Info(var).sat_clause->Lbd() < bump_again_lbd_limit) { activities_[var] += variable_activity_increment_; } @@ -1022,7 +1159,7 @@ void SatSolver::BumpReasonActivities(const std::vector& literals) { } void SatSolver::BumpClauseActivity(SatClause* clause) { - if (clause->MustBeKept()) return; + if (!clause->IsRedundant()) return; clause->IncreaseActivity(clause_activity_increment_); if (clause->Activity() > parameters_.max_clause_activity_value()) { RescaleClauseActivities(1.0 / parameters_.max_clause_activity_value()); @@ -1144,6 +1281,8 @@ std::string SatSolver::StatusString(Status status) const { static_cast(num_propagations()) / time_in_s) + StringPrintf(" num binary propagations: %" GG_LL_FORMAT "d\n", binary_implication_graph_.num_propagations()) + + StringPrintf(" num binary inspections: %" GG_LL_FORMAT "d\n", + binary_implication_graph_.num_inspections()) + StringPrintf(" num classic minimizations: %" GG_LL_FORMAT "d" " (literals removed: %" GG_LL_FORMAT "d)\n", @@ -1156,6 +1295,8 @@ std::string SatSolver::StatusString(Status status) const { binary_implication_graph_.num_literals_removed()) + StringPrintf(" num inspected clauses: %" GG_LL_FORMAT "d\n", watched_clauses_.num_inspected_clauses()) + + StringPrintf(" num inspected clause_literals: %" GG_LL_FORMAT "d\n", + watched_clauses_.num_inspected_clause_literals()) + StringPrintf( " num learned literals: %lld (avg: %.1f /clause)\n", counters_.num_literals_learned, @@ -1164,7 +1305,22 @@ std::string SatSolver::StatusString(Status status) const { counters_.num_learned_pb_literals_, 1.0 * counters_.num_learned_pb_literals_ / counters_.num_failures) + - StringPrintf(" num restarts: %d\n", restart_count_); + StringPrintf(" num subsumed clauses: %lld\n", + counters_.num_subsumed_clauses) + + StringPrintf(" num restarts: %d\n", restart_count_) + + StringPrintf(" pb num threshold updates: %lld\n", + pb_constraints_.num_threshold_updates()) + + StringPrintf(" pb num constraint lookups: %lld\n", + pb_constraints_.num_constraint_lookups()) + + StringPrintf(" pb num inspected constraint literals: %lld\n", + pb_constraints_.num_inspected_constraint_literals()) + + StringPrintf(" conflict decision level avg: %f\n", + dl_running_average_.GlobalAverage()) + + StringPrintf(" conflict lbd avg: %f\n", + lbd_running_average_.GlobalAverage()) + + StringPrintf(" conflict trail size avg: %f\n", + trail_size_running_average_.GlobalAverage()) + + StringPrintf(" deterministic time: %f\n", deterministic_time()); } std::string SatSolver::RunningStatisticsString() const { @@ -1186,12 +1342,12 @@ void SatSolver::ProcessNewlyFixedVariableResolutionNodes() { CHECK_NE(info.type, AssignmentInfo::SEARCH_DECISION); CHECK_NE(info.type, AssignmentInfo::BINARY_PROPAGATION); - // We need this loop to remove the propagated literal from the reason. - // TODO(user): The reason should probably not contains the propagated - // literal in the first place. Clean that up. - literals_scratchpad_.clear(); - for (Literal literal : Reason(trail_[i].Variable())) { - if (literal != trail_[i]) literals_scratchpad_.push_back(literal); + // DCHECK that the reason doesn't contain the propagated literal (it used + // to, so this check that it is properly removed). + if (DEBUG_MODE) { + for (Literal literal : Reason(trail_[i].Variable())) { + CHECK_NE(literal.Variable(), trail_[i].Variable()); + } } // Note that this works because level 0 literals are part of the reason @@ -1200,7 +1356,11 @@ void SatSolver::ProcessNewlyFixedVariableResolutionNodes() { CreateResolutionNode(info.type == AssignmentInfo::CLAUSE_PROPAGATION ? info.sat_clause->ResolutionNodePointer() : info.pb_constraint->ResolutionNodePointer(), - ClauseRef(literals_scratchpad_)); + Reason(trail_[i].Variable())); + + // This will also allow us to delete the underlying clause in + // ProcessNewlyFixedVariables() in a safe way since it will no longer be + // referenced anywhere. trail_.SetFixedVariableInfo(trail_[i].Variable(), new_node); } } @@ -1227,7 +1387,11 @@ void SatSolver::ProcessNewlyFixedVariables() { } else if (!removed_literals.empty()) { if (clause->Size() == 2 && parameters_.treat_binary_clauses_separately()) { - // The clause is now a binary clause, treat it separately. + // The clause is now a binary clause, treat it separately. Note that + // if it was used as a reason for a variable x, the variable must not + // be unassigned (since we are at level 0, and the clause is of size > + // 1). So this it is okay to delete the clause completely (it will be + // done at the end of the function). AddBinaryClauseInternal(clause->FirstLiteral(), clause->SecondLiteral()); watched_clauses_.LazyDetach(clause); @@ -1243,25 +1407,13 @@ void SatSolver::ProcessNewlyFixedVariables() { } } } + watched_clauses_.CleanUpWatchers(); if (num_detached_clauses > 0) { VLOG(1) << trail_.Index() << " fixed variables at level 0. " << "Detached " << num_detached_clauses << " clauses. " << num_binary << " converted to binary."; - - // Free-up learned clause memory. Note that this also postpone a bit the - // next clause cleaning phase since we removed some clauses. - std::vector::iterator iter = std::partition( - clauses_.begin(), clauses_.end(), - std::bind1st(std::mem_fun(&SatSolver::IsClauseAttachedOrUsedAsReason), - this)); - if (parameters_.unsat_proof()) { - for (std::vector::iterator it = iter; it != clauses_.end(); ++it) { - unsat_proof_.UnlockNode((*it)->ResolutionNodePointer()); - } - } - STLDeleteContainerPointers(iter, clauses_.end()); - clauses_.erase(iter, clauses_.end()); + DeleteDetachedClauses(); } // We also clean the binary implication graph. @@ -1269,6 +1421,22 @@ void SatSolver::ProcessNewlyFixedVariables() { num_processed_fixed_variables_ = trail_.Index(); } +namespace { +bool IsClauseAttached(SatClause* a) { return a->IsAttached(); } +} // namespace + +void SatSolver::DeleteDetachedClauses() { + std::vector::iterator iter = + std::partition(clauses_.begin(), clauses_.end(), IsClauseAttached); + if (parameters_.unsat_proof()) { + for (std::vector::iterator it = iter; it != clauses_.end(); ++it) { + unsat_proof_.UnlockNode((*it)->ResolutionNodePointer()); + } + } + STLDeleteContainerPointers(iter, clauses_.end()); + clauses_.erase(iter, clauses_.end()); +} + bool SatSolver::Propagate() { SCOPED_TIME_STAT(&stats_); @@ -1365,6 +1533,13 @@ ClauseRef SatSolver::Reason(VariableIndex var) { } } +SatClause* SatSolver::ReasonClauseOrNull(VariableIndex var) const { + DCHECK(trail_.Assignment().IsVariableAssigned(var)); + const AssignmentInfo& info = trail_.Info(var); + if (info.type == AssignmentInfo::CLAUSE_PROPAGATION) return info.sat_clause; + return nullptr; +} + bool SatSolver::ResolvePBConflict(VariableIndex var, MutableUpperBoundedLinearConstraint* conflict, Coefficient* slack) { @@ -1551,6 +1726,8 @@ void SatSolver::InitializeVariableOrdering() { } void SatSolver::ResetDecisionHeuristic() { + DCHECK(!is_model_unsat_); + // Note that this will never be false again. is_decision_heuristic_initialized_ = true; @@ -1728,8 +1905,9 @@ int SatSolver::ComputeMaxTrailIndex(ClauseRef clause) const { // http://www.cs.tau.ac.il/~msagiv/courses/ATP/iccad2001_final.pdf // http://gauss.ececs.uc.edu/SAT/articles/FAIA185-0131.pdf void SatSolver::ComputeFirstUIPConflict( - ClauseRef failing_clause, int max_trail_index, std::vector* conflict, - std::vector* reason_used_to_infer_the_conflict) { + int max_trail_index, std::vector* conflict, + std::vector* reason_used_to_infer_the_conflict, + std::vector* subsumed_clauses) { SCOPED_TIME_STAT(&stats_); // This will be used to mark all the literals inspected while we process the @@ -1738,12 +1916,13 @@ void SatSolver::ComputeFirstUIPConflict( conflict->clear(); reason_used_to_infer_the_conflict->clear(); + subsumed_clauses->clear(); if (max_trail_index == -1) return; // max_trail_index is the maximum trail index appearing in the failing_clause // and its level (Which is almost always equals to the CurrentDecisionLevel(), // except for symmetry propagation). - DCHECK_EQ(max_trail_index, ComputeMaxTrailIndex(failing_clause)); + DCHECK_EQ(max_trail_index, ComputeMaxTrailIndex(trail_.FailingClause())); int trail_index = max_trail_index; const int highest_level = DecisionLevel(trail_[trail_index].Variable()); if (highest_level == 0) return; @@ -1763,13 +1942,16 @@ void SatSolver::ComputeFirstUIPConflict( // // This last literal will be the first UIP because by definition all the // propagation done at the current level will pass though it at some point. - ClauseRef clause_to_expand = failing_clause; + ClauseRef clause_to_expand = trail_.FailingClause(); + SatClause* sat_clause = trail_.FailingSatClause(); DCHECK(!clause_to_expand.IsEmpty()); int num_literal_at_highest_level_that_needs_to_be_processed = 0; while (true) { + int num_new_vars = 0; for (const Literal literal : clause_to_expand) { const VariableIndex var = literal.Variable(); if (!is_marked_[var]) { + ++num_new_vars; is_marked_.Set(var); const int level = DecisionLevel(var); if (level == highest_level) { @@ -1785,6 +1967,25 @@ void SatSolver::ComputeFirstUIPConflict( } } + // If there is new variables, then all the previously subsumed clauses are + // not subsumed anymore. + if (num_new_vars > 0) { + // TODO(user): We could still replace all these clauses with the current + // conflict. + subsumed_clauses->clear(); + } + + // This check if the new conflict is exactly equal to clause_to_expand. + // Since we just performed an union, comparing the size is enough. When this + // is true, then the current conflict subsumes the reason whose underlying + // clause is given by sat_clause. + if (sat_clause != nullptr && + clause_to_expand.size() == + conflict->size() + + num_literal_at_highest_level_that_needs_to_be_processed) { + subsumed_clauses->push_back(sat_clause); + } + // Find next marked literal to expand from the trail. DCHECK_GT(num_literal_at_highest_level_that_needs_to_be_processed, 0); while (!is_marked_[trail_[trail_index].Variable()]) { @@ -1816,6 +2017,7 @@ void SatSolver::ComputeFirstUIPConflict( clause_to_expand = Reason(literal.Variable()); DCHECK(!clause_to_expand.IsEmpty()); } + sat_clause = ReasonClauseOrNull(literal.Variable()); --num_literal_at_highest_level_that_needs_to_be_processed; --trail_index; @@ -2358,36 +2560,49 @@ void SatSolver::MinimizeConflictExperimental(std::vector* conflict) { namespace { +// Order the clauses by decreasing activity. +bool ActivityClauseOrder(SatClause* a, SatClause* b) { + return a->Activity() > b->Activity(); +} + // Order the clause by increasing LBD (Literal Blocks Distance) first. For the // same LBD they are ordered by decreasing activity. -bool ClauseOrdering(SatClause* a, SatClause* b) { +bool LbdClauseOrder(SatClause* a, SatClause* b) { if (a->Lbd() == b->Lbd()) return a->Activity() > b->Activity(); return a->Lbd() < b->Lbd(); } } // namespace -void SatSolver::InitLearnedClauseLimit(int current_num_learned) { +void SatSolver::InitLearnedClauseLimit(int current_num_deletable) { target_number_of_learned_clauses_ = - current_num_learned + parameters_.clause_cleanup_increment(); + std::max(parameters_.clause_cleanup_min_target(), + current_num_deletable + parameters_.clause_cleanup_increment()); num_learned_clause_before_cleanup_ = target_number_of_learned_clauses_ / parameters_.clause_cleanup_ratio() - - current_num_learned; - VLOG(1) << "reduced learned database to " << current_num_learned + current_num_deletable; + VLOG(1) << "reduced learned database to " << current_num_deletable << " clauses. Next cleanup in " << num_learned_clause_before_cleanup_ << " conflicts."; } -void SatSolver::CompressLearnedClausesIfNeeded() { +void SatSolver::CleanClauseDatabaseIfNeeded() { if (num_learned_clause_before_cleanup_ > 0) return; SCOPED_TIME_STAT(&stats_); + // Start by removing all the detached clauses (if any). + DeleteDetachedClauses(); + // Move the clause that should be kept at the beginning and sort the other - // using the ClauseOrdering order. + // using the specified clause ordering. std::vector::iterator clause_to_keep_end = std::partition( clauses_.begin(), clauses_.end(), std::bind1st(std::mem_fun(&SatSolver::ClauseShouldBeKept), this)); - std::sort(clause_to_keep_end, clauses_.end(), ClauseOrdering); + if (parameters_.clause_cleanup_ordering() == SatParameters::CLAUSE_LBD) { + std::sort(clause_to_keep_end, clauses_.end(), LbdClauseOrder); + } else { + std::sort(clause_to_keep_end, clauses_.end(), ActivityClauseOrder); + } // Delete all the clause after first_clause_to_delete (if any). std::vector::iterator first_clause_to_delete = @@ -2411,11 +2626,11 @@ void SatSolver::CompressLearnedClausesIfNeeded() { void SatSolver::InitRestart() { SCOPED_TIME_STAT(&stats_); restart_count_ = 0; - if (parameters_.restart_period() > 0) { - DCHECK_EQ(SUniv(1), 1); - conflicts_until_next_restart_ = parameters_.restart_period(); - } else { + if (parameters_.restart_algorithm() == SatParameters::NO_RESTART) { conflicts_until_next_restart_ = -1; + } else if (parameters_.restart_algorithm() == SatParameters::LUBY_RESTART) { + DCHECK_EQ(SUniv(1), 1); + conflicts_until_next_restart_ = parameters_.luby_restart_period(); } } diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 69e9c2ec9f..ecf1bd0997 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -38,6 +38,7 @@ #include "sat/symmetry.h" #include "sat/unsat_proof.h" #include "util/bitset.h" +#include "util/running_stat.h" #include "util/stats.h" #include "util/time_limit.h" #include "base/adjustable_priority_queue.h" @@ -120,6 +121,7 @@ class SatSolver { // // TODO(user): This currently can't be used with unsat_proof() on. Fix it. void AddSymmetries(std::vector>* generators) { + DCHECK(!is_model_unsat_); for (int i = 0; i < generators->size(); ++i) { symmetry_propagator_.AddSymmetry(std::move((*generators)[i])); } @@ -131,6 +133,7 @@ class SatSolver { // ignored (and thus save memory during the solve). This starts with a value // of true. void SetNextConstraintsRelevanceForUnsatCore(bool value) { + DCHECK(!is_model_unsat_); is_relevant_for_core_computation_ = value; } @@ -138,7 +141,7 @@ class SatSolver { // will also be the unique index associated to the next constraint that will // be added. This unique index is used by UnsatCore() to indicates what // constraints are part of the core. - int NumAddedConstraints() const { return num_constraints_; } + int NumAddedConstraints() { return num_constraints_; } // Gives a hint so the solver tries to find a solution with the given literal // set to true. Currently this take precedence over the phase saving heuristic @@ -160,12 +163,17 @@ class SatSolver { // Solves the problem and returns its status. // - // Note that the time or conflict limit applies only to this function and - // starts counting from the time it is called. + // Note that the conflict limit applies only to this function and starts + // counting from the time it is called. // // This will restart from the current solver configuration. If a previous call // to Solve() was interupted by a conflict or time limit, calling this again // will resume the search exactly as it would have continued. + // + // Note that if a time limit has been defined earlier, using the SAT + // parameters or the SolveWithTimeLimit() method, it is still in use in this + // solve. To override the timelimit one should reset the parameters or use the + // SolveWithTimeLimit() with a new time limit. enum Status { ASSUMPTIONS_UNSAT, MODEL_UNSAT, @@ -174,11 +182,12 @@ class SatSolver { }; Status Solve(); - // Same as Solve(), but with a given time limit in seconds. Note that this is - // slightly redundant with the max_time_in_seconds() parameter, but because - // SetParameters() resets more than just the time limit, it is useful to have - // this more specific api. - Status SolveWithTimeLimit(double max_time_in_seconds); + // Same as Solve(), but with a given time limit. Note that this is slightly + // redundant with the max_time_in_seconds() and + // max_time_in_deterministic_seconds() parameters, but because SetParameters() + // resets more than just the time limit, it is useful to have this more + // specific api. + Status SolveWithTimeLimit(TimeLimit* time_limit); // Simple interface to solve a problem under the given assumptions. This // simply ask the solver to solve a problem given a set of variables fixed to @@ -288,7 +297,7 @@ class SatSolver { // currently process the clauses in order. binary_implication_graph_.ExtractAllBinaryClauses(out); for (SatClause* clause : clauses_) { - if (clause->MustBeKept()) { + if (!clause->IsRedundant()) { out->AddClause(ClauseRef(clause->begin(), clause->end())); } } @@ -318,6 +327,11 @@ class SatSolver { int64 num_failures() const; int64 num_propagations() const; + // A deterministic number that should be correlated with the time spent in + // the Solve() function. The order of magnitude should be close to the time + // in seconds. + double deterministic_time() const; + // Only used for debugging. Save the current assignment in debug_assignment_. // The idea is that if we know that a given assignment is satisfiable, then // all the learned clauses or PB constraints must be satisfiable by it. In @@ -326,6 +340,9 @@ class SatSolver { void SaveDebugAssignment(); private: + // All Solve() functions end up calling this one. + Status SolveInternal(TimeLimit* time_limit); + // Adds a binary clause to the BinaryImplicationGraph and to the // BinaryClauseManager when track_binary_clauses_ is true. void AddBinaryClauseInternal(Literal a, Literal b); @@ -366,7 +383,7 @@ class SatSolver { bool IsMemoryLimitReached() const; // Sets is_model_unsat_ to true and return false. - bool ModelUnsat(); + bool SetModelUnsat(); // Utility function to insert spaces proportional to the search depth. // It is used in the pretty print of the search. @@ -387,6 +404,7 @@ class SatSolver { // better to do as little work as possible during Enqueue() and more work // here. In particular, generating a reason clause lazily make sense. ClauseRef Reason(VariableIndex var); + SatClause* ReasonClauseOrNull(VariableIndex var) const; // This does one step of a pseudo-Boolean resolution: // - The variable var has been assigned to l at a given trail_index. @@ -414,15 +432,11 @@ class SatSolver { trail_.Info(var).sat_clause == clause; } - // Predicate used by ProcessNewlyFixedVariables(). - bool IsClauseAttachedOrUsedAsReason(SatClause* clause) const { - return clause->IsAttached() || IsClauseUsedAsReason(clause); - } - - // Predicate used by CompressLearnedClausesIfNeeded(). + // Predicate used by CleanClauseDatabaseIfNeeded(). bool ClauseShouldBeKept(SatClause* clause) const { - return clause->MustBeKept() || clause->Lbd() <= 2 || clause->Size() <= 2 || - IsClauseUsedAsReason(clause); + return !clause->IsRedundant() || + clause->Lbd() <= parameters_.clause_cleanup_lbd_bound() || + clause->Size() <= 2 || IsClauseUsedAsReason(clause); } // Add a problem clause. Not that the clause is assumed to be "cleaned", that @@ -441,7 +455,7 @@ class SatSolver { // literals of the learned close except one will be false. Thus the last one // will be implied True. This function also Enqueue() the implied literal. void AddLearnedClauseAndEnqueueUnitPropagation( - const std::vector& literals, ResolutionNode* node); + const std::vector& literals, bool must_be_kept, ResolutionNode* node); // Creates a new decision which corresponds to setting the given literal to // True and Enqueue() this change. @@ -464,6 +478,9 @@ class SatSolver { // needed because level zero variables are treated differently by the solver. void ProcessNewlyFixedVariableResolutionNodes(); + // Deletes all the clauses that are detached. + void DeleteDetachedClauses(); + // Simplifies the problem when new variables are assigned at level 0. void ProcessNewlyFixedVariables(); @@ -487,8 +504,9 @@ class SatSolver { // IEEE/ACM international conference on Computer-aided design, Pages 279-285. // http://www.cs.tau.ac.il/~msagiv/courses/ATP/iccad2001_final.pdf void ComputeFirstUIPConflict( - ClauseRef failing_clause, int max_trail_index, std::vector* conflict, - std::vector* reason_used_to_infer_the_conflict); + int max_trail_index, std::vector* conflict, + std::vector* reason_used_to_infer_the_conflict, + std::vector* subsumed_clauses); // Given an assumption (i.e. literal) currently assigned to false, this will // returns the set of all assumptions that caused this particular assignment. @@ -565,7 +583,7 @@ class SatSolver { // Checks if we need to reduce the number of learned clauses and do // it if needed. The second function updates the learned clause limit. - void CompressLearnedClausesIfNeeded(); + void CleanClauseDatabaseIfNeeded(); void InitLearnedClauseLimit(int current_num_learned); // Bumps the activity of all variables appearing in the conflict. @@ -672,6 +690,7 @@ class SatSolver { // Clause learning /deletion stats. int64 num_literals_learned; int64 num_literals_forgotten; + int64 num_subsumed_clauses; Counters() : num_branches(0), @@ -681,7 +700,8 @@ class SatSolver { num_literals_removed(0), num_learned_pb_literals_(0), num_literals_learned(0), - num_literals_forgotten(0) {} + num_literals_forgotten(0), + num_subsumed_clauses(0) {} }; Counters counters_; @@ -801,6 +821,7 @@ class SatSolver { // Temporary vectors used by EnqueueDecisionAndBackjumpOnConflict(). std::vector learned_conflict_; std::vector reason_used_to_infer_the_conflict_; + std::vector subsumed_clauses_; // "cache" to avoid inspecting many times the same reason during conflict // analysis. @@ -830,9 +851,19 @@ class SatSolver { // The current pseudo-Boolean conflict used in PB conflict analysis. MutableUpperBoundedLinearConstraint pb_conflict_; + // Running average used by some restart algorithms. + RunningAverage dl_running_average_; + RunningAverage lbd_running_average_; + RunningAverage trail_size_running_average_; + // The solver time limit. std::unique_ptr time_limit_; + // The deterministic time when the time limit was updated. + // As the deterministic time in the time limit has to be advanced manually, + // it is necessary to keep track of the last time the time was advanced. + double deterministic_time_at_last_advanced_time_limit_; + mutable StatsGroup stats_; DISALLOW_COPY_AND_ASSIGN(SatSolver); }; diff --git a/src/sat/simplification.cc b/src/sat/simplification.cc index b52c921ce0..3878f80228 100644 --- a/src/sat/simplification.cc +++ b/src/sat/simplification.cc @@ -14,10 +14,58 @@ #include "sat/simplification.h" #include "base/timer.h" +#include "algorithms/dynamic_partition.h" namespace operations_research { namespace sat { +SatPostsolver::SatPostsolver(int num_variables) { + reverse_mapping_.resize(num_variables); + for (VariableIndex var(0); var < num_variables; ++var) { + reverse_mapping_[var] = var; + } + assignment_.Resize(num_variables); +} + +void SatPostsolver::Add(Literal x, std::vector* clause) { + CHECK(!clause->empty()); + DCHECK(std::find(clause->begin(), clause->end(), x) != clause->end()); + clauses_.push_back(std::vector()); + clauses_.back().swap(*clause); + associated_literal_.push_back(ApplyReverseMapping(x)); + for (Literal& l_ref : clauses_.back()) { + l_ref = ApplyReverseMapping(l_ref); + } +} + +void SatPostsolver::FixVariable(Literal x) { + Literal l = ApplyReverseMapping(x); + CHECK(!assignment_.IsLiteralAssigned(l)); + assignment_.AssignFromTrueLiteral(l); +} + +void SatPostsolver::ApplyMapping( + const ITIVector& mapping) { + ITIVector new_mapping(reverse_mapping_.size(), + VariableIndex(-1)); + for (VariableIndex v(0); v < mapping.size(); ++v) { + const VariableIndex image = mapping[v]; + if (image != VariableIndex(-1)) { + CHECK_EQ(new_mapping[image], VariableIndex(-1)); + CHECK_LT(v, reverse_mapping_.size()); + CHECK_NE(reverse_mapping_[v], VariableIndex(-1)); + new_mapping[image] = reverse_mapping_[v]; + } + } + std::swap(new_mapping, reverse_mapping_); +} + +Literal SatPostsolver::ApplyReverseMapping(Literal l) { + CHECK_LT(l.Variable(), reverse_mapping_.size()); + CHECK_NE(reverse_mapping_[l.Variable()], VariableIndex(-1)); + return Literal(reverse_mapping_[l.Variable()], l.IsPositive()); +} + void SatPostsolver::Postsolve(VariablesAssignment* assignment) const { // First, we set all unassigned variable to true. // This will be a valid assignment of the presolved problem. @@ -43,6 +91,34 @@ void SatPostsolver::Postsolve(VariablesAssignment* assignment) const { } } +std::vector SatPostsolver::ExtractAndPostsolveSolution( + const SatSolver& solver) { + std::vector solution(solver.NumVariables()); + for (VariableIndex var(0); var < solver.NumVariables(); ++var) { + CHECK(solver.Assignment().IsVariableAssigned(var)); + solution[var.value()] = + solver.Assignment().IsLiteralTrue(Literal(var, true)); + } + return PostsolveSolution(solution); +} + +std::vector SatPostsolver::PostsolveSolution(const std::vector& solution) { + for (VariableIndex var(0); var < solution.size(); ++var) { + CHECK_LT(var, reverse_mapping_.size()); + CHECK_NE(reverse_mapping_[var], VariableIndex(-1)); + CHECK(!assignment_.IsVariableAssigned(reverse_mapping_[var])); + assignment_.AssignFromTrueLiteral( + Literal(reverse_mapping_[var], solution[var.value()])); + } + Postsolve(&assignment_); + std::vector postsolved_solution; + for (int i = 0; i < reverse_mapping_.size(); ++i) { + postsolved_solution.push_back( + assignment_.IsLiteralTrue(Literal(VariableIndex(i), true))); + } + return postsolved_solution; +} + void SatPresolver::AddBinaryClause(Literal a, Literal b) { Literal c[2]; c[0] = a; @@ -51,43 +127,95 @@ void SatPresolver::AddBinaryClause(Literal a, Literal b) { } void SatPresolver::AddClause(ClauseRef clause) { - CHECK_GT(clause.size(), 0) << "TODO(fdid): Unsat during presolve?"; + CHECK_GT(clause.size(), 0) << "Added an empty clause to the presolver"; const ClauseIndex ci(clauses_.size()); clauses_.push_back(std::vector(clause.begin(), clause.end())); in_clause_to_process_.push_back(true); clause_to_process_.push_back(ci); - std::sort(clauses_.back().begin(), clauses_.back().end()); - const Literal max_literal = clauses_.back().back(); + + std::vector& clause_ref = clauses_.back(); + if (!equiv_mapping_.empty()) { + for (int i = 0; i < clause_ref.size(); ++i) { + clause_ref[i] = Literal(equiv_mapping_[clause_ref[i].Index()]); + } + } + std::sort(clause_ref.begin(), clause_ref.end()); + clause_ref.erase(std::unique(clause_ref.begin(), clause_ref.end()), + clause_ref.end()); + + // Check for trivial clauses: + for (int i = 1; i < clause_ref.size(); ++i) { + if (clause_ref[i] == clause_ref[i - 1].Negated()) { + // The clause is trivial! + ++num_trivial_clauses_; + clause_to_process_.pop_back(); + clauses_.pop_back(); + in_clause_to_process_.pop_back(); + return; + } + } + + const Literal max_literal = clause_ref.back(); const int required_size = std::max(max_literal.Index().value(), max_literal.NegatedIndex().value()) + 1; if (required_size > literal_to_clauses_.size()) { literal_to_clauses_.resize(required_size); - literal_to_clauses_sizes_.resize(required_size); + literal_to_clause_sizes_.resize(required_size); } - for (Literal e : clauses_.back()) { + for (Literal e : clause_ref) { literal_to_clauses_[e.Index()].push_back(ci); - literal_to_clauses_sizes_[e.Index()]++; - UpdatePriorityQueue(e.Variable()); + literal_to_clause_sizes_[e.Index()]++; } } -ITIVector SatPresolver::GetMapping( - int* new_size) const { +void SatPresolver::AddClauseInternal(std::vector* clause) { + CHECK_GT(clause->size(), 0) << "TODO(fdid): Unsat during presolve?"; + const ClauseIndex ci(clauses_.size()); + clauses_.push_back(std::vector()); + clauses_.back().swap(*clause); + in_clause_to_process_.push_back(true); + clause_to_process_.push_back(ci); + for (Literal e : clauses_.back()) { + literal_to_clauses_[e.Index()].push_back(ci); + literal_to_clause_sizes_[e.Index()]++; + } +} + +ITIVector SatPresolver::VariableMapping() const { ITIVector result; VariableIndex new_var(0); for (VariableIndex var(0); var < NumVariables(); ++var) { - if (literal_to_clauses_sizes_[Literal(var, true).Index()] > 0 || - literal_to_clauses_sizes_[Literal(var, false).Index()] > 0) { + if (literal_to_clause_sizes_[Literal(var, true).Index()] > 0 || + literal_to_clause_sizes_[Literal(var, false).Index()] > 0) { result.push_back(new_var); ++new_var; } else { result.push_back(VariableIndex(-1)); } } - *new_size = new_var.value(); return result; } +void SatPresolver::LoadProblemIntoSatSolver(SatSolver* solver) const { + const ITIVector mapping = VariableMapping(); + + int new_size = 0; + for (VariableIndex index : mapping) { + if (index != VariableIndex(-1)) ++new_size; + } + + std::vector temp; + solver->SetNumVariables(new_size); + for (const std::vector& clause : *this) { + temp.clear(); + for (Literal l : clause) { + CHECK_NE(mapping[l.Variable()], VariableIndex(-1)); + temp.push_back(Literal(mapping[l.Variable()], l.IsPositive())); + } + if (!temp.empty()) solver->AddProblemClause(temp); + } +} + bool SatPresolver::ProcessAllClauses() { while (!clause_to_process_.empty()) { const ClauseIndex ci = clause_to_process_.front(); @@ -101,6 +229,7 @@ bool SatPresolver::ProcessAllClauses() { bool SatPresolver::Presolve() { WallTimer timer; timer.Start(); + LOG(INFO) << "num trivial clauses: " << num_trivial_clauses_; DisplayStats(0); // TODO(user): When a clause is strengthened, add it to a queue so it can @@ -158,7 +287,7 @@ bool SatPresolver::ProcessClauseToSimplifyOthers(ClauseIndex clause_index) { DCHECK(iter != literal_to_clauses_[opposite_literal].end()); literal_to_clauses_[opposite_literal].erase(iter); - --literal_to_clauses_sizes_[opposite_literal]; + --literal_to_clause_sizes_[opposite_literal]; UpdatePriorityQueue(Literal(opposite_literal).Variable()); if (!in_clause_to_process_[ci]) { @@ -171,8 +300,8 @@ bool SatPresolver::ProcessClauseToSimplifyOthers(ClauseIndex clause_index) { ++new_index; } occurence_list_ref.resize(new_index); - CHECK_EQ(literal_to_clauses_sizes_[lit.Index()], new_index); - literal_to_clauses_sizes_[lit.Index()] = new_index; + CHECK_EQ(literal_to_clause_sizes_[lit.Index()], new_index); + literal_to_clause_sizes_[lit.Index()] = new_index; } // Now treat clause containing lit.Negated(). @@ -201,7 +330,7 @@ bool SatPresolver::ProcessClauseToSimplifyOthers(ClauseIndex clause_index) { ++new_index; } occurence_list_ref.resize(new_index); - literal_to_clauses_sizes_[lit.NegatedIndex()] = new_index; + literal_to_clause_sizes_[lit.NegatedIndex()] = new_index; if (something_removed) { UpdatePriorityQueue(Literal(lit.NegatedIndex()).Variable()); } @@ -214,70 +343,92 @@ void SatPresolver::RemoveAndRegisterForPostsolveAllClauseContaining(Literal x) { if (!clauses_[i].empty()) RemoveAndRegisterForPostsolve(i, x); } literal_to_clauses_[x.Index()].clear(); - literal_to_clauses_sizes_[x.Index()] = 0; + literal_to_clause_sizes_[x.Index()] = 0; } bool SatPresolver::CrossProduct(Literal x) { - const int s1 = literal_to_clauses_sizes_[x.Index()]; - const int s2 = literal_to_clauses_sizes_[x.NegatedIndex()]; + const int s1 = literal_to_clause_sizes_[x.Index()]; + const int s2 = literal_to_clause_sizes_[x.NegatedIndex()]; // Note that if s1 or s2 is equal to 0, this function will implicitely just // fix the variable x. if (s1 == 0 && s2 == 0) return false; + // Heuristic. Abort if the work required to decide if x should be removed + // seems to big. + if (s1 > 1 && s2 > 1 && s1 * s2 > parameters_.presolve_bve_threshold()) { + return false; + } + + // Compute the threshold under which we don't remove x.Variable(). + int threshold = 0; + const int clause_weight = parameters_.presolve_bve_clause_weight(); + for (ClauseIndex i : literal_to_clauses_[x.Index()]) { + if (!clauses_[i].empty()) { + threshold += clause_weight + clauses_[i].size(); + } + } + for (ClauseIndex i : literal_to_clauses_[x.NegatedIndex()]) { + if (!clauses_[i].empty()) { + threshold += clause_weight + clauses_[i].size(); + } + } + + // For the BCE, we prefer s2 to be small. + if (s1 < s2) x = x.Negated(); + + // Test whether we should remove the x.Variable(). + int size = 0; std::vector temp; - if (s1 > 1 && s2 > 1) { - // Heuristic. Abort if the work required to decide if x should be removed - // seems to big. - if (s1 * s2 > parameters_.presolve_bce_threshold()) return false; + for (ClauseIndex i : literal_to_clauses_[x.Index()]) { + if (clauses_[i].empty()) continue; + bool no_resolvant = true; + for (ClauseIndex j : literal_to_clauses_[x.NegatedIndex()]) { + if (clauses_[j].empty()) continue; - // Test whether we should remove the variable x.Variable(). - int size = 0; - for (ClauseIndex i : literal_to_clauses_[x.Index()]) { - if (clauses_[i].empty()) continue; - const int old_size = size; - for (ClauseIndex j : literal_to_clauses_[x.NegatedIndex()]) { - if (clauses_[j].empty()) continue; + // TODO(user): The output temp is not needed here. Optimize. + if (ComputeResolvant(x, clauses_[i], clauses_[j], &temp)) { + no_resolvant = false; + size += clause_weight + temp.size(); - // TODO(user): The output temp is not needed here. Optimize. - if (ComputeResolvant(x, clauses_[i], clauses_[j], &temp)) { - ++size; - - // Abort early if the resolution is producing more clauses than the - // ones it will eliminate. - if (size > s1 + s2) return false; - } - } - if (size == old_size) { - // This is an incomplete heuristic for blocked clause detection. Here, - // the clause i is "blocked", so we can remove it. Note that the code - // below already do that if we decide to eliminate x. - // - // For more details, see the paper "Blocked clause elimination", Matti - // Jarvisalo, Armin Biere, Marijn Heule. TACAS, volume 6015 of Lecture - // Notes in Computer Science, pages 129–144. Springer, 2010. - // - // TODO(user): Choose if we use x or x.Negated() depending on the list - // sizes? The function achieve the same if x = x.Negated(), however the - // loops are not done in the same order which may change this incomplete - // "blocked" clause detection. - RemoveAndRegisterForPostsolve(i, x); + // Abort early if the "size" become too big. + if (size > threshold) return false; } } + if (no_resolvant) { + // This is an incomplete heuristic for blocked clause detection. Here, + // the clause i is "blocked", so we can remove it. Note that the code + // below already do that if we decide to eliminate x. + // + // For more details, see the paper "Blocked clause elimination", Matti + // Jarvisalo, Armin Biere, Marijn Heule. TACAS, volume 6015 of Lecture + // Notes in Computer Science, pages 129–144. Springer, 2010. + // + // TODO(user): Choose if we use x or x.Negated() depending on the list + // sizes? The function achieve the same if x = x.Negated(), however the + // loops are not done in the same order which may change this incomplete + // "blocked" clause detection. + RemoveAndRegisterForPostsolve(i, x); + } } // Add all the resolvant clauses. + // Note that the variable priority queue will only be updated during the + // deletion. for (ClauseIndex i : literal_to_clauses_[x.Index()]) { if (clauses_[i].empty()) continue; for (ClauseIndex j : literal_to_clauses_[x.NegatedIndex()]) { if (clauses_[j].empty()) continue; if (ComputeResolvant(x, clauses_[i], clauses_[j], &temp)) { - AddClause(ClauseRef(temp)); + AddClauseInternal(&temp); } } } // Deletes the old clauses. + // + // TODO(user): We could only update the priority queue once for each variable + // instead of doing it many times. RemoveAndRegisterForPostsolveAllClauseContaining(x); RemoveAndRegisterForPostsolveAllClauseContaining(x.Negated()); @@ -288,7 +439,7 @@ bool SatPresolver::CrossProduct(Literal x) { void SatPresolver::Remove(ClauseIndex ci) { for (Literal e : clauses_[ci]) { - literal_to_clauses_sizes_[e.Index()]--; + literal_to_clause_sizes_[e.Index()]--; UpdatePriorityQueue(e.Variable()); } clauses_[ci].clear(); @@ -296,11 +447,11 @@ void SatPresolver::Remove(ClauseIndex ci) { void SatPresolver::RemoveAndRegisterForPostsolve(ClauseIndex ci, Literal x) { for (Literal e : clauses_[ci]) { - literal_to_clauses_sizes_[e.Index()]--; + literal_to_clause_sizes_[e.Index()]--; UpdatePriorityQueue(e.Variable()); } // This will copy and clear the clause. - postsolver_.Add(x, &clauses_[ci]); + postsolver_->Add(x, &clauses_[ci]); } Literal SatPresolver::FindLiteralWithShortestOccurenceList( @@ -308,8 +459,8 @@ Literal SatPresolver::FindLiteralWithShortestOccurenceList( CHECK(!clause.empty()); Literal result = clause.front(); for (Literal l : clause) { - if (literal_to_clauses_sizes_[l.Index()] < - literal_to_clauses_sizes_[result.Index()]) { + if (literal_to_clause_sizes_[l.Index()] < + literal_to_clause_sizes_[result.Index()]) { result = l; } } @@ -319,8 +470,8 @@ Literal SatPresolver::FindLiteralWithShortestOccurenceList( void SatPresolver::UpdatePriorityQueue(VariableIndex var) { if (var_pq_elements_.empty()) return; // not initialized. PQElement* element = &var_pq_elements_[var]; - element->weight = literal_to_clauses_sizes_[Literal(var, true).Index()] + - literal_to_clauses_sizes_[Literal(var, false).Index()]; + element->weight = literal_to_clause_sizes_[Literal(var, true).Index()] + + literal_to_clause_sizes_[Literal(var, false).Index()]; if (var_pq_.Contains(element)) { var_pq_.NoteChangedPriority(element); } else { @@ -334,8 +485,8 @@ void SatPresolver::InitializePriorityQueue() { for (VariableIndex var(0); var < num_vars; ++var) { PQElement* element = &var_pq_elements_[var]; element->variable = var; - element->weight = literal_to_clauses_sizes_[Literal(var, true).Index()] + - literal_to_clauses_sizes_[Literal(var, false).Index()]; + element->weight = literal_to_clause_sizes_[Literal(var, true).Index()] + + literal_to_clause_sizes_[Literal(var, false).Index()]; var_pq_.Add(element); } } @@ -355,8 +506,8 @@ void SatPresolver::DisplayStats(double elapsed_seconds) { int num_simple_definition = 0; int num_vars = 0; for (VariableIndex var(0); var < NumVariables(); ++var) { - const int s1 = literal_to_clauses_sizes_[Literal(var, true).Index()]; - const int s2 = literal_to_clauses_sizes_[Literal(var, false).Index()]; + const int s1 = literal_to_clause_sizes_[Literal(var, true).Index()]; + const int s2 = literal_to_clause_sizes_[Literal(var, false).Index()]; if (s1 == 0 && s2 == 0) continue; ++num_vars; @@ -449,5 +600,69 @@ bool ComputeResolvant(Literal x, const std::vector& a, return true; } +// A simple graph where the nodes are the literals and the nodes adjacent to a +// literal l are the propagated literal when l is assigned in the underlying +// sat solver. +// +// This can be used to do a strong component analysis while probing all the +// literals of a solver. Note that this can be expensive, hence the support +// for a deterministic time limit. +class PropagationGraph { + public: + PropagationGraph(double deterministic_time_limit, SatSolver* solver) + : solver_(solver), + deterministic_time_limit(solver->deterministic_time() + + deterministic_time_limit) {} + + // Returns the set of node adjacent to the given one. + // Interface needed by FindStronglyConnectedComponents(), note that it needs + // to be const. + const std::vector& operator[](int32 index) const { + scratchpad_.clear(); + solver_->Backtrack(0); + + // Note that when the time limit is reached, we just keep returning empty + // adjacency list. This way, the SCC algorithm will terminate quickly and + // the equivalent literals detection will be incomplete but correct. Note + // also that thanks to the SCC algorithm, we will explore the connected + // components first. + if (solver_->deterministic_time() > deterministic_time_limit) { + return scratchpad_; + } + + const Literal l = Literal(LiteralIndex(index)); + if (!solver_->Assignment().IsLiteralAssigned(l)) { + const int trail_index = solver_->LiteralTrail().Index(); + solver_->EnqueueDecisionAndBackjumpOnConflict(l); + if (solver_->CurrentDecisionLevel() > 0) { + // Note that the +1 is to avoid adding a => a. + for (int i = trail_index + 1; i < solver_->LiteralTrail().Index(); + ++i) { + scratchpad_.push_back(solver_->LiteralTrail()[i].Index().value()); + } + } + } + return scratchpad_; + } + + private: + mutable std::vector scratchpad_; + SatSolver* const solver_; + const double deterministic_time_limit; + + DISALLOW_COPY_AND_ASSIGN(PropagationGraph); +}; + +void ProbeAndFindEquivalentLiteral( + SatSolver* solver, SatPostsolver* postsolver, + ITIVector* mapping) { + solver->Backtrack(0); + mapping->clear(); + const int num_already_fixed_vars = solver->LiteralTrail().Index(); + + // Currently, this is not supported in the open-source version because we + // need to open source the strongly connected component algo first. +} + } // namespace sat } // namespace operations_research diff --git a/src/sat/simplification.h b/src/sat/simplification.h index bfa21d8636..5c99f4d475 100644 --- a/src/sat/simplification.h +++ b/src/sat/simplification.h @@ -24,29 +24,66 @@ #include "sat/sat_base.h" #include "sat/sat_parameters.pb.h" +#include "sat/sat_solver.h" #include "base/adjustable_priority_queue.h" namespace operations_research { namespace sat { -// A really simple postsolver that process the clause added in reverse order. -// If a clause has all its literals at false, it simply sets the literal -// that was registered with the clause to true. +// A simple sat postsolver. +// +// The idea is that any presolve algorithm can just update this class, and at +// the end, this class will recover a solution of the initial problem from a +// solution of the presolved problem. class SatPostsolver { public: - SatPostsolver() {} - void Add(Literal x, std::vector* clause) { - CHECK(!clause->empty()); - clauses_.push_back(std::vector()); - clauses_.back().swap(*clause); - associated_literal_.push_back(x); - } - void Postsolve(VariablesAssignment* assignment) const; + explicit SatPostsolver(int num_variables); + + // The postsolver will process the Add() calls in reverse order. If the given + // clause has all its literals at false, it simply sets the literal x to true. + // Note that x must be a literal of the given clause, and that the clause will + // be cleared. + void Add(Literal x, std::vector* clause); + + // Tells the postsolver that the given literal must be true in any solution. + // We currently check that the variable is not already fixed. + void FixVariable(Literal x); + + // This assumes that the given variable mapping has been applied to the + // problem. All the subsequent Add() and FixVariable() will refer to the new + // problem. During postsolve, the initial solution must also correspond to + // this new problem. Note that if mapping[v] == -1, then the literal v is + // assumed to be deleted. + // + // This can be called more than once. But each call must refer to the current + // variables set (after all the previous mapping have been applied). + void ApplyMapping(const ITIVector& mapping); + + // Extracts the current assignment of the given solver and postsolve it. + // + // Node(fdid): This can currently be called only once (but this is easy to + // change since only some CHECK will fail). + std::vector ExtractAndPostsolveSolution(const SatSolver& solver); + std::vector PostsolveSolution(const std::vector& solution); private: + Literal ApplyReverseMapping(Literal l); + void Postsolve(VariablesAssignment* assignment) const; + + // Stores the arguments of the Add() calls. std::vector> clauses_; std::vector associated_literal_; + + // All the added clauses will be mapped back to the initial variables using + // this reverse mapping. This way, clauses_ and associated_literal_ are only + // in term of the initial problem. + ITIVector reverse_mapping_; + + // This will stores the fixed variables value and later the postsolved + // assignment. + VariablesAssignment assignment_; + DISALLOW_COPY_AND_ASSIGN(SatPostsolver); }; @@ -69,9 +106,17 @@ class SatPresolver { // it is not really needed here. typedef int32 ClauseIndex; - SatPresolver() {} + explicit SatPresolver(SatPostsolver* postsolver) + : postsolver_(postsolver), num_trivial_clauses_(0) {} void SetParameters(const SatParameters& params) { parameters_ = params; } + // Registers a mapping to encode equivalent literals. + // See ProbeAndFindEquivalentLiteral(). + void SetEquivalentLiteralMapping( + const ITIVector& mapping) { + equiv_mapping_ = mapping; + } + // Adds new clause to the SatPresolver. void AddBinaryClause(Literal a, Literal b); void AddClause(ClauseRef clause); @@ -83,11 +128,6 @@ class SatPresolver { // so that this can never take too much time. bool Presolve(); - // Postsolve a SAT assignment of the presolved problem. - void Postsolve(VariablesAssignment* assignemnt) const { - postsolver_.Postsolve(assignemnt); - } - // All the clauses managed by this class. // Note that deleted clauses keep their indices (they are just empty). int NumClauses() const { return clauses_.size(); } @@ -105,9 +145,14 @@ class SatPresolver { // After presolving, Some variables in [0, NumVariables()) have no longer any // clause pointing to them. This return a mapping that maps this interval to - // [0, *new_size) such that now all variables are used. The unused variable + // [0, new_size) such that now all variables are used. The unused variable // will be mapped to VariableIndex(-1). - ITIVector GetMapping(int* new_size) const; + ITIVector VariableMapping() const; + + // Loads the current presolved problem in to the given sat solver. + // Note that the variables will be re-indexed according to the mapping given + // by GetMapping() so that they form a dense set. + void LoadProblemIntoSatSolver(SatSolver* solver) const; // Visible for Testing. Takes a given clause index and looks for clause that // can be subsumed or strengthened using this clause. Returns false if the @@ -123,6 +168,11 @@ class SatPresolver { bool CrossProduct(Literal x); private: + // Internal function to add clauses generated during the presolve. The clause + // must already be sorted with the default Literal order and will be cleared + // after this call. + void AddClauseInternal(std::vector* clause); + // Clause removal function. void Remove(ClauseIndex ci); void RemoveAndRegisterForPostsolve(ClauseIndex ci, Literal x); @@ -181,10 +231,15 @@ class SatPresolver { // Because we only lazily clean the occurence list after clause deletions, // we keep the size of the occurence list (without the deleted clause) here. - ITIVector literal_to_clauses_sizes_; + ITIVector literal_to_clause_sizes_; // Used for postsolve. - SatPostsolver postsolver_; + SatPostsolver* postsolver_; + + // Equivalent literal mapping. + ITIVector equiv_mapping_; + + int num_trivial_clauses_; SatParameters parameters_; DISALLOW_COPY_AND_ASSIGN(SatPresolver); @@ -213,6 +268,22 @@ bool SimplifyClause(const std::vector& a, std::vector* b, bool ComputeResolvant(Literal x, const std::vector& a, const std::vector& b, std::vector* out); +// Presolver that does literals probing and finds equivalent literals by +// computing the strongly connected components of the graph: +// literal l -> literals propagated by l. +// +// Clears the mapping if there are no equivalent literals. Otherwise, mapping[l] +// is the representative of the equivalent class of l. Note that mapping[l] may +// be equal to l. +// +// The postsolver will be updated so it can recover a solution of the mapped +// problem. Note that this works on any problem the SatSolver can handle, not +// only pure SAT problem, but the returned mapping do need to be applied to all +// constraints. +void ProbeAndFindEquivalentLiteral( + SatSolver* solver, SatPostsolver* postsolver, + ITIVector* mapping); + } // namespace sat } // namespace operations_research