From 4ade94b96025a43237389498905efdec61527574 Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Mon, 24 Jul 2023 07:09:47 -0700 Subject: [PATCH] [CP-SAT] remove unused pure sat code; cleanup sat_runner --- ortools/sat/optimization.cc | 963 --------------------------- ortools/sat/optimization.h | 78 +-- ortools/sat/python/cp_model_test.py | 2 +- ortools/sat/sat_runner.cc | 347 +--------- ortools/sat/timetable_edgefinding.cc | 2 +- 5 files changed, 28 insertions(+), 1364 deletions(-) diff --git a/ortools/sat/optimization.cc b/ortools/sat/optimization.cc index 09e1f9216ca..95b5dcbb271 100644 --- a/ortools/sat/optimization.cc +++ b/ortools/sat/optimization.cc @@ -59,170 +59,6 @@ namespace operations_research { namespace sat { -namespace { - -// Used to log messages to stdout or to the normal logging framework according -// to the given LogBehavior value. -class Logger { - public: - explicit Logger(LogBehavior v) : use_stdout_(v == STDOUT_LOG) {} - void Log(const std::string& message) { - if (use_stdout_) { - absl::PrintF("%s\n", message); - } else { - LOG(INFO) << message; - } - } - - private: - bool use_stdout_; -}; - -// Outputs the current objective value in the cnf output format. -// Note that this function scale the given objective. -std::string CnfObjectiveLine(const LinearBooleanProblem& problem, - Coefficient objective) { - const double scaled_objective = - AddOffsetAndScaleObjectiveValue(problem, objective); - return absl::StrFormat("o %d", static_cast(scaled_objective)); -} - -struct LiteralWithCoreIndex { - LiteralWithCoreIndex(Literal l, int i) : literal(l), core_index(i) {} - Literal literal; - int core_index; -}; - -// Deletes the given indices from a vector. The given indices must be sorted in -// increasing order. The order of the non-deleted entries in the vector is -// preserved. -template -void DeleteVectorIndices(const std::vector& indices, Vector* v) { - int new_size = 0; - int indices_index = 0; - for (int i = 0; i < v->size(); ++i) { - if (indices_index < indices.size() && i == indices[indices_index]) { - ++indices_index; - } else { - (*v)[new_size] = (*v)[i]; - ++new_size; - } - } - v->resize(new_size); -} - -// In the Fu & Malik algorithm (or in WPM1), when two cores overlap, we -// artificially introduce symmetries. More precisely: -// -// The picture below shows two cores with index 0 and 1, with one blocking -// variable per '-' and with the variables ordered from left to right (by their -// assumptions index). The blocking variables will be the one added to "relax" -// the core for the next iteration. -// -// 1: ------------------------------- -// 0: ------------------------------------ -// -// The 2 following assignment of the blocking variables are equivalent. -// Remember that exactly one blocking variable per core must be assigned to 1. -// -// 1: ----------------------1-------- -// 0: --------1--------------------------- -// -// and -// -// 1: ---------------------------1--- -// 0: ---1-------------------------------- -// -// This class allows to add binary constraints excluding the second possibility. -// Basically, each time a new core is added, if two of its blocking variables -// (b1, b2) have the same assumption index of two blocking variables from -// another core (c1, c2), then we forbid the assignment c1 true and b2 true. -// -// Reference: C Ansótegui, ML Bonet, J Levy, "Sat-based maxsat algorithms", -// Artificial Intelligence, 2013 - Elsevier. -class FuMalikSymmetryBreaker { - public: - FuMalikSymmetryBreaker() = default; - - // Must be called before a new core is processed. - void StartResolvingNewCore(int new_core_index) { - literal_by_core_.resize(new_core_index); - for (int i = 0; i < new_core_index; ++i) { - literal_by_core_[i].clear(); - } - } - - // This should be called for each blocking literal b of the new core. The - // assumption_index identify the soft clause associated to the given blocking - // literal. Note that between two StartResolvingNewCore() calls, - // ProcessLiteral() is assumed to be called with different assumption_index. - // - // Changing the order of the calls will not change the correctness, but will - // change the symmetry-breaking clause produced. - // - // Returns a set of literals which can't be true at the same time as b (under - // symmetry breaking). - std::vector ProcessLiteral(int assumption_index, Literal b) { - if (assumption_index >= info_by_assumption_index_.size()) { - info_by_assumption_index_.resize(assumption_index + 1); - } - - // Compute the function result. - // info_by_assumption_index_[assumption_index] will contain all the pairs - // (blocking_literal, core) of the previous resolved cores at the same - // assumption index as b. - std::vector result; - for (LiteralWithCoreIndex data : - info_by_assumption_index_[assumption_index]) { - // literal_by_core_ will contain all the blocking literal of a given core - // with an assumption_index that was used in one of the ProcessLiteral() - // calls since the last StartResolvingNewCore(). - // - // Note that there can be only one such literal by core, so we will not - // add duplicates. - result.insert(result.end(), literal_by_core_[data.core_index].begin(), - literal_by_core_[data.core_index].end()); - } - - // Update the internal data structure. - for (LiteralWithCoreIndex data : - info_by_assumption_index_[assumption_index]) { - literal_by_core_[data.core_index].push_back(data.literal); - } - info_by_assumption_index_[assumption_index].push_back( - LiteralWithCoreIndex(b, literal_by_core_.size())); - return result; - } - - // Deletes the given assumption indices. - void DeleteIndices(const std::vector& indices) { - DeleteVectorIndices(indices, &info_by_assumption_index_); - } - - // This is only used in WPM1 to forget all the information related to a given - // assumption_index. - void ClearInfo(int assumption_index) { - CHECK_LE(assumption_index, info_by_assumption_index_.size()); - info_by_assumption_index_[assumption_index].clear(); - } - - // This is only used in WPM1 when a new assumption_index is created. - void AddInfo(int assumption_index, Literal b) { - CHECK_GE(assumption_index, info_by_assumption_index_.size()); - info_by_assumption_index_.resize(assumption_index + 1); - info_by_assumption_index_[assumption_index].push_back( - LiteralWithCoreIndex(b, literal_by_core_.size())); - } - - private: - std::vector> info_by_assumption_index_; - std::vector> literal_by_core_; - - DISALLOW_COPY_AND_ASSIGN(FuMalikSymmetryBreaker); -}; - -} // namespace - void MinimizeCoreWithPropagation(TimeLimit* limit, SatSolver* solver, std::vector* core) { if (solver->ModelIsUnsat()) return; @@ -295,805 +131,6 @@ void FilterAssignedLiteral(const VariablesAssignment& assignment, core->resize(new_size); } -// This algorithm works by exploiting the unsat core returned by the SAT solver -// when the problem is UNSAT. It starts by trying to solve the decision problem -// where all the objective variables are set to their value with minimal cost, -// and relax in each step some of these fixed variables until the problem -// becomes satisfiable. -SatSolver::Status SolveWithFuMalik(LogBehavior log, - const LinearBooleanProblem& problem, - SatSolver* solver, - std::vector* solution) { - Logger logger(log); - FuMalikSymmetryBreaker symmetry; - - // blocking_clauses will contains a set of clauses that are currently added to - // the initial problem. - // - // Initially, each clause just contains a literal associated to an objective - // variable with non-zero cost. Setting all these literals to true will lead - // to the lowest possible objective. - // - // During the algorithm, "blocking" literals will be added to each clause. - // Moreover each clause will contain an extra "assumption" literal stored in - // the separate assumptions vector (in its negated form). - // - // The meaning of a given clause will always be: - // If the assumption literal and all blocking literals are false, then the - // "objective" literal (which is the first one in the clause) must be true. - // When the "objective" literal is true, its variable (which have a non-zero - // cost) is set to the value that minimize the objective cost. - // - // ex: If a variable "x" as a cost of 3, its cost contribution is smaller when - // it is set to false (since it will contribute to zero instead of 3). - std::vector> blocking_clauses; - std::vector assumptions; - - // Initialize blocking_clauses and assumptions. - const LinearObjective& objective = problem.objective(); - CHECK_GT(objective.coefficients_size(), 0); - const Coefficient unique_objective_coeff(std::abs(objective.coefficients(0))); - for (int i = 0; i < objective.literals_size(); ++i) { - CHECK_EQ(std::abs(objective.coefficients(i)), unique_objective_coeff) - << "The basic Fu & Malik algorithm needs constant objective coeffs."; - const Literal literal(objective.literals(i)); - - // We want to minimize the cost when this literal is true. - const Literal min_literal = - objective.coefficients(i) > 0 ? literal.Negated() : literal; - blocking_clauses.push_back(std::vector(1, min_literal)); - - // Note that initialy, we do not create any extra variables. - assumptions.push_back(min_literal); - } - - // Print the number of variable with a non-zero cost. - logger.Log(absl::StrFormat("c #weights:%u #vars:%d #constraints:%d", - assumptions.size(), problem.num_variables(), - problem.constraints_size())); - - // Starts the algorithm. Each loop will solve the problem under the given - // assumptions, and if unsat, will relax exactly one of the objective - // variables (from the unsat core) to be in its "costly" state. When the - // algorithm terminates, the number of iterations is exactly the minimal - // objective value. - for (int iter = 0;; ++iter) { - const SatSolver::Status result = - solver->ResetAndSolveWithGivenAssumptions(assumptions); - if (result == SatSolver::FEASIBLE) { - ExtractAssignment(problem, *solver, solution); - Coefficient objective = ComputeObjectiveValue(problem, *solution); - logger.Log(CnfObjectiveLine(problem, objective)); - return SatSolver::FEASIBLE; - } - if (result != SatSolver::ASSUMPTIONS_UNSAT) return result; - - // The interesting case: we have an unsat core. - // - // We need to add new "blocking" variables b_i for all the objective - // variable appearing in the core. Moreover, we will only relax as little - // as possible (to not miss the optimal), so we will enforce that the sum - // of the b_i is exactly one. - std::vector core = solver->GetLastIncompatibleDecisions(); - MinimizeCore(solver, &core); - solver->Backtrack(0); - - // Print the search progress. - logger.Log(absl::StrFormat("c iter:%d core:%u", iter, core.size())); - - // Special case for a singleton core. - if (core.size() == 1) { - // Find the index of the "objective" variable that need to be fixed in - // its "costly" state. - const int index = - std::find(assumptions.begin(), assumptions.end(), core[0]) - - assumptions.begin(); - CHECK_LT(index, assumptions.size()); - - // Fix it. We also fix all the associated blocking variables if any. - if (!solver->AddUnitClause(core[0].Negated())) { - return SatSolver::INFEASIBLE; - } - for (Literal b : blocking_clauses[index]) { - if (!solver->AddUnitClause(b.Negated())) return SatSolver::INFEASIBLE; - } - - // Erase this entry from the current "objective" - std::vector to_delete(1, index); - DeleteVectorIndices(to_delete, &assumptions); - DeleteVectorIndices(to_delete, &blocking_clauses); - symmetry.DeleteIndices(to_delete); - } else { - symmetry.StartResolvingNewCore(iter); - - // We will add 2 * |core.size()| variables. - const int old_num_variables = solver->NumVariables(); - if (core.size() == 2) { - // Special case. If core.size() == 2, we can use only one blocking - // variable (the other one beeing its negation). This actually do happen - // quite often in practice, so it is worth it. - solver->SetNumVariables(old_num_variables + 3); - } else { - solver->SetNumVariables(old_num_variables + 2 * core.size()); - } - - // Temporary vectors for the constraint (sum new blocking variable == 1). - std::vector at_most_one_constraint; - std::vector at_least_one_constraint; - - // This will be set to false if the problem becomes unsat while adding a - // new clause. This is unlikely, but may be possible. - bool ok = true; - - // Loop over the core. - int index = 0; - for (int i = 0; i < core.size(); ++i) { - // Since the assumptions appear in order in the core, we can find the - // relevant "objective" variable efficiently with a simple linear scan - // in the assumptions vector (done with index). - index = - std::find(assumptions.begin() + index, assumptions.end(), core[i]) - - assumptions.begin(); - CHECK_LT(index, assumptions.size()); - - // The new blocking and assumption variables for this core entry. - const Literal a(BooleanVariable(old_num_variables + i), true); - Literal b(BooleanVariable(old_num_variables + core.size() + i), true); - if (core.size() == 2) { - b = Literal(BooleanVariable(old_num_variables + 2), true); - if (i == 1) b = b.Negated(); - } - - // Symmetry breaking clauses. - for (Literal l : symmetry.ProcessLiteral(index, b)) { - ok &= solver->AddBinaryClause(l.Negated(), b.Negated()); - } - - // Note(user): There is more than one way to encode the algorithm in - // SAT. Here we "delete" the old blocking clause and add a new one. In - // the WPM1 algorithm below, the blocking clause is decomposed into - // 3-SAT and we don't need to delete anything. - - // First, fix the old "assumption" variable to false, which has the - // effect of deleting the old clause from the solver. - if (assumptions[index].Variable() >= problem.num_variables()) { - CHECK(solver->AddUnitClause(assumptions[index].Negated())); - } - - // Add the new blocking variable. - blocking_clauses[index].push_back(b); - - // Add the new clause to the solver. Temporary including the - // assumption, but removing it right afterwards. - blocking_clauses[index].push_back(a); - ok &= solver->AddProblemClause(blocking_clauses[index]); - blocking_clauses[index].pop_back(); - - // For the "== 1" constraint on the blocking literals. - at_most_one_constraint.push_back(LiteralWithCoeff(b, 1.0)); - at_least_one_constraint.push_back(b); - - // The new assumption variable replace the old one. - assumptions[index] = a.Negated(); - } - - // Add the "<= 1" side of the "== 1" constraint. - ok &= solver->AddLinearConstraint(false, Coefficient(0), true, - Coefficient(1.0), - &at_most_one_constraint); - - // TODO(user): The algorithm does not really need the >= 1 side of this - // constraint. Initial investigation shows that it doesn't really help, - // but investigate more. - if (/* DISABLES CODE */ (false)) { - ok &= solver->AddProblemClause(at_least_one_constraint); - } - - if (!ok) { - LOG(INFO) << "Infeasible while adding a clause."; - return SatSolver::INFEASIBLE; - } - } - } -} - -SatSolver::Status SolveWithWPM1(LogBehavior log, - const LinearBooleanProblem& problem, - SatSolver* solver, - std::vector* solution) { - Logger logger(log); - FuMalikSymmetryBreaker symmetry; - - // The current lower_bound on the cost. - // It will be correct after the initialization. - Coefficient lower_bound(static_cast(problem.objective().offset())); - Coefficient upper_bound(std::numeric_limits::max()); - - // The assumption literals and their associated cost. - std::vector assumptions; - std::vector costs; - std::vector reference; - - // Initialization. - const LinearObjective& objective = problem.objective(); - CHECK_GT(objective.coefficients_size(), 0); - for (int i = 0; i < objective.literals_size(); ++i) { - const Literal literal(objective.literals(i)); - const Coefficient coeff(objective.coefficients(i)); - - // We want to minimize the cost when the assumption is true. - // Note that initially, we do not create any extra variables. - if (coeff > 0) { - assumptions.push_back(literal.Negated()); - costs.push_back(coeff); - } else { - assumptions.push_back(literal); - costs.push_back(-coeff); - lower_bound += coeff; - } - } - reference = assumptions; - - // This is used by the "stratified" approach. - Coefficient stratified_lower_bound = - *std::max_element(costs.begin(), costs.end()); - - // Print the number of variables with a non-zero cost. - logger.Log(absl::StrFormat("c #weights:%u #vars:%d #constraints:%d", - assumptions.size(), problem.num_variables(), - problem.constraints_size())); - - for (int iter = 0;; ++iter) { - // This is called "hardening" in the literature. - // Basically, we know that there is only hardening_threshold weight left - // to distribute, so any assumption with a greater cost than this can never - // be false. We fix it instead of treating it as an assumption. - solver->Backtrack(0); - const Coefficient hardening_threshold = upper_bound - lower_bound; - CHECK_GE(hardening_threshold, 0); - std::vector to_delete; - int num_above_threshold = 0; - for (int i = 0; i < assumptions.size(); ++i) { - if (costs[i] > hardening_threshold) { - if (!solver->AddUnitClause(assumptions[i])) { - return SatSolver::INFEASIBLE; - } - to_delete.push_back(i); - ++num_above_threshold; - } else { - // This impact the stratification heuristic. - if (solver->Assignment().LiteralIsTrue(assumptions[i])) { - to_delete.push_back(i); - } - } - } - if (!to_delete.empty()) { - logger.Log(absl::StrFormat("c fixed %u assumptions, %d with cost > %d", - to_delete.size(), num_above_threshold, - hardening_threshold.value())); - DeleteVectorIndices(to_delete, &assumptions); - DeleteVectorIndices(to_delete, &costs); - DeleteVectorIndices(to_delete, &reference); - symmetry.DeleteIndices(to_delete); - } - - // This is the "stratification" part. - // Extract the assumptions with a cost >= stratified_lower_bound. - std::vector assumptions_subset; - for (int i = 0; i < assumptions.size(); ++i) { - if (costs[i] >= stratified_lower_bound) { - assumptions_subset.push_back(assumptions[i]); - } - } - - const SatSolver::Status result = - solver->ResetAndSolveWithGivenAssumptions(assumptions_subset); - if (result == SatSolver::FEASIBLE) { - // If not all assumptions were taken, continue with a lower stratified - // bound. Otherwise we have an optimal solution! - // - // TODO(user): Try more advanced variant where the bound is lowered by - // more than this minimal amount. - const Coefficient old_lower_bound = stratified_lower_bound; - for (Coefficient cost : costs) { - if (cost < old_lower_bound) { - if (stratified_lower_bound == old_lower_bound || - cost > stratified_lower_bound) { - stratified_lower_bound = cost; - } - } - } - - ExtractAssignment(problem, *solver, solution); - DCHECK(IsAssignmentValid(problem, *solution)); - const Coefficient objective_offset( - static_cast(problem.objective().offset())); - const Coefficient objective = ComputeObjectiveValue(problem, *solution); - if (objective + objective_offset < upper_bound) { - logger.Log(CnfObjectiveLine(problem, objective)); - upper_bound = objective + objective_offset; - } - - if (stratified_lower_bound < old_lower_bound) continue; - return SatSolver::FEASIBLE; - } - if (result != SatSolver::ASSUMPTIONS_UNSAT) return result; - - // The interesting case: we have an unsat core. - // - // We need to add new "blocking" variables b_i for all the objective - // variables appearing in the core. Moreover, we will only relax as little - // as possible (to not miss the optimal), so we will enforce that the sum - // of the b_i is exactly one. - std::vector core = solver->GetLastIncompatibleDecisions(); - MinimizeCore(solver, &core); - solver->Backtrack(0); - - // Compute the min cost of all the assertions in the core. - // The lower bound will be updated by that much. - Coefficient min_cost = kCoefficientMax; - { - int index = 0; - for (int i = 0; i < core.size(); ++i) { - index = - std::find(assumptions.begin() + index, assumptions.end(), core[i]) - - assumptions.begin(); - CHECK_LT(index, assumptions.size()); - min_cost = std::min(min_cost, costs[index]); - } - } - lower_bound += min_cost; - - // Print the search progress. - logger.Log(absl::StrFormat( - "c iter:%d core:%u lb:%d min_cost:%d strat:%d", iter, core.size(), - lower_bound.value(), min_cost.value(), stratified_lower_bound.value())); - - // This simple line helps a lot on the packup-wpms instances! - // - // TODO(user): That was because of a bug before in the way - // stratified_lower_bound was decremented, not sure it helps that much now. - if (min_cost > stratified_lower_bound) { - stratified_lower_bound = min_cost; - } - - // Special case for a singleton core. - if (core.size() == 1) { - // Find the index of the "objective" variable that need to be fixed in - // its "costly" state. - const int index = - std::find(assumptions.begin(), assumptions.end(), core[0]) - - assumptions.begin(); - CHECK_LT(index, assumptions.size()); - - // Fix it. - if (!solver->AddUnitClause(core[0].Negated())) { - return SatSolver::INFEASIBLE; - } - - // Erase this entry from the current "objective". - std::vector to_delete(1, index); - DeleteVectorIndices(to_delete, &assumptions); - DeleteVectorIndices(to_delete, &costs); - DeleteVectorIndices(to_delete, &reference); - symmetry.DeleteIndices(to_delete); - } else { - symmetry.StartResolvingNewCore(iter); - - // We will add 2 * |core.size()| variables. - const int old_num_variables = solver->NumVariables(); - if (core.size() == 2) { - // Special case. If core.size() == 2, we can use only one blocking - // variable (the other one beeing its negation). This actually do happen - // quite often in practice, so it is worth it. - solver->SetNumVariables(old_num_variables + 3); - } else { - solver->SetNumVariables(old_num_variables + 2 * core.size()); - } - - // Temporary vectors for the constraint (sum new blocking variable == 1). - std::vector at_most_one_constraint; - std::vector at_least_one_constraint; - - // This will be set to false if the problem becomes unsat while adding a - // new clause. This is unlikely, but may be possible. - bool ok = true; - - // Loop over the core. - int index = 0; - for (int i = 0; i < core.size(); ++i) { - // Since the assumptions appear in order in the core, we can find the - // relevant "objective" variable efficiently with a simple linear scan - // in the assumptions vector (done with index). - index = - std::find(assumptions.begin() + index, assumptions.end(), core[i]) - - assumptions.begin(); - CHECK_LT(index, assumptions.size()); - - // The new blocking and assumption variables for this core entry. - const Literal a(BooleanVariable(old_num_variables + i), true); - Literal b(BooleanVariable(old_num_variables + core.size() + i), true); - if (core.size() == 2) { - b = Literal(BooleanVariable(old_num_variables + 2), true); - if (i == 1) b = b.Negated(); - } - - // a false & b false => previous assumptions (which was false). - const Literal old_a = assumptions[index]; - ok &= solver->AddTernaryClause(a, b, old_a); - - // Optional. Also add the two implications a => x and b => x where x is - // the negation of the previous assumption variable. - ok &= solver->AddBinaryClause(a.Negated(), old_a.Negated()); - ok &= solver->AddBinaryClause(b.Negated(), old_a.Negated()); - - // Optional. Also add the implication a => not(b). - ok &= solver->AddBinaryClause(a.Negated(), b.Negated()); - - // This is the difference with the Fu & Malik algorithm. - // If the soft clause protected by old_a has a cost greater than - // min_cost then: - // - its cost is disminished by min_cost. - // - an identical clause with cost min_cost is artificially added to - // the problem. - CHECK_GE(costs[index], min_cost); - if (costs[index] == min_cost) { - // The new assumption variable replaces the old one. - assumptions[index] = a.Negated(); - - // Symmetry breaking clauses. - for (Literal l : symmetry.ProcessLiteral(index, b)) { - ok &= solver->AddBinaryClause(l.Negated(), b.Negated()); - } - } else { - // Since the cost of the given index changes, we need to start a new - // "equivalence" class for the symmetry breaking algo and clear the - // old one. - symmetry.AddInfo(assumptions.size(), b); - symmetry.ClearInfo(index); - - // Reduce the cost of the old assumption. - costs[index] -= min_cost; - - // We add the new assumption with a cost of min_cost. - // - // Note(user): I think it is nice that these are added after old_a - // because assuming old_a will implies all the derived assumptions to - // true, and thus they will never appear in a core until old_a is not - // an assumption anymore. - assumptions.push_back(a.Negated()); - costs.push_back(min_cost); - reference.push_back(reference[index]); - } - - // For the "<= 1" constraint on the blocking literals. - // Note(user): we don't add the ">= 1" side because it is not needed for - // the correctness and it doesn't seems to help. - at_most_one_constraint.push_back(LiteralWithCoeff(b, 1.0)); - - // Because we have a core, we know that at least one of the initial - // problem variables must be true. This seems to help a bit. - // - // TODO(user): Experiment more. - at_least_one_constraint.push_back(reference[index].Negated()); - } - - // Add the "<= 1" side of the "== 1" constraint. - ok &= solver->AddLinearConstraint(false, Coefficient(0), true, - Coefficient(1.0), - &at_most_one_constraint); - - // Optional. Add the ">= 1" constraint on the initial problem variables. - ok &= solver->AddProblemClause(at_least_one_constraint); - - if (!ok) { - LOG(INFO) << "Unsat while adding a clause."; - return SatSolver::INFEASIBLE; - } - } - } -} - -SatSolver::Status SolveWithRandomParameters( - LogBehavior log, const LinearBooleanProblem& problem, int num_times, - absl::BitGenRef random, SatSolver* solver, std::vector* solution) { - Logger logger(log); - const SatParameters initial_parameters = solver->parameters(); - - SatParameters parameters = initial_parameters; - TimeLimit time_limit(parameters.max_time_in_seconds()); - - // We start with a low conflict limit and increase it until we are able to - // solve the problem at least once. After this, the limit stays the same. - int max_number_of_conflicts = 5; - parameters.set_log_search_progress(false); - - Coefficient min_seen(std::numeric_limits::max()); - Coefficient max_seen(std::numeric_limits::min()); - Coefficient best(min_seen); - for (int i = 0; i < num_times; ++i) { - solver->Backtrack(0); - RandomizeDecisionHeuristic(random, ¶meters); - - parameters.set_max_number_of_conflicts(max_number_of_conflicts); - parameters.set_max_time_in_seconds(time_limit.GetTimeLeft()); - parameters.set_random_seed(i); - solver->SetParameters(parameters); - solver->ResetDecisionHeuristic(); - - const bool use_obj = absl::Bernoulli(random, 1.0 / 4); - if (use_obj) UseObjectiveForSatAssignmentPreference(problem, solver); - - const SatSolver::Status result = solver->Solve(); - if (result == SatSolver::INFEASIBLE) { - // If the problem is INFEASIBLE after we over-constrained the objective, - // then we found an optimal solution, otherwise, even the decision problem - // is INFEASIBLE. - if (best == kCoefficientMax) return SatSolver::INFEASIBLE; - return SatSolver::FEASIBLE; - } - if (result == SatSolver::LIMIT_REACHED) { - // We augment the number of conflict until we have one feasible solution. - if (best == kCoefficientMax) ++max_number_of_conflicts; - if (time_limit.LimitReached()) return SatSolver::LIMIT_REACHED; - continue; - } - - CHECK_EQ(result, SatSolver::FEASIBLE); - std::vector candidate; - ExtractAssignment(problem, *solver, &candidate); - CHECK(IsAssignmentValid(problem, candidate)); - const Coefficient objective = ComputeObjectiveValue(problem, candidate); - if (objective < best) { - *solution = candidate; - best = objective; - logger.Log(CnfObjectiveLine(problem, objective)); - - // Overconstrain the objective. - solver->Backtrack(0); - if (!AddObjectiveConstraint(problem, false, Coefficient(0), true, - objective - 1, solver)) { - return SatSolver::FEASIBLE; - } - } - min_seen = std::min(min_seen, objective); - max_seen = std::max(max_seen, objective); - - logger.Log(absl::StrCat( - "c ", objective.value(), " [", min_seen.value(), ", ", max_seen.value(), - "] objective_preference: ", use_obj ? "true" : "false", " ", - ProtobufShortDebugString(parameters))); - } - - // Restore the initial parameter (with an updated time limit). - parameters = initial_parameters; - parameters.set_max_time_in_seconds(time_limit.GetTimeLeft()); - solver->SetParameters(parameters); - return SatSolver::LIMIT_REACHED; -} - -SatSolver::Status SolveWithLinearScan(LogBehavior log, - const LinearBooleanProblem& problem, - SatSolver* solver, - std::vector* solution) { - Logger logger(log); - - // This has a big positive impact on most problems. - UseObjectiveForSatAssignmentPreference(problem, solver); - - Coefficient objective = kCoefficientMax; - if (!solution->empty()) { - CHECK(IsAssignmentValid(problem, *solution)); - objective = ComputeObjectiveValue(problem, *solution); - } - while (true) { - if (objective != kCoefficientMax) { - // Over constrain the objective. - solver->Backtrack(0); - if (!AddObjectiveConstraint(problem, false, Coefficient(0), true, - objective - 1, solver)) { - return SatSolver::FEASIBLE; - } - } - - // Solve the problem. - const SatSolver::Status result = solver->Solve(); - CHECK_NE(result, SatSolver::ASSUMPTIONS_UNSAT); - if (result == SatSolver::INFEASIBLE) { - if (objective == kCoefficientMax) return SatSolver::INFEASIBLE; - return SatSolver::FEASIBLE; - } - if (result == SatSolver::LIMIT_REACHED) { - return SatSolver::LIMIT_REACHED; - } - - // Extract the new best solution. - CHECK_EQ(result, SatSolver::FEASIBLE); - ExtractAssignment(problem, *solver, solution); - CHECK(IsAssignmentValid(problem, *solution)); - const Coefficient old_objective = objective; - objective = ComputeObjectiveValue(problem, *solution); - CHECK_LT(objective, old_objective); - logger.Log(CnfObjectiveLine(problem, objective)); - } -} - -SatSolver::Status SolveWithCardinalityEncoding( - LogBehavior log, const LinearBooleanProblem& problem, SatSolver* solver, - std::vector* solution) { - Logger logger(log); - std::deque repository; - - // Create one initial node per variables with cost. - Coefficient offset(0); - std::vector nodes = - CreateInitialEncodingNodes(problem.objective(), &offset, &repository); - - // This algorithm only work with weights of the same magnitude. - CHECK(!nodes.empty()); - const Coefficient reference = nodes.front()->weight(); - for (const EncodingNode* n : nodes) CHECK_EQ(n->weight(), reference); - - // Initialize the current objective. - Coefficient objective = kCoefficientMax; - Coefficient upper_bound = kCoefficientMax; - if (!solution->empty()) { - CHECK(IsAssignmentValid(problem, *solution)); - objective = ComputeObjectiveValue(problem, *solution); - upper_bound = objective + offset; - } - - // Print the number of variables with a non-zero cost. - logger.Log(absl::StrFormat("c #weights:%u #vars:%d #constraints:%d", - nodes.size(), problem.num_variables(), - problem.constraints_size())); - - // Create the sorter network. - solver->Backtrack(0); - EncodingNode* root = - MergeAllNodesWithDeque(upper_bound, nodes, solver, &repository); - logger.Log(absl::StrFormat("c encoding depth:%d", root->depth())); - - while (true) { - if (objective != kCoefficientMax) { - // Over constrain the objective by fixing the variable index - 1 of the - // root node to 0. - const int index = offset.value() + objective.value(); - if (index == 0) return SatSolver::FEASIBLE; - solver->Backtrack(0); - if (!solver->AddUnitClause(root->literal(index - 1).Negated())) { - return SatSolver::FEASIBLE; - } - } - - // Solve the problem. - const SatSolver::Status result = solver->Solve(); - CHECK_NE(result, SatSolver::ASSUMPTIONS_UNSAT); - if (result == SatSolver::INFEASIBLE) { - if (objective == kCoefficientMax) return SatSolver::INFEASIBLE; - return SatSolver::FEASIBLE; - } - if (result == SatSolver::LIMIT_REACHED) return SatSolver::LIMIT_REACHED; - - // Extract the new best solution. - CHECK_EQ(result, SatSolver::FEASIBLE); - ExtractAssignment(problem, *solver, solution); - CHECK(IsAssignmentValid(problem, *solution)); - const Coefficient old_objective = objective; - objective = ComputeObjectiveValue(problem, *solution); - CHECK_LT(objective, old_objective); - logger.Log(CnfObjectiveLine(problem, objective)); - } -} - -SatSolver::Status SolveWithCardinalityEncodingAndCore( - LogBehavior log, const LinearBooleanProblem& problem, SatSolver* solver, - std::vector* solution) { - Logger logger(log); - SatParameters parameters = solver->parameters(); - - // Create one initial nodes per variables with cost. - Coefficient offset(0); - std::deque repository; - std::vector nodes = - CreateInitialEncodingNodes(problem.objective(), &offset, &repository); - - // Initialize the bounds. - // This is in term of number of variables not at their minimal value. - Coefficient lower_bound(0); - Coefficient upper_bound(std::numeric_limits::max()); - if (!solution->empty()) { - CHECK(IsAssignmentValid(problem, *solution)); - upper_bound = ComputeObjectiveValue(problem, *solution) + offset; - } - - // Print the number of variables with a non-zero cost. - logger.Log(absl::StrFormat("c #weights:%u #vars:%d #constraints:%d", - nodes.size(), problem.num_variables(), - problem.constraints_size())); - - // This is used by the "stratified" approach. - Coefficient stratified_lower_bound(0); - if (parameters.max_sat_stratification() == - SatParameters::STRATIFICATION_DESCENT) { - // In this case, we initialize it to the maximum assumption weights. - for (EncodingNode* n : nodes) { - stratified_lower_bound = std::max(stratified_lower_bound, n->weight()); - } - } - - // Start the algorithm. - int max_depth = 0; - std::string previous_core_info = ""; - for (int iter = 0;; ++iter) { - // TODO(user): We are suboptimal here because we use for upper bound the - // current best objective, not best_obj - 1. This code is not really used - // but we should still fix it. - ReduceNodes(upper_bound, &lower_bound, &nodes, solver); - - const std::vector assumptions = - ExtractAssumptions(stratified_lower_bound, nodes, solver); - if (assumptions.empty()) return SatSolver::FEASIBLE; - - // Display the progress. - const std::string gap_string = - (upper_bound == kCoefficientMax) - ? "" - : absl::StrFormat(" gap:%d", (upper_bound - lower_bound).value()); - logger.Log( - absl::StrFormat("c iter:%d [%s] lb:%d%s assumptions:%u depth:%d", iter, - previous_core_info, - lower_bound.value() - offset.value() + - static_cast(problem.objective().offset()), - gap_string, nodes.size(), max_depth)); - - // Solve under the assumptions. - const SatSolver::Status result = - solver->ResetAndSolveWithGivenAssumptions(assumptions); - if (result == SatSolver::FEASIBLE) { - // Extract the new solution and save it if it is the best found so far. - std::vector temp_solution; - ExtractAssignment(problem, *solver, &temp_solution); - CHECK(IsAssignmentValid(problem, temp_solution)); - const Coefficient obj = ComputeObjectiveValue(problem, temp_solution); - if (obj + offset < upper_bound) { - *solution = temp_solution; - logger.Log(CnfObjectiveLine(problem, obj)); - upper_bound = obj + offset; - } - - // If not all assumptions were taken, continue with a lower stratified - // bound. Otherwise we have an optimal solution. - stratified_lower_bound = - MaxNodeWeightSmallerThan(nodes, stratified_lower_bound); - if (stratified_lower_bound > 0) continue; - return SatSolver::FEASIBLE; - } - if (result != SatSolver::ASSUMPTIONS_UNSAT) return result; - - // We have a new core. - std::vector core = solver->GetLastIncompatibleDecisions(); - if (parameters.minimize_core()) MinimizeCore(solver, &core); - - // Compute the min weight of all the nodes in the core. - // The lower bound will be increased by that much. - const Coefficient min_weight = ComputeCoreMinWeight(nodes, core); - previous_core_info = - absl::StrFormat("size:%u mw:%d", core.size(), min_weight.value()); - - // Increase stratified_lower_bound according to the parameters. - if (stratified_lower_bound < min_weight && - parameters.max_sat_stratification() == - SatParameters::STRATIFICATION_ASCENT) { - stratified_lower_bound = min_weight; - } - - ProcessCore(core, min_weight, /*gap=*/upper_bound - lower_bound, - &repository, &nodes, solver, &previous_core_info, nullptr); - max_depth = std::max(max_depth, nodes.back()->depth()); - } -} - SatSolver::Status MinimizeIntegerVariableWithLinearScanAndLazyEncoding( IntegerVariable objective_var, const std::function& feasible_solution_observer, Model* model) { diff --git a/ortools/sat/optimization.h b/ortools/sat/optimization.h index a0c638f91d3..acd31aacbd9 100644 --- a/ortools/sat/optimization.h +++ b/ortools/sat/optimization.h @@ -17,14 +17,11 @@ #include #include -#include "absl/random/bit_gen_ref.h" -#include "ortools/sat/boolean_problem.pb.h" #include "ortools/sat/clause.h" #include "ortools/sat/cp_model_mapping.h" #include "ortools/sat/integer.h" #include "ortools/sat/integer_search.h" #include "ortools/sat/model.h" -#include "ortools/sat/pb_constraint.h" #include "ortools/sat/sat_base.h" #include "ortools/sat/sat_parameters.pb.h" #include "ortools/sat/sat_solver.h" @@ -45,83 +42,10 @@ namespace sat { void MinimizeCoreWithPropagation(TimeLimit* limit, SatSolver* solver, std::vector* core); +// Remove fixed literals from the core. void FilterAssignedLiteral(const VariablesAssignment& assignment, std::vector* core); -// Because the Solve*() functions below are also used in scripts that requires a -// special output format, we use this to tell them whether or not to use the -// default logging framework or simply stdout. Most users should just use -// DEFAULT_LOG. -enum LogBehavior { DEFAULT_LOG, STDOUT_LOG }; - -// All the Solve*() functions below reuse the SatSolver::Status with a slightly -// different meaning: -// - FEASIBLE: The problem has been solved to optimality. -// - INFEASIBLE: Same meaning, the decision version is already unsat. -// - LIMIT_REACHED: we may have some feasible solution (if solution is -// non-empty), but the optimality is not proven. - -// Implements the "Fu & Malik" algorithm described in: -// Zhaohui Fu, Sharad Malik, "On solving the Partial MAX-SAT problem", 2006, -// International Conference on Theory and Applications of Satisfiability -// Testing. (SAT’06), LNCS 4121. -// -// This algorithm requires all the objective weights to be the same (CHECKed) -// and currently only works on minimization problems. The problem is assumed to -// be already loaded into the given solver. -// -// TODO(user): double-check the correctness if the objective coefficients are -// negative. -SatSolver::Status SolveWithFuMalik(LogBehavior log, - const LinearBooleanProblem& problem, - SatSolver* solver, - std::vector* solution); - -// The WPM1 algorithm is a generalization of the Fu & Malik algorithm to -// weighted problems. Note that if all objective weights are the same, this is -// almost the same as SolveWithFuMalik() but the encoding of the constraints is -// slightly different. -// -// Ansotegui, C., Bonet, M.L., Levy, J.: Solving (weighted) partial MaxSAT -// through satisfiability testing. In: Proc. of the 12th Int. Conf. on Theory and -// Applications of Satisfiability Testing (SAT’09). pp. 427-440 (2009) -SatSolver::Status SolveWithWPM1(LogBehavior log, - const LinearBooleanProblem& problem, - SatSolver* solver, std::vector* solution); - -// Solves num_times the decision version of the given problem with different -// random parameters. Keep the best solution (regarding the objective) and -// returns it in solution. The problem is assumed to be already loaded into the -// given solver. -SatSolver::Status SolveWithRandomParameters( - LogBehavior log, const LinearBooleanProblem& problem, int num_times, - absl::BitGenRef random, SatSolver* solver, std::vector* solution); - -// Starts by solving the decision version of the given LinearBooleanProblem and -// then simply add a constraint to find a lower objective that the current best -// solution and repeat until the problem becomes unsat. -// -// The problem is assumed to be already loaded into the given solver. If -// solution is initially a feasible solution, the search will starts from there. -// solution will be updated with the best solution found so far. -SatSolver::Status SolveWithLinearScan(LogBehavior log, - const LinearBooleanProblem& problem, - SatSolver* solver, - std::vector* solution); - -// Similar algorithm as the one used by qmaxsat, this is a linear scan with the -// at-most k constraint encoded in SAT. This only works on problems with -// constant weights. -SatSolver::Status SolveWithCardinalityEncoding( - LogBehavior log, const LinearBooleanProblem& problem, SatSolver* solver, - std::vector* solution); - -// This is an original algorithm. It is a mix between the cardinality encoding -// and the Fu & Malik algorithm. It also works on general weighted instances. -SatSolver::Status SolveWithCardinalityEncodingAndCore( - LogBehavior log, const LinearBooleanProblem& problem, SatSolver* solver, - std::vector* solution); - // Model-based API to minimize a given IntegerVariable by solving a sequence of // decision problem. Each problem is solved using SolveIntegerProblem(). Returns // the status of the last solved decision problem. diff --git a/ortools/sat/python/cp_model_test.py b/ortools/sat/python/cp_model_test.py index 825cbababba..934fd370fe1 100644 --- a/ortools/sat/python/cp_model_test.py +++ b/ortools/sat/python/cp_model_test.py @@ -1400,7 +1400,7 @@ def testCustomLog(self): self.assertEqual(10, solver.Value(x)) self.assertEqual(-5, solver.Value(y)) - self.assertRegex(log_callback.Log(), "Parameters.*log_to_stdout.*") + self.assertRegex(log_callback.Log(), ".*log_to_stdout.*") def testIssue2762(self): print("testIssue2762") diff --git a/ortools/sat/sat_runner.cc b/ortools/sat/sat_runner.cc index 97fcc4c24c9..58b15ccde54 100644 --- a/ortools/sat/sat_runner.cc +++ b/ortools/sat/sat_runner.cc @@ -65,74 +65,16 @@ ABSL_FLAG( std::string, input, "", "Required: input file of the problem to solve. Many format are supported:" ".cnf (sat, max-sat, weighted max-sat), .opb (pseudo-boolean sat/optim) " - "and by default the LinearBooleanProblem proto (binary or text)."); + "and by default the CpModelProto proto (binary or text)."); -ABSL_FLAG( - std::string, output, "", - "If non-empty, write the input problem as a LinearBooleanProblem proto to " - "this file. By default it uses the binary format except if the file " - "extension is '.txt'. If the problem is SAT, a satisfiable assignment is " - "also written to the file."); - -ABSL_FLAG(bool, output_cnf_solution, false, - "If true and the problem was solved to optimality, this output " - "the solution to stdout in cnf form.\n"); +ABSL_FLAG(std::string, output, "", + "If non-empty, write the response there. By default it uses the " + "binary format except if the file extension is '.txt'."); ABSL_FLAG(std::string, params, "", "Parameters for the sat solver in a text format of the " "SatParameters proto, example: --params=use_conflicts:true."); -ABSL_FLAG(bool, strict_validity, false, - "If true, stop if the given input is invalid (duplicate literals, " - "out of range, zero cofficients, etc.)"); - -ABSL_FLAG( - std::string, lower_bound, "", - "If not empty, look for a solution with an objective value >= this bound."); - -ABSL_FLAG( - std::string, upper_bound, "", - "If not empty, look for a solution with an objective value <= this bound."); - -ABSL_FLAG(bool, fu_malik, false, - "If true, search the optimal solution with the Fu & Malik algo."); - -ABSL_FLAG(bool, wpm1, false, - "If true, search the optimal solution with the WPM1 algo."); - -ABSL_FLAG(bool, qmaxsat, false, - "If true, search the optimal solution with a linear scan and " - " the cardinality encoding used in qmaxsat."); - -ABSL_FLAG(bool, core_enc, false, - "If true, search the optimal solution with the core-based " - "cardinality encoding algo."); - -ABSL_FLAG(bool, linear_scan, false, - "If true, search the optimal solution with the linear scan algo."); - -ABSL_FLAG(int, randomize, 500, - "If positive, solve that many times the problem with a random " - "decision heuristic before trying to optimize it."); - -ABSL_FLAG(bool, use_symmetry, false, - "If true, find and exploit the eventual symmetries " - "of the problem."); - -ABSL_FLAG(bool, presolve, true, - "Only work on pure SAT problem. If true, presolve the problem."); - -ABSL_FLAG(bool, probing, false, "If true, presolve the problem using probing."); - -ABSL_FLAG(bool, use_cp_model, true, - "Whether to interpret everything as a CpModelProto or " - "to read by default a CpModelProto."); - -ABSL_FLAG(bool, reduce_memory_usage, false, - "If true, do not keep a copy of the original problem in memory." - "This reduce the memory usage, but disable the solution cheking at " - "the end."); - ABSL_FLAG(bool, wcnf_use_strong_slack, true, "If true, when we add a slack variable to reify a soft clause, we " "enforce the fact that when it is true, the clause must be false."); @@ -141,25 +83,15 @@ namespace operations_research { namespace sat { namespace { -// Returns a trivial best bound. The best bound corresponds to the lower bound -// (resp. upper bound) in case of a minimization (resp. maximization) problem. -double GetScaledTrivialBestBound(const LinearBooleanProblem& problem) { - Coefficient best_bound(0); - const LinearObjective& objective = problem.objective(); - for (const int64_t value : objective.coefficients()) { - if (value < 0) best_bound += Coefficient(value); - } - return AddOffsetAndScaleObjectiveValue(problem, best_bound); -} - -bool LoadBooleanProblem(const std::string& filename, - LinearBooleanProblem* problem, CpModelProto* cp_model) { +bool LoadBooleanProblem(const std::string& filename, CpModelProto* cp_model) { if (absl::EndsWith(filename, ".opb") || absl::EndsWith(filename, ".opb.bz2")) { OpbReader reader; - if (!reader.Load(filename, problem)) { + LinearBooleanProblem problem; + if (!reader.Load(filename, &problem)) { LOG(FATAL) << "Cannot load file '" << filename << "'."; } + *cp_model = BooleanProblemToCpModelproto(problem); } else if (absl::EndsWith(filename, ".cnf") || absl::EndsWith(filename, ".cnf.xz") || absl::EndsWith(filename, ".cnf.gz") || @@ -167,44 +99,16 @@ bool LoadBooleanProblem(const std::string& filename, absl::EndsWith(filename, ".wcnf.xz") || absl::EndsWith(filename, ".wcnf.gz")) { SatCnfReader reader(absl::GetFlag(FLAGS_wcnf_use_strong_slack)); - if (absl::GetFlag(FLAGS_fu_malik) || absl::GetFlag(FLAGS_linear_scan) || - absl::GetFlag(FLAGS_wpm1) || absl::GetFlag(FLAGS_qmaxsat) || - absl::GetFlag(FLAGS_core_enc)) { - reader.InterpretCnfAsMaxSat(true); - } - if (absl::GetFlag(FLAGS_use_cp_model)) { - if (!reader.Load(filename, cp_model)) { - LOG(FATAL) << "Cannot load file '" << filename << "'."; - } - } else { - if (!reader.Load(filename, problem)) { - LOG(FATAL) << "Cannot load file '" << filename << "'."; - } + if (!reader.Load(filename, cp_model)) { + LOG(FATAL) << "Cannot load file '" << filename << "'."; } - } else if (absl::GetFlag(FLAGS_use_cp_model)) { + } else { LOG(INFO) << "Reading a CpModelProto."; *cp_model = ReadFileToProtoOrDie(filename); - } else { - LOG(INFO) << "Reading a LinearBooleanProblem."; - *problem = ReadFileToProtoOrDie(filename); } return true; } -std::string SolutionString(const LinearBooleanProblem& problem, - const std::vector& assignment) { - std::string output; - BooleanVariable limit(problem.original_num_variables()); - for (BooleanVariable index(0); index < limit; ++index) { - if (index > 0) output += " "; - absl::StrAppend(&output, - Literal(index, assignment[index.value()]).SignedValue()); - } - return output; -} - -// To benefit from the operations_research namespace, we put all the main() code -// here. int Run() { SatParameters parameters; if (absl::GetFlag(FLAGS_input).empty()) { @@ -219,236 +123,35 @@ int Run() { << absl::GetFlag(FLAGS_params); } - // Initialize the solver. - std::unique_ptr solver(new SatSolver()); - solver->SetParameters(parameters); - // Read the problem. google::protobuf::Arena arena; CpModelProto* cp_model = google::protobuf::Arena::CreateMessage(&arena); - LinearBooleanProblem problem; - if (!LoadBooleanProblem(absl::GetFlag(FLAGS_input), &problem, cp_model)) { + if (!LoadBooleanProblem(absl::GetFlag(FLAGS_input), cp_model)) { CpSolverResponse response; response.set_status(CpSolverStatus::MODEL_INVALID); return EXIT_SUCCESS; } - if (!absl::GetFlag(FLAGS_use_cp_model)) { - LOG(INFO) << "Converting to CpModelProto ..."; - *cp_model = BooleanProblemToCpModelproto(problem); - } - - // TODO(user): clean this hack. Ideally LinearBooleanProblem should be - // completely replaced by the more general CpModelProto. - if (absl::GetFlag(FLAGS_use_cp_model)) { - problem.Clear(); // We no longer need it, release memory. - Model model; - model.Add(NewSatParameters(parameters)); - const CpSolverResponse response = SolveCpModel(*cp_model, &model); - if (!absl::GetFlag(FLAGS_output).empty()) { - if (absl::EndsWith(absl::GetFlag(FLAGS_output), "txt")) { - CHECK_OK(file::SetTextProto(absl::GetFlag(FLAGS_output), response, - file::Defaults())); - } else { - CHECK_OK(file::SetBinaryProto(absl::GetFlag(FLAGS_output), response, - file::Defaults())); - } - } + Model model; + model.Add(NewSatParameters(parameters)); + const CpSolverResponse response = SolveCpModel(*cp_model, &model); - // The SAT competition requires a particular exit code and since we don't - // really use it for any other purpose, we comply. - if (response.status() == CpSolverStatus::OPTIMAL) return 10; - if (response.status() == CpSolverStatus::FEASIBLE) return 10; - if (response.status() == CpSolverStatus::INFEASIBLE) return 20; - return EXIT_SUCCESS; - } - - if (absl::GetFlag(FLAGS_strict_validity)) { - const absl::Status status = ValidateBooleanProblem(problem); - if (!status.ok()) { - LOG(ERROR) << "Invalid Boolean problem: " << status.message(); - return EXIT_FAILURE; - } - } - - // Count the time from there. - WallTimer wall_timer; - UserTimer user_timer; - wall_timer.Start(); - user_timer.Start(); - double scaled_best_bound = GetScaledTrivialBestBound(problem); - - // Probing. - SatPostsolver probing_postsolver(problem.num_variables()); - LinearBooleanProblem original_problem; - if (absl::GetFlag(FLAGS_probing)) { - // TODO(user): This is nice for testing, but consumes memory. - original_problem = problem; - ProbeAndSimplifyProblem(&probing_postsolver, &problem); - } - - // Load the problem into the solver. - if (absl::GetFlag(FLAGS_reduce_memory_usage)) { - if (!LoadAndConsumeBooleanProblem(&problem, solver.get())) { - LOG(INFO) << "UNSAT when loading the problem."; - } - } else { - if (!LoadBooleanProblem(problem, solver.get())) { - LOG(INFO) << "UNSAT when loading the problem."; - } - } - auto strtoint64 = [](const std::string& word) { - int64_t value = 0; - if (!word.empty()) CHECK(absl::SimpleAtoi(word, &value)); - return value; - }; - if (!AddObjectiveConstraint( - problem, !absl::GetFlag(FLAGS_lower_bound).empty(), - Coefficient(strtoint64(absl::GetFlag(FLAGS_lower_bound))), - !absl::GetFlag(FLAGS_upper_bound).empty(), - Coefficient(strtoint64(absl::GetFlag(FLAGS_upper_bound))), - solver.get())) { - LOG(INFO) << "UNSAT when setting the objective constraint."; - } - - // Symmetries! - // - // TODO(user): To make this compatible with presolve, we just need to run - // it after the presolve step. - if (absl::GetFlag(FLAGS_use_symmetry)) { - CHECK(!absl::GetFlag(FLAGS_reduce_memory_usage)) << "incompatible"; - CHECK(!absl::GetFlag(FLAGS_presolve)) << "incompatible"; - LOG(INFO) << "Finding symmetries of the problem."; - std::vector> generators; - FindLinearBooleanProblemSymmetries(problem, &generators); - std::unique_ptr propagator(new SymmetryPropagator); - for (int i = 0; i < generators.size(); ++i) { - propagator->AddSymmetry(std::move(generators[i])); - } - solver->AddPropagator(propagator.get()); - solver->TakePropagatorOwnership(std::move(propagator)); - } - - // Optimize? - std::vector solution; - SatSolver::Status result = SatSolver::LIMIT_REACHED; - if (absl::GetFlag(FLAGS_fu_malik) || absl::GetFlag(FLAGS_linear_scan) || - absl::GetFlag(FLAGS_wpm1) || absl::GetFlag(FLAGS_qmaxsat) || - absl::GetFlag(FLAGS_core_enc)) { - if (absl::GetFlag(FLAGS_randomize) > 0 && - (absl::GetFlag(FLAGS_linear_scan) || absl::GetFlag(FLAGS_qmaxsat))) { - CHECK(!absl::GetFlag(FLAGS_reduce_memory_usage)) << "incompatible"; - absl::BitGen bitgen; - result = SolveWithRandomParameters(STDOUT_LOG, problem, - absl::GetFlag(FLAGS_randomize), bitgen, - solver.get(), &solution); - } - if (result == SatSolver::LIMIT_REACHED) { - if (absl::GetFlag(FLAGS_qmaxsat)) { - solver = std::make_unique(); - solver->SetParameters(parameters); - CHECK(LoadBooleanProblem(problem, solver.get())); - result = SolveWithCardinalityEncoding(STDOUT_LOG, problem, solver.get(), - &solution); - } else if (absl::GetFlag(FLAGS_core_enc)) { - result = SolveWithCardinalityEncodingAndCore(STDOUT_LOG, problem, - solver.get(), &solution); - } else if (absl::GetFlag(FLAGS_fu_malik)) { - result = SolveWithFuMalik(STDOUT_LOG, problem, solver.get(), &solution); - } else if (absl::GetFlag(FLAGS_wpm1)) { - result = SolveWithWPM1(STDOUT_LOG, problem, solver.get(), &solution); - } else if (absl::GetFlag(FLAGS_linear_scan)) { - result = - SolveWithLinearScan(STDOUT_LOG, problem, solver.get(), &solution); - } - } - } else { - // Only solve the decision version. - parameters.set_log_search_progress(true); - solver->SetParameters(parameters); - if (absl::GetFlag(FLAGS_presolve)) { - std::unique_ptr time_limit = - TimeLimit::FromParameters(parameters); - SolverLogger logger; - result = SolveWithPresolve(&solver, time_limit.get(), &solution, - /*drat_proof_handler=*/nullptr, &logger); - if (result == SatSolver::FEASIBLE) { - CHECK(IsAssignmentValid(problem, solution)); - } + if (!absl::GetFlag(FLAGS_output).empty()) { + if (absl::EndsWith(absl::GetFlag(FLAGS_output), "txt")) { + CHECK_OK(file::SetTextProto(absl::GetFlag(FLAGS_output), response, + file::Defaults())); } else { - result = solver->Solve(); - if (result == SatSolver::FEASIBLE) { - ExtractAssignment(problem, *solver, &solution); - CHECK(IsAssignmentValid(problem, solution)); - } - } - } - - // Print the solution status. - if (result == SatSolver::FEASIBLE) { - if (absl::GetFlag(FLAGS_fu_malik) || absl::GetFlag(FLAGS_linear_scan) || - absl::GetFlag(FLAGS_wpm1) || absl::GetFlag(FLAGS_core_enc)) { - absl::PrintF("s OPTIMUM FOUND\n"); - CHECK(!solution.empty()); - const Coefficient objective = ComputeObjectiveValue(problem, solution); - scaled_best_bound = AddOffsetAndScaleObjectiveValue(problem, objective); - - // Postsolve. - if (absl::GetFlag(FLAGS_probing)) { - solution = probing_postsolver.PostsolveSolution(solution); - problem = original_problem; - } - } else { - absl::PrintF("s SATISFIABLE\n"); - } - - // Check and output the solution. - CHECK(IsAssignmentValid(problem, solution)); - if (absl::GetFlag(FLAGS_output_cnf_solution)) { - absl::PrintF("v %s\n", SolutionString(problem, solution)); - } - if (!absl::GetFlag(FLAGS_output).empty()) { - CHECK(!absl::GetFlag(FLAGS_reduce_memory_usage)) << "incompatible"; - if (result == SatSolver::FEASIBLE) { - StoreAssignment(solver->Assignment(), problem.mutable_assignment()); - } - if (absl::EndsWith(absl::GetFlag(FLAGS_output), ".txt")) { - CHECK_OK(file::SetTextProto(absl::GetFlag(FLAGS_output), problem, + CHECK_OK(file::SetBinaryProto(absl::GetFlag(FLAGS_output), response, file::Defaults())); - } else { - CHECK_OK(file::SetBinaryProto(absl::GetFlag(FLAGS_output), problem, - file::Defaults())); - } } } - if (result == SatSolver::INFEASIBLE) { - absl::PrintF("s UNSATISFIABLE\n"); - } - - // Print status. - absl::PrintF("c status: %s\n", SatStatusString(result)); - - // Print objective value. - if (solution.empty()) { - absl::PrintF("c objective: na\n"); - absl::PrintF("c best bound: na\n"); - } else { - const Coefficient objective = ComputeObjectiveValue(problem, solution); - absl::PrintF("c objective: %.16g\n", - AddOffsetAndScaleObjectiveValue(problem, objective)); - absl::PrintF("c best bound: %.16g\n", scaled_best_bound); - } - - // Print final statistics. - absl::PrintF("c booleans: %d\n", solver->NumVariables()); - absl::PrintF("c conflicts: %d\n", solver->num_failures()); - absl::PrintF("c branches: %d\n", solver->num_branches()); - absl::PrintF("c propagations: %d\n", solver->num_propagations()); - absl::PrintF("c walltime: %f\n", wall_timer.Get()); - absl::PrintF("c usertime: %f\n", user_timer.Get()); - absl::PrintF("c deterministic_time: %f\n", solver->deterministic_time()); + // The SAT competition requires a particular exit code and since we don't + // really use it for any other purpose, we comply. + if (response.status() == CpSolverStatus::OPTIMAL) return 10; + if (response.status() == CpSolverStatus::FEASIBLE) return 10; + if (response.status() == CpSolverStatus::INFEASIBLE) return 20; return EXIT_SUCCESS; } diff --git a/ortools/sat/timetable_edgefinding.cc b/ortools/sat/timetable_edgefinding.cc index ae1cc935819..2bb8397ace9 100644 --- a/ortools/sat/timetable_edgefinding.cc +++ b/ortools/sat/timetable_edgefinding.cc @@ -96,7 +96,7 @@ void TimeTableEdgeFinding::BuildTimeTable() { IntegerValue height = IntegerValue(0); IntegerValue energy = IntegerValue(0); - // We don't care since at the beginning heigh is zero, and previous_time will + // We don't care since at the beginning height is zero, and previous_time will // be correct after the first iteration. IntegerValue previous_time = IntegerValue(0);