From aee340b07cde2b3e83cba175a095d27a62a7d75c Mon Sep 17 00:00:00 2001 From: "lperron@google.com" Date: Wed, 21 May 2014 12:56:57 +0000 Subject: [PATCH] update examples --- examples/cpp/dobble_ls.cc | 2 +- examples/cpp/jobshop.h | 5 +- examples/cpp/ls_api.cc | 2 +- examples/cpp/multidim_knapsack.cc | 5 +- examples/cpp/opb_reader.h | 5 +- examples/cpp/pdptw.cc | 10 +- examples/cpp/print_dimacs_assignment.h | 30 +---- examples/cpp/sat_cnf_reader.h | 95 +++++++++------ examples/cpp/sat_runner.cc | 153 ++++++++++++++++++++----- 9 files changed, 205 insertions(+), 102 deletions(-) diff --git a/examples/cpp/dobble_ls.cc b/examples/cpp/dobble_ls.cc index 6ec5ee4566..1bbdf8e638 100644 --- a/examples/cpp/dobble_ls.cc +++ b/examples/cpp/dobble_ls.cc @@ -444,7 +444,7 @@ class DobbleFilter : public IntVarLocalSearchFilter { // We build the current bitmap and the matrix of violation cost // between any two cards. - virtual void OnSynchronize() { + virtual void OnSynchronize(const Assignment* delta) { symbol_bitmask_per_card_.assign(num_cards_, 0); for (int card = 0; card < num_cards_; ++card) { for (int symbol = 0; symbol < num_symbols_; ++symbol) { diff --git a/examples/cpp/jobshop.h b/examples/cpp/jobshop.h index a45670b16d..759437b111 100644 --- a/examples/cpp/jobshop.h +++ b/examples/cpp/jobshop.h @@ -121,9 +121,8 @@ class JobShopData { private: void ProcessNewLine(char* const line) { // TODO(user): more robust logic to support single-task jobs. - static const char kWordDelimiters[] = " "; - std::vector words; - SplitStringUsing(line, kWordDelimiters, &words); + const std::vector words = + strings::Split(line, " ", strings::SkipEmpty()); switch (problem_type_) { case UNDEFINED: { if (words.size() == 2 && words[0] == "instance") { diff --git a/examples/cpp/ls_api.cc b/examples/cpp/ls_api.cc index 6708a54e18..c5a0fd44cf 100644 --- a/examples/cpp/ls_api.cc +++ b/examples/cpp/ls_api.cc @@ -89,7 +89,7 @@ class SumFilter : public IntVarLocalSearchFilter { ~SumFilter() {} - virtual void OnSynchronize() { + virtual void OnSynchronize(const Assignment* delta) { sum_ = 0; for (int index = 0; index < Size(); ++index) { sum_ += Value(index); diff --git a/examples/cpp/multidim_knapsack.cc b/examples/cpp/multidim_knapsack.cc index ef38fc90c6..29320b6a30 100644 --- a/examples/cpp/multidim_knapsack.cc +++ b/examples/cpp/multidim_knapsack.cc @@ -90,9 +90,8 @@ class MultiDimKnapsackData { // Used internally. void ProcessNewLine(char* const line) { - const char* const kWordDelimiters(" "); - std::vector words; - SplitStringUsing(line, kWordDelimiters, &words); + const std::vector words = + strings::Split(line, " ", strings::SkipEmpty()); line_read_++; if (problem_type_ == -1) { if (words.size() == 1) { diff --git a/examples/cpp/opb_reader.h b/examples/cpp/opb_reader.h index 5fb21bd525..34c540cee4 100644 --- a/examples/cpp/opb_reader.h +++ b/examples/cpp/opb_reader.h @@ -64,9 +64,8 @@ class OpbReader { } void ProcessNewLine(LinearBooleanProblem* problem, const std::string& line) { - static const char kWordDelimiters[] = " "; - std::vector words; - SplitStringUsing(line, kWordDelimiters, &words); + const std::vector words = + strings::Split(line, " ", strings::SkipEmpty()); if (words.size() == 0 || words[0].empty() || words[0][0] == '*') { return; } diff --git a/examples/cpp/pdptw.cc b/examples/cpp/pdptw.cc index 853750aa57..edaa7ff44d 100644 --- a/examples/cpp/pdptw.cc +++ b/examples/cpp/pdptw.cc @@ -169,17 +169,15 @@ bool LoadAndSolve(const std::string& pdp_file) { // Load all the lines of the file in RAM (it shouldn't be too large anyway). std::vector lines; { - const int64 kMaxInputFileSize = 1 << 30; // 1GB - File* data_file = File::OpenOrDie(pdp_file, "r"); std::string contents; - data_file->ReadToString(&contents, kMaxInputFileSize); - data_file->Close(); - if (contents.size() == kMaxInputFileSize) { + CHECK(file::GetContents(pdp_file, &contents, file::Defaults()).ok()); + const int64 kMaxInputFileSize = 1 << 30; // 1GB + if (contents.size() >= kMaxInputFileSize) { LOG(WARNING) << "Input file '" << pdp_file << "' is too large (>" << kMaxInputFileSize << " bytes)."; return false; } - SplitStringUsing(contents, "\n", &lines); + lines = strings::Split(contents, "\n", strings::SkipEmpty()); } // Reading header. if (lines.empty()) { diff --git a/examples/cpp/print_dimacs_assignment.h b/examples/cpp/print_dimacs_assignment.h index ab79eddbca..91763bfd70 100644 --- a/examples/cpp/print_dimacs_assignment.h +++ b/examples/cpp/print_dimacs_assignment.h @@ -22,8 +22,10 @@ #include "base/logging.h" #include "base/stringprintf.h" +#include "base/file.h" #include "graph/ebert_graph.h" #include "graph/linear_assignment.h" +#include "base/status.h" namespace operations_research { @@ -40,41 +42,22 @@ void PrintDimacsAssignmentProblem( const TailArrayManager& tail_array_manager, const std::string& output_filename); -// Implementation is below here. -namespace internal { - -void WriteOrDie(const char* buffer, - size_t item_size, - size_t buffer_length, - FILE* fp) { - size_t written = fwrite(buffer, item_size, buffer_length, fp); - if (written != buffer_length) { - fprintf(stderr, "Write failed.\n"); - exit(1); - } -} - -} // namespace internal - - template void PrintDimacsAssignmentProblem( const LinearSumAssignment& assignment, const TailArrayManager& tail_array_manager, const std::string& output_filename) { - FILE* output = fopen(output_filename.c_str(), "w"); + File* output = File::Open(output_filename, "w"); const GraphType& graph(assignment.Graph()); std::string output_line = StringPrintf("p asn %d %d\n", graph.num_nodes(), graph.num_arcs()); - internal::WriteOrDie(output_line.c_str(), 1, - output_line.length(), output); + CHECK(file::WriteString(output, output_line, file::Defaults()).ok()); for (typename LinearSumAssignment::BipartiteLeftNodeIterator node_it(assignment); node_it.Ok(); node_it.Next()) { output_line = StringPrintf("n %d\n", node_it.Index() + 1); - internal::WriteOrDie(output_line.c_str(), 1, - output_line.length(), output); + CHECK(file::WriteString(output, output_line, file::Defaults()).ok()); } tail_array_manager.BuildTailArrayFromAdjacencyListsIfForwardGraph(); @@ -84,8 +67,7 @@ void PrintDimacsAssignmentProblem( ArcIndex arc = arc_it.Index(); output_line = StringPrintf("a %d %d %lld\n", graph.Tail(arc) + 1, graph.Head(arc) + 1, assignment.ArcCost(arc)); - internal::WriteOrDie(output_line.c_str(), 1, - output_line.length(), output); + CHECK(file::WriteString(output, output_line, file::Defaults()).ok()); } } diff --git a/examples/cpp/sat_cnf_reader.h b/examples/cpp/sat_cnf_reader.h index d27fc0d9f2..9893cdb929 100644 --- a/examples/cpp/sat_cnf_reader.h +++ b/examples/cpp/sat_cnf_reader.h @@ -13,9 +13,11 @@ #ifndef OR_TOOLS_SAT_SAT_CNF_READER_H_ #define OR_TOOLS_SAT_SAT_CNF_READER_H_ +#include #include #include +#include "base/commandlineflags.h" #include "base/integral_types.h" #include "base/logging.h" #include "base/strtoint.h" @@ -23,6 +25,11 @@ #include "sat/boolean_problem.pb.h" #include "util/filelineiter.h" +DEFINE_bool( + max_sat, false, + "A cnf file can be both interpreted as a pure SAT or a max-SAT problem. " + "If this flag is true, we interpret it as the max-sat version."); + namespace operations_research { namespace sat { @@ -41,7 +48,10 @@ class SatCnfReader { problem->set_name(ExtractProblemName(filename)); is_wcnf_ = false; end_marker_seen_ = false; - slack_variable_weights_.clear(); + hard_weight_ = 0; + num_skipped_soft_clauses_ = 0; + num_singleton_soft_clauses_ = 0; + num_slack_variables_ = 0; int num_lines = 0; for (const std::string& line : FileLines(filename)) { @@ -52,21 +62,11 @@ class SatCnfReader { LOG(FATAL) << "File '" << filename << "' is empty or can't be read."; } problem->set_original_num_variables(num_variables_); - problem->set_num_variables(num_variables_ + slack_variable_weights_.size()); + problem->set_num_variables(num_variables_ + num_slack_variables_); - // Add the slack variables (to convert max-sat to an pseudo-Boolean - // optimization problem). - if (is_wcnf_) { - LinearObjective* objective = problem->mutable_objective(); - int slack_literal = num_variables_ + 1; - for (const int weight : slack_variable_weights_) { - objective->add_literals(slack_literal); - objective->add_coefficients(weight); - ++slack_literal; - } - } - - if (problem->constraints_size() != num_clauses_) { + if (num_clauses_ != + problem->constraints_size() + num_singleton_soft_clauses_ + + num_skipped_soft_clauses_) { LOG(ERROR) << "Wrong number of clauses."; return false; } @@ -110,7 +110,9 @@ class SatCnfReader { hard_weight_ = (words_.size() > 4) ? StringPieceAtoi(words_[4]) : 0; problem->set_type(LinearBooleanProblem::MINIMIZATION); } else { - problem->set_type(LinearBooleanProblem::SATISFIABILITY); + problem->set_type(FLAGS_max_sat + ? LinearBooleanProblem::MINIMIZATION + : LinearBooleanProblem::SATISFIABILITY); } } else { LOG(FATAL) << "Unknow file type: " << words_[1]; @@ -119,37 +121,63 @@ class SatCnfReader { // In the cnf file format, the last words should always be 0. DCHECK_EQ("0", words_.back()); const int size = words_.size() - 1; + const int reserved_size = (!is_wcnf_ && FLAGS_max_sat) ? size + 1 : size; LinearBooleanConstraint* constraint = problem->add_constraints(); - constraint->mutable_literals()->Reserve(size); - constraint->mutable_coefficients()->Reserve(size); + constraint->mutable_literals()->Reserve(reserved_size); + constraint->mutable_coefficients()->Reserve(reserved_size); constraint->set_lower_bound(1); + int64 weight = (!is_wcnf_ && FLAGS_max_sat) ? 1 : hard_weight_; for (int i = 0; i < size; ++i) { const int64 signed_value = StringPieceAtoi(words_[i]); if (i == 0 && is_wcnf_) { // Mathematically, a soft clause of weight 0 can be removed. if (signed_value == 0) { + ++num_skipped_soft_clauses_; problem->mutable_constraints()->RemoveLast(); break; } - if (signed_value != hard_weight_) { - const int slack_literal = - num_variables_ + slack_variable_weights_.size() + 1; - constraint->add_literals(slack_literal); - constraint->add_coefficients(1); - slack_variable_weights_.push_back(signed_value); - } - continue; + weight = signed_value; + } else { + DCHECK_NE(signed_value, 0); + constraint->add_literals(signed_value); + constraint->add_coefficients(1); } - DCHECK_NE(signed_value, 0); - constraint->add_literals(signed_value); - constraint->add_coefficients(1); } - if (DEBUG_MODE && !is_wcnf_) { + if (weight != hard_weight_) { + if (constraint->literals_size() == 1) { + // The max-sat formulation of an optimization sat problem with a + // linear objective introduces many singleton soft clauses. Because we + // natively work with a linear objective, we can just put the cost on + // the unique variable of such clause and remove the clause. + // + // TODO(user): If many singleton clauses with the same variable + // appear, we will create duplicate entry in the objective which is + // not supported (and is checked by BooleanProblemIsValid()). If we do + // encounter this case in practice, fix this. + ++num_singleton_soft_clauses_; + LinearObjective* objective = problem->mutable_objective(); + objective->add_literals(-constraint->literals(0)); + objective->add_coefficients(weight); + problem->mutable_constraints()->RemoveLast(); + } else { + // The +1 is because a positive literal is the same as the 1-based + // variable index. + const int slack_literal = num_variables_ + num_slack_variables_ + 1; + ++num_slack_variables_; + constraint->add_literals(slack_literal); + constraint->add_coefficients(1); + + LinearObjective* objective = problem->mutable_objective(); + objective->add_literals(slack_literal); + objective->add_coefficients(weight); + DCHECK_EQ(constraint->literals_size(), reserved_size); + } + } else { // If wcnf is true, we currently reserve one more literals than needed // for the hard clauses. - DCHECK_EQ(constraint->literals_size(), size); + DCHECK_EQ(constraint->literals_size(), is_wcnf_ ? size - 1 : size); } } } @@ -164,9 +192,12 @@ class SatCnfReader { bool is_wcnf_; // Some files have text after %. This indicates if we have seen the '%'. bool end_marker_seen_; - std::vector slack_variable_weights_; int64 hard_weight_; + int num_slack_variables_; + int num_skipped_soft_clauses_; + int num_singleton_soft_clauses_; + DISALLOW_COPY_AND_ASSIGN(SatCnfReader); }; diff --git a/examples/cpp/sat_runner.cc b/examples/cpp/sat_runner.cc index 0d8ce61418..7d017c760d 100644 --- a/examples/cpp/sat_runner.cc +++ b/examples/cpp/sat_runner.cc @@ -26,6 +26,7 @@ // TODO(user): Move sat_cnf_reader.h and sat_runner.cc to examples? #include "cpp/opb_reader.h" #include "cpp/sat_cnf_reader.h" +#include "base/random.h" #include "sat/boolean_problem.h" #include "sat/sat_solver.h" #include "util/time_limit.h" @@ -65,6 +66,10 @@ DEFINE_bool(search_optimal, false, "If true, search for the optimal solution. " "The algorithm is currently really basic."); +DEFINE_int32(randomize, 100, + "If positive, solve that many times the problem with a random " + "decision heuristic before trying to optimize it."); + DEFINE_bool(use_symmetry, false, "If true, find and exploit the eventual symmetries " "of the problem."); @@ -85,6 +90,30 @@ double GetScaledObjective(const LinearBooleanProblem& problem, problem.objective().offset(); } +void RandomizeDecisionHeuristic(MTRandom* random, SatParameters* parameters) { + // Random preferred variable order. + const google::protobuf::EnumDescriptor* order_d = + SatParameters::VariableOrder_descriptor(); + parameters->set_preferred_variable_order( + static_cast( + order_d->value(random->Uniform(order_d->value_count()))->number())); + + // Random polarity initial value. + const google::protobuf::EnumDescriptor* polarity_d = + SatParameters::Polarity_descriptor(); + parameters->set_initial_polarity(static_cast( + polarity_d->value(random->Uniform(polarity_d->value_count()))->number())); + + // Other random parameters. + parameters->set_use_phase_saving(random->OneIn(2)); + const std::vector ratios = {0.0, 0.0, 0.0, 0.01, 1.0}; + parameters->set_random_polarity_ratio(ratios[random->Uniform(ratios.size())]); + + // IMPORTANT: SetParameters() will reinitialize the seed, so we must change + // it. + parameters->set_random_seed(parameters->random_seed() + 1); +} + void LoadBooleanProblem(std::string filename, LinearBooleanProblem* problem) { if (HasSuffixString(filename, ".opb") || HasSuffixString(filename, ".opb.bz2")) { @@ -119,6 +148,56 @@ void PrintObjective(double objective) { printf("o %lld\n", static_cast(objective)); } +int64 SolveWithDifferentParameters(const LinearBooleanProblem& problem, + SatSolver* solver, TimeLimit* time_limit, + int num_solve) { + MTRandom random("A random seed."); + SatParameters parameters = solver->parameters(); + + // We start with a low limit (increased on each LIMIT_REACHED). + parameters.set_log_search_progress(false); + parameters.set_max_number_of_conflicts(10); + + int64 min_seen = std::numeric_limits::max(); + int64 max_seen = std::numeric_limits::min(); + int64 best = min_seen; + for (int i = 0; i < num_solve; ++i) { + solver->Backtrack(0); + RandomizeDecisionHeuristic(&random, ¶meters); + parameters.set_max_time_in_seconds(time_limit->GetTimeLeft()); + solver->SetParameters(parameters); + solver->ResetDecisionHeuristic(); + + const bool use_obj = random.OneIn(4); + if (use_obj) UseObjectiveForSatAssignmentPreference(problem, solver); + + const SatSolver::Status result = solver->Solve(); + if (result == SatSolver::LIMIT_REACHED) { + printf("limit reached\n"); + parameters.set_max_number_of_conflicts( + static_cast(1.1 * parameters.max_number_of_conflicts())); + if (time_limit->LimitReached()) return best; + continue; + } + + CHECK_EQ(result, SatSolver::MODEL_SAT); + CHECK(IsAssignmentValid(problem, solver->Assignment())); + + const Coefficient objective = + ComputeObjectiveValue(problem, solver->Assignment()); + best = std::min(best, objective.value()); + const int64 scaled_objective = + static_cast(GetScaledObjective(problem, objective)); + min_seen = std::min(min_seen, scaled_objective); + max_seen = std::max(max_seen, scaled_objective); + + printf("objective preference: %s\n", use_obj ? "true" : "false"); + printf("%s", parameters.DebugString().c_str()); + printf(" %lld [%lld, %lld]\n", scaled_objective, min_seen, max_seen); + } + return best; +} + // Same as Run() with --solve_optimal, no logging, and an output in the cnf // format. int RunWithCnfOutputFormat(std::string filename) { @@ -225,41 +304,57 @@ int Run() { TimeLimit time_limit(parameters.max_time_in_seconds()); Coefficient objective = kCoefficientMax; int old_num_fixed_variables = 0; + bool first_time = true; while (true) { - const SatSolver::Status result = solver.Solve(); - if (result == SatSolver::MODEL_UNSAT) { - if (objective == kCoefficientMax) { - LOG(INFO) << "The problem is UNSAT"; + if (first_time && FLAGS_randomize > 0) { + first_time = false; + solver.SetParameters(parameters); + objective = SolveWithDifferentParameters(problem, &solver, &time_limit, + FLAGS_randomize); + solver.SetParameters(parameters); + solver.Backtrack(0); + solver.ResetDecisionHeuristic(); + UseObjectiveForSatAssignmentPreference(problem, &solver); + } else { + const SatSolver::Status result = solver.Solve(); + if (result == SatSolver::MODEL_UNSAT) { + if (objective == kCoefficientMax) { + LOG(INFO) << "The problem is UNSAT"; + break; + } + LOG(INFO) << "Optimal found!"; + LOG(INFO) << "Objective = " << GetScaledObjective(problem, objective); + LOG(INFO) << "Time = " << time_limit.GetElapsedTime(); break; } - LOG(INFO) << "Optimal found!"; - LOG(INFO) << "Objective = " << GetScaledObjective(problem, objective); - LOG(INFO) << "Time = " << time_limit.GetElapsedTime(); - break; - } - if (result != SatSolver::MODEL_SAT) { - LOG(INFO) << "Search aborted."; - if (objective == kCoefficientMax) { - LOG(INFO) << "No solution found!"; - LOG(INFO) << "Objective = " << kCoefficientMax; - } else { - LOG(INFO) << "Objective = " << GetScaledObjective(problem, objective); + if (result != SatSolver::MODEL_SAT) { + LOG(INFO) << "Search aborted."; + if (objective == kCoefficientMax) { + LOG(INFO) << "No solution found!"; + LOG(INFO) << "Objective = " << kCoefficientMax; + } else { + LOG(INFO) << "Objective = " << GetScaledObjective(problem, + objective); + } + LOG(INFO) << "Time = " << time_limit.GetElapsedTime(); + break; } - LOG(INFO) << "Time = " << time_limit.GetElapsedTime(); - break; + CHECK(IsAssignmentValid(problem, solver.Assignment())); + const Coefficient old_objective = objective; + objective = ComputeObjectiveValue(problem, solver.Assignment()); + PrintObjective(GetScaledObjective(problem, objective)); + CHECK_LT(objective, old_objective); } - CHECK(IsAssignmentValid(problem, solver.Assignment())); - const Coefficient old_objective = objective; - objective = ComputeObjectiveValue(problem, solver.Assignment()); - CHECK_LT(objective, old_objective); solver.Backtrack(0); - if (!AddObjectiveConstraint(problem, false, Coefficient(0), true, - objective - 1, &solver)) { - LOG(INFO) << "UNSAT (when tightenning the objective constraint)."; - LOG(INFO) << "Optimal found!"; - LOG(INFO) << "Objective = " << GetScaledObjective(problem, objective); - LOG(INFO) << "Time = " << time_limit.GetElapsedTime(); - break; + if (objective != kCoefficientMax) { + if (!AddObjectiveConstraint(problem, false, Coefficient(0), true, + objective - 1, &solver)) { + LOG(INFO) << "UNSAT (when tightenning the objective constraint)."; + LOG(INFO) << "Optimal found!"; + LOG(INFO) << "Objective = " << GetScaledObjective(problem, objective); + LOG(INFO) << "Time = " << time_limit.GetElapsedTime(); + break; + } } parameters.set_max_time_in_seconds(time_limit.GetTimeLeft()); solver.SetParameters(parameters);