always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

update examples

Browse Source
This commit is contained in:
lperron@google.com
2014-05-21 12:56:57 +00:00
parent 6fbf886676
commit aee340b07c
9 changed files with 205 additions and 102 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
examples/cpp/dobble_ls.cc
View File

@@ -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) {

5
examples/cpp/jobshop.h
View File

@@ -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<std::string> words;
SplitStringUsing(line, kWordDelimiters, &words);
const std::vector<std::string> words =
strings::Split(line, " ", strings::SkipEmpty());
switch (problem_type_) {
case UNDEFINED: {
if (words.size() == 2 && words[0] == "instance") {

2
examples/cpp/ls_api.cc
View File

@@ -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);

5
examples/cpp/multidim_knapsack.cc
View File

@@ -90,9 +90,8 @@ class MultiDimKnapsackData {
// Used internally.
void ProcessNewLine(char* const line) {
const char* const kWordDelimiters(" ");
std::vector<std::string> words;
SplitStringUsing(line, kWordDelimiters, &words);
const std::vector<std::string> words =
strings::Split(line, " ", strings::SkipEmpty());
line_read_++;
if (problem_type_ == -1) {
if (words.size() == 1) {

5
examples/cpp/opb_reader.h
View File

@@ -64,9 +64,8 @@ class OpbReader {
}
void ProcessNewLine(LinearBooleanProblem* problem, const std::string& line) {
static const char kWordDelimiters[] = " ";
std::vector<std::string> words;
SplitStringUsing(line, kWordDelimiters, &words);
const std::vector<std::string> words =
strings::Split(line, " ", strings::SkipEmpty());
if (words.size() == 0 || words[0].empty() || words[0][0] == '*') {
return;
}

10
examples/cpp/pdptw.cc
View File

@@ -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<std::string> 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()) {

30
examples/cpp/print_dimacs_assignment.h
View File

@@ -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<GraphType>& 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 <typename GraphType>
void PrintDimacsAssignmentProblem(
const LinearSumAssignment<GraphType>& assignment,
const TailArrayManager<GraphType>& 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<GraphType>::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());
}
}

95
examples/cpp/sat_cnf_reader.h
View File

@@ -13,9 +13,11 @@
#ifndef OR_TOOLS_SAT_SAT_CNF_READER_H_
#define OR_TOOLS_SAT_SAT_CNF_READER_H_
#include <map>
#include <string>
#include <vector>
#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<int64> 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);
};

153
examples/cpp/sat_runner.cc
View File

@@ -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<SatParameters::VariableOrder>(
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<SatParameters::Polarity>(
polarity_d->value(random->Uniform(polarity_d->value_count()))->number()));
// Other random parameters.
parameters->set_use_phase_saving(random->OneIn(2));
const std::vector<double> 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<int64>(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<int64>::max();
int64 max_seen = std::numeric_limits<int64>::min();
int64 best = min_seen;
for (int i = 0; i < num_solve; ++i) {
solver->Backtrack(0);
RandomizeDecisionHeuristic(&random, &parameters);
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<int64>(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<int64>(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);