move sat_runner from examples/cpp to ortools/sat
This commit is contained in:
Laurent Perron
@@ -463,38 +463,6 @@ cc_binary(
|
||||
],
|
||||
)
|
||||
|
||||
cc_binary(
|
||||
name = "sat_runner",
|
||||
srcs = [
|
||||
"opb_reader.h",
|
||||
"sat_cnf_reader.h",
|
||||
"sat_runner.cc",
|
||||
],
|
||||
deps = [
|
||||
"//ortools/algorithms:sparse_permutation",
|
||||
"//ortools/base",
|
||||
"//ortools/base:file",
|
||||
"//ortools/base:threadpool",
|
||||
"//ortools/lp_data:mps_reader",
|
||||
"//ortools/lp_data:proto_utils",
|
||||
"//ortools/sat:boolean_problem",
|
||||
"//ortools/sat:boolean_problem_cc_proto",
|
||||
"//ortools/sat:cp_model_cc_proto",
|
||||
"//ortools/sat:cp_model_solver",
|
||||
"//ortools/sat:drat_proof_handler",
|
||||
"//ortools/sat:lp_utils",
|
||||
"//ortools/sat:optimization",
|
||||
"//ortools/sat:sat_solver",
|
||||
"//ortools/sat:simplification",
|
||||
"//ortools/sat:symmetry",
|
||||
"//ortools/util:filelineiter",
|
||||
"//ortools/util:sigint",
|
||||
"//ortools/util:time_limit",
|
||||
"@com_google_absl//absl/status",
|
||||
"@com_google_absl//absl/strings",
|
||||
"@com_google_protobuf//:protobuf",
|
||||
],
|
||||
)
|
||||
|
||||
cc_binary(
|
||||
name = "shift_minimization_sat",
|
||||
|
||||
@@ -41,7 +41,6 @@ list(FILTER CXX_SRCS EXCLUDE REGEX ".*/multi_knapsack_sat.cc") # crash
|
||||
list(FILTER CXX_SRCS EXCLUDE REGEX ".*/network_routing_sat.cc")
|
||||
list(FILTER CXX_SRCS EXCLUDE REGEX ".*/pdlp_solve.cc")
|
||||
list(FILTER CXX_SRCS EXCLUDE REGEX ".*/pdptw.cc")
|
||||
list(FILTER CXX_SRCS EXCLUDE REGEX ".*/sat_runner.cc")
|
||||
list(FILTER CXX_SRCS EXCLUDE REGEX ".*/shift_minimization_sat.cc")
|
||||
list(FILTER CXX_SRCS EXCLUDE REGEX ".*/pdlp_solve.cc")
|
||||
list(FILTER CXX_SRCS EXCLUDE REGEX ".*/solve.cc")
|
||||
@@ -52,25 +51,3 @@ list(FILTER CXX_SRCS EXCLUDE REGEX ".*/weighted_tardiness_sat.cc")
|
||||
foreach(SAMPLE IN LISTS CXX_SRCS)
|
||||
add_cxx_example(${SAMPLE})
|
||||
endforeach()
|
||||
|
||||
# Sat Runner
|
||||
include(GNUInstallDirs)
|
||||
if(APPLE)
|
||||
set(CMAKE_INSTALL_RPATH
|
||||
"@loader_path/../${CMAKE_INSTALL_LIBDIR};@loader_path")
|
||||
elseif(UNIX)
|
||||
set(CMAKE_INSTALL_RPATH
|
||||
"$ORIGIN/../${CMAKE_INSTALL_LIBDIR}:$ORIGIN/../lib64:$ORIGIN/../lib:$ORIGIN")
|
||||
endif()
|
||||
|
||||
add_executable(sat_runner)
|
||||
target_sources(sat_runner PRIVATE
|
||||
"sat_runner.cc"
|
||||
"opb_reader.h"
|
||||
"sat_cnf_reader.h")
|
||||
target_include_directories(sat_runner PUBLIC ${CMAKE_CURRENT_SOURCE_DIR})
|
||||
target_compile_features(sat_runner PRIVATE cxx_std_17)
|
||||
target_link_libraries(sat_runner PRIVATE ${PROJECT_NAMESPACE}::ortools)
|
||||
|
||||
install(TARGETS sat_runner)
|
||||
|
||||
|
||||
@@ -1,139 +0,0 @@
|
||||
// Copyright 2010-2022 Google LLC
|
||||
// Licensed under the Apache License, Version 2.0 (the "License");
|
||||
// you may not use this file except in compliance with the License.
|
||||
// You may obtain a copy of the License at
|
||||
//
|
||||
// http://www.apache.org/licenses/LICENSE-2.0
|
||||
//
|
||||
// Unless required by applicable law or agreed to in writing, software
|
||||
// distributed under the License is distributed on an "AS IS" BASIS,
|
||||
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
// See the License for the specific language governing permissions and
|
||||
// limitations under the License.
|
||||
|
||||
#ifndef OR_TOOLS_SAT_OPB_READER_H_
|
||||
#define OR_TOOLS_SAT_OPB_READER_H_
|
||||
|
||||
#include <algorithm>
|
||||
#include <cstdint>
|
||||
#include <memory>
|
||||
#include <string>
|
||||
#include <vector>
|
||||
|
||||
#include "absl/strings/numbers.h"
|
||||
#include "absl/strings/str_split.h"
|
||||
#include "ortools/base/logging.h"
|
||||
#include "ortools/base/macros.h"
|
||||
#include "ortools/sat/boolean_problem.pb.h"
|
||||
#include "ortools/util/filelineiter.h"
|
||||
|
||||
namespace operations_research {
|
||||
namespace sat {
|
||||
|
||||
// This class loads a file in pbo file format into a LinearBooleanProblem.
|
||||
// The format is described here:
|
||||
// http://www.cril.univ-artois.fr/PB12/format.pdf
|
||||
class OpbReader {
|
||||
public:
|
||||
OpbReader() {}
|
||||
|
||||
// Loads the given opb filename into the given problem.
|
||||
bool Load(const std::string& filename, LinearBooleanProblem* problem) {
|
||||
problem->Clear();
|
||||
problem->set_name(ExtractProblemName(filename));
|
||||
|
||||
num_variables_ = 0;
|
||||
int num_lines = 0;
|
||||
for (const std::string& line : FileLines(filename)) {
|
||||
++num_lines;
|
||||
ProcessNewLine(problem, line);
|
||||
}
|
||||
if (num_lines == 0) {
|
||||
LOG(FATAL) << "File '" << filename << "' is empty or can't be read.";
|
||||
}
|
||||
problem->set_num_variables(num_variables_);
|
||||
return true;
|
||||
}
|
||||
|
||||
private:
|
||||
// Since the problem name is not stored in the cnf format, we infer it from
|
||||
// the file name.
|
||||
static std::string ExtractProblemName(const std::string& filename) {
|
||||
const int found = filename.find_last_of('/');
|
||||
const std::string problem_name =
|
||||
found != std::string::npos ? filename.substr(found + 1) : filename;
|
||||
return problem_name;
|
||||
}
|
||||
|
||||
void ProcessNewLine(LinearBooleanProblem* problem, const std::string& line) {
|
||||
const std::vector<std::string> words =
|
||||
absl::StrSplit(line, absl::ByAnyChar(" ;"), absl::SkipEmpty());
|
||||
if (words.empty() || words[0].empty() || words[0][0] == '*') {
|
||||
return;
|
||||
}
|
||||
|
||||
if (words[0] == "min:") {
|
||||
LinearObjective* objective = problem->mutable_objective();
|
||||
for (int i = 1; i < words.size(); ++i) {
|
||||
const std::string& word = words[i];
|
||||
if (word.empty() || word[0] == ';') continue;
|
||||
if (word[0] == 'x') {
|
||||
int literal;
|
||||
CHECK(absl::SimpleAtoi(word.substr(1), &literal));
|
||||
num_variables_ = std::max(num_variables_, literal);
|
||||
objective->add_literals(literal);
|
||||
} else {
|
||||
int64_t value;
|
||||
CHECK(absl::SimpleAtoi(word, &value));
|
||||
objective->add_coefficients(value);
|
||||
}
|
||||
}
|
||||
if (objective->literals_size() != objective->coefficients_size()) {
|
||||
LOG(INFO) << "words.size() = " << words.size();
|
||||
LOG(FATAL) << "Failed to parse objective:\n " << line;
|
||||
}
|
||||
return;
|
||||
}
|
||||
LinearBooleanConstraint* constraint = problem->add_constraints();
|
||||
for (int i = 0; i < words.size(); ++i) {
|
||||
const std::string& word = words[i];
|
||||
CHECK(!word.empty());
|
||||
if (word == ">=") {
|
||||
CHECK_LT(i + 1, words.size());
|
||||
int64_t value;
|
||||
CHECK(absl::SimpleAtoi(words[i + 1], &value));
|
||||
constraint->set_lower_bound(value);
|
||||
break;
|
||||
} else if (word == "=") {
|
||||
CHECK_LT(i + 1, words.size());
|
||||
int64_t value;
|
||||
CHECK(absl::SimpleAtoi(words[i + 1], &value));
|
||||
constraint->set_upper_bound(value);
|
||||
constraint->set_lower_bound(value);
|
||||
break;
|
||||
} else {
|
||||
if (word[0] == 'x') {
|
||||
int literal;
|
||||
CHECK(absl::SimpleAtoi(word.substr(1), &literal));
|
||||
num_variables_ = std::max(num_variables_, literal);
|
||||
constraint->add_literals(literal);
|
||||
} else {
|
||||
int64_t value;
|
||||
CHECK(absl::SimpleAtoi(words[i], &value));
|
||||
constraint->add_coefficients(value);
|
||||
}
|
||||
}
|
||||
}
|
||||
if (constraint->literals_size() != constraint->coefficients_size()) {
|
||||
LOG(FATAL) << "Failed to parse constraint:\n " << line;
|
||||
}
|
||||
}
|
||||
|
||||
int num_variables_;
|
||||
DISALLOW_COPY_AND_ASSIGN(OpbReader);
|
||||
};
|
||||
|
||||
} // namespace sat
|
||||
} // namespace operations_research
|
||||
|
||||
#endif // OR_TOOLS_SAT_OPB_READER_H_
|
||||
@@ -1,343 +0,0 @@
|
||||
// Copyright 2010-2022 Google LLC
|
||||
// Licensed under the Apache License, Version 2.0 (the "License");
|
||||
// you may not use this file except in compliance with the License.
|
||||
// You may obtain a copy of the License at
|
||||
//
|
||||
// http://www.apache.org/licenses/LICENSE-2.0
|
||||
//
|
||||
// Unless required by applicable law or agreed to in writing, software
|
||||
// distributed under the License is distributed on an "AS IS" BASIS,
|
||||
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
// See the License for the specific language governing permissions and
|
||||
// limitations under the License.
|
||||
|
||||
#ifndef OR_TOOLS_SAT_SAT_CNF_READER_H_
|
||||
#define OR_TOOLS_SAT_SAT_CNF_READER_H_
|
||||
|
||||
#include <cstdint>
|
||||
#include <memory>
|
||||
#include <string>
|
||||
#include <utility>
|
||||
#include <vector>
|
||||
|
||||
#include "absl/container/btree_map.h"
|
||||
#include "absl/flags/flag.h"
|
||||
#include "absl/strings/numbers.h"
|
||||
#include "absl/strings/str_split.h"
|
||||
#include "absl/strings/string_view.h"
|
||||
#include "absl/types/span.h"
|
||||
#include "ortools/base/commandlineflags.h"
|
||||
#include "ortools/base/integral_types.h"
|
||||
#include "ortools/base/logging.h"
|
||||
#include "ortools/base/macros.h"
|
||||
#include "ortools/sat/boolean_problem.pb.h"
|
||||
#include "ortools/sat/cp_model.pb.h"
|
||||
#include "ortools/util/filelineiter.h"
|
||||
|
||||
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.");
|
||||
|
||||
namespace operations_research {
|
||||
namespace sat {
|
||||
|
||||
struct LinearBooleanProblemWrapper {
|
||||
explicit LinearBooleanProblemWrapper(LinearBooleanProblem* p) : problem(p) {}
|
||||
|
||||
void SetNumVariables(int num) { problem->set_num_variables(num); }
|
||||
void SetOriginalNumVariables(int num) {
|
||||
problem->set_original_num_variables(num);
|
||||
}
|
||||
|
||||
void AddConstraint(absl::Span<const int> clause) {
|
||||
LinearBooleanConstraint* constraint = problem->add_constraints();
|
||||
constraint->mutable_literals()->Reserve(clause.size());
|
||||
constraint->mutable_coefficients()->Reserve(clause.size());
|
||||
constraint->set_lower_bound(1);
|
||||
for (const int literal : clause) {
|
||||
constraint->add_literals(literal);
|
||||
constraint->add_coefficients(1);
|
||||
}
|
||||
}
|
||||
|
||||
void AddObjectiveTerm(int literal, int64_t value) {
|
||||
CHECK_GE(literal, 0) << "Negative literal not supported.";
|
||||
problem->mutable_objective()->add_literals(literal);
|
||||
problem->mutable_objective()->add_coefficients(value);
|
||||
}
|
||||
|
||||
void SetObjectiveOffset(int64_t offset) {
|
||||
problem->mutable_objective()->set_offset(offset);
|
||||
}
|
||||
|
||||
LinearBooleanProblem* problem;
|
||||
};
|
||||
|
||||
struct CpModelProtoWrapper {
|
||||
explicit CpModelProtoWrapper(CpModelProto* p) : problem(p) {}
|
||||
|
||||
void SetNumVariables(int num) {
|
||||
for (int i = 0; i < num; ++i) {
|
||||
IntegerVariableProto* variable = problem->add_variables();
|
||||
variable->add_domain(0);
|
||||
variable->add_domain(1);
|
||||
}
|
||||
}
|
||||
|
||||
// TODO(user): Not supported. This is only used for displaying a wcnf
|
||||
// solution in cnf format, so it is not useful internally. Instead of adding
|
||||
// another field, we could use the variables names or the search heuristics
|
||||
// to encode this info.
|
||||
void SetOriginalNumVariables(int num) {}
|
||||
|
||||
int LiteralToRef(int signed_value) {
|
||||
return signed_value > 0 ? signed_value - 1 : signed_value;
|
||||
}
|
||||
|
||||
void AddConstraint(absl::Span<const int> clause) {
|
||||
auto* constraint = problem->add_constraints()->mutable_bool_or();
|
||||
constraint->mutable_literals()->Reserve(clause.size());
|
||||
for (const int literal : clause) {
|
||||
constraint->add_literals(LiteralToRef(literal));
|
||||
}
|
||||
}
|
||||
|
||||
void AddObjectiveTerm(int literal, int64_t value) {
|
||||
CHECK_GE(literal, 0) << "Negative literal not supported.";
|
||||
problem->mutable_objective()->add_vars(LiteralToRef(literal));
|
||||
problem->mutable_objective()->add_coeffs(value);
|
||||
}
|
||||
|
||||
void SetObjectiveOffset(int64_t offset) {
|
||||
problem->mutable_objective()->set_offset(offset);
|
||||
}
|
||||
|
||||
CpModelProto* problem;
|
||||
};
|
||||
|
||||
// This class loads a file in cnf file format into a SatProblem.
|
||||
// The format is described here:
|
||||
// http://people.sc.fsu.edu/~jburkardt/data/cnf/cnf.html
|
||||
//
|
||||
// It also support the wcnf input format for partial weighted max-sat problems.
|
||||
class SatCnfReader {
|
||||
public:
|
||||
SatCnfReader() : interpret_cnf_as_max_sat_(false) {}
|
||||
|
||||
// If called with true, then a cnf file will be converted to the max-sat
|
||||
// problem: Try to minimize the number of unsatisfiable clauses.
|
||||
void InterpretCnfAsMaxSat(bool v) { interpret_cnf_as_max_sat_ = v; }
|
||||
|
||||
// Loads the given cnf filename into the given proto.
|
||||
bool Load(const std::string& filename, LinearBooleanProblem* problem) {
|
||||
problem->Clear();
|
||||
problem->set_name(ExtractProblemName(filename));
|
||||
LinearBooleanProblemWrapper wrapper(problem);
|
||||
return LoadInternal(filename, &wrapper);
|
||||
}
|
||||
bool Load(const std::string& filename, CpModelProto* problem) {
|
||||
problem->Clear();
|
||||
problem->set_name(ExtractProblemName(filename));
|
||||
CpModelProtoWrapper wrapper(problem);
|
||||
return LoadInternal(filename, &wrapper);
|
||||
}
|
||||
|
||||
private:
|
||||
template <class Problem>
|
||||
bool LoadInternal(const std::string& filename, Problem* problem) {
|
||||
positive_literal_to_weight_.clear();
|
||||
objective_offset_ = 0;
|
||||
is_wcnf_ = false;
|
||||
end_marker_seen_ = false;
|
||||
hard_weight_ = 0;
|
||||
num_skipped_soft_clauses_ = 0;
|
||||
num_singleton_soft_clauses_ = 0;
|
||||
num_added_clauses_ = 0;
|
||||
num_slack_variables_ = 0;
|
||||
|
||||
int num_lines = 0;
|
||||
for (const std::string& line : FileLines(filename)) {
|
||||
++num_lines;
|
||||
ProcessNewLine(line, problem);
|
||||
}
|
||||
if (num_lines == 0) {
|
||||
LOG(FATAL) << "File '" << filename << "' is empty or can't be read.";
|
||||
}
|
||||
problem->SetOriginalNumVariables(num_variables_);
|
||||
problem->SetNumVariables(num_variables_ + num_slack_variables_);
|
||||
|
||||
// Fill the objective.
|
||||
if (!positive_literal_to_weight_.empty()) {
|
||||
for (const std::pair<int, int64_t> p : positive_literal_to_weight_) {
|
||||
if (p.second != 0) {
|
||||
problem->AddObjectiveTerm(p.first, p.second);
|
||||
}
|
||||
}
|
||||
problem->SetObjectiveOffset(objective_offset_);
|
||||
}
|
||||
|
||||
if (num_clauses_ != num_added_clauses_ + num_singleton_soft_clauses_ +
|
||||
num_skipped_soft_clauses_) {
|
||||
LOG(ERROR) << "Wrong number of clauses. " << num_clauses_ << " "
|
||||
<< num_added_clauses_;
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
// Since the problem name is not stored in the cnf format, we infer it from
|
||||
// the file name.
|
||||
static std::string ExtractProblemName(const std::string& filename) {
|
||||
const int found = filename.find_last_of('/');
|
||||
const std::string problem_name =
|
||||
found != std::string::npos ? filename.substr(found + 1) : filename;
|
||||
return problem_name;
|
||||
}
|
||||
|
||||
int64_t StringPieceAtoi(absl::string_view input) {
|
||||
int64_t value;
|
||||
// Hack: data() is not null terminated, but we do know that it points
|
||||
// inside a string where numbers are separated by " " and since SimpleAtoi
|
||||
// will stop at the first invalid char, this works.
|
||||
CHECK(absl::SimpleAtoi(input, &value));
|
||||
return value;
|
||||
}
|
||||
|
||||
void ProcessHeader(const std::string& line) {
|
||||
static const char kWordDelimiters[] = " ";
|
||||
words_ = absl::StrSplit(line, kWordDelimiters, absl::SkipEmpty());
|
||||
|
||||
CHECK_EQ(words_[0], "p");
|
||||
if (words_[1] == "cnf" || words_[1] == "wcnf") {
|
||||
num_variables_ = StringPieceAtoi(words_[2]);
|
||||
num_clauses_ = StringPieceAtoi(words_[3]);
|
||||
if (words_[1] == "wcnf") {
|
||||
is_wcnf_ = true;
|
||||
hard_weight_ = (words_.size() > 4) ? StringPieceAtoi(words_[4]) : 0;
|
||||
}
|
||||
} else {
|
||||
// TODO(user): The ToString() is only required for the open source. Fix.
|
||||
LOG(FATAL) << "Unknown file type: " << words_[1];
|
||||
}
|
||||
}
|
||||
|
||||
template <class Problem>
|
||||
void ProcessNewLine(const std::string& line, Problem* problem) {
|
||||
if (line.empty() || end_marker_seen_) return;
|
||||
if (line[0] == 'c') return;
|
||||
if (line[0] == '%') {
|
||||
end_marker_seen_ = true;
|
||||
return;
|
||||
}
|
||||
if (line[0] == 'p') {
|
||||
ProcessHeader(line);
|
||||
return;
|
||||
}
|
||||
|
||||
static const char kWordDelimiters[] = " ";
|
||||
auto splitter = absl::StrSplit(line, kWordDelimiters, absl::SkipEmpty());
|
||||
|
||||
tmp_clause_.clear();
|
||||
int64_t weight =
|
||||
(!is_wcnf_ && interpret_cnf_as_max_sat_) ? 1 : hard_weight_;
|
||||
bool first = true;
|
||||
bool end_marker_seen = false;
|
||||
for (const absl::string_view word : splitter) {
|
||||
const int64_t signed_value = StringPieceAtoi(word);
|
||||
if (first && is_wcnf_) {
|
||||
// Mathematically, a soft clause of weight 0 can be removed.
|
||||
if (signed_value == 0) {
|
||||
++num_skipped_soft_clauses_;
|
||||
return;
|
||||
}
|
||||
weight = signed_value;
|
||||
} else {
|
||||
if (signed_value == 0) {
|
||||
end_marker_seen = true;
|
||||
break; // end of clause.
|
||||
}
|
||||
tmp_clause_.push_back(signed_value);
|
||||
}
|
||||
first = false;
|
||||
}
|
||||
if (!end_marker_seen) return;
|
||||
|
||||
if (weight == hard_weight_) {
|
||||
++num_added_clauses_;
|
||||
problem->AddConstraint(tmp_clause_);
|
||||
} else {
|
||||
if (tmp_clause_.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 add the cost to
|
||||
// the unique variable of such clause and remove the clause.
|
||||
++num_singleton_soft_clauses_;
|
||||
const int literal = -tmp_clause_[0];
|
||||
if (literal > 0) {
|
||||
positive_literal_to_weight_[literal] += weight;
|
||||
} else {
|
||||
positive_literal_to_weight_[-literal] -= weight;
|
||||
objective_offset_ += weight;
|
||||
}
|
||||
} 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_;
|
||||
|
||||
tmp_clause_.push_back(slack_literal);
|
||||
|
||||
++num_added_clauses_;
|
||||
problem->AddConstraint(tmp_clause_);
|
||||
|
||||
if (slack_literal > 0) {
|
||||
positive_literal_to_weight_[slack_literal] += weight;
|
||||
} else {
|
||||
positive_literal_to_weight_[-slack_literal] -= weight;
|
||||
objective_offset_ += weight;
|
||||
}
|
||||
|
||||
if (absl::GetFlag(FLAGS_wcnf_use_strong_slack)) {
|
||||
// Add the binary implications slack_literal true => all the other
|
||||
// clause literals are false.
|
||||
for (int i = 0; i + 1 < tmp_clause_.size(); ++i) {
|
||||
problem->AddConstraint({-slack_literal, -tmp_clause_[i]});
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
bool interpret_cnf_as_max_sat_;
|
||||
|
||||
int num_clauses_;
|
||||
int num_variables_;
|
||||
|
||||
// Temporary storage for ProcessNewLine().
|
||||
std::vector<absl::string_view> words_;
|
||||
|
||||
// We stores the objective in a map because we want the variables to appear
|
||||
// only once in the LinearObjective proto.
|
||||
absl::btree_map<int, int64_t> positive_literal_to_weight_;
|
||||
int64_t objective_offset_;
|
||||
|
||||
// Used for the wcnf format.
|
||||
bool is_wcnf_;
|
||||
// Some files have text after %. This indicates if we have seen the '%'.
|
||||
bool end_marker_seen_;
|
||||
int64_t hard_weight_;
|
||||
|
||||
int num_slack_variables_;
|
||||
int num_skipped_soft_clauses_;
|
||||
int num_singleton_soft_clauses_;
|
||||
int num_added_clauses_;
|
||||
|
||||
std::vector<int> tmp_clause_;
|
||||
|
||||
DISALLOW_COPY_AND_ASSIGN(SatCnfReader);
|
||||
};
|
||||
|
||||
} // namespace sat
|
||||
} // namespace operations_research
|
||||
|
||||
#endif // OR_TOOLS_SAT_SAT_CNF_READER_H_
|
||||
@@ -1,457 +0,0 @@
|
||||
// Copyright 2010-2022 Google LLC
|
||||
// Licensed under the Apache License, Version 2.0 (the "License");
|
||||
// you may not use this file except in compliance with the License.
|
||||
// You may obtain a copy of the License at
|
||||
//
|
||||
// http://www.apache.org/licenses/LICENSE-2.0
|
||||
//
|
||||
// Unless required by applicable law or agreed to in writing, software
|
||||
// distributed under the License is distributed on an "AS IS" BASIS,
|
||||
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
// See the License for the specific language governing permissions and
|
||||
// limitations under the License.
|
||||
|
||||
#include <cstdint>
|
||||
#include <cstdlib>
|
||||
#include <memory>
|
||||
#include <string>
|
||||
#include <utility>
|
||||
#include <vector>
|
||||
|
||||
#include "absl/flags/flag.h"
|
||||
#include "absl/random/random.h"
|
||||
#include "absl/status/status.h"
|
||||
#include "absl/strings/match.h"
|
||||
#include "absl/strings/numbers.h"
|
||||
#include "absl/strings/str_cat.h"
|
||||
#include "absl/strings/str_format.h"
|
||||
#include "absl/strings/string_view.h"
|
||||
#include "examples/cpp/opb_reader.h"
|
||||
#include "examples/cpp/sat_cnf_reader.h"
|
||||
#include "google/protobuf/text_format.h"
|
||||
#include "ortools/algorithms/sparse_permutation.h"
|
||||
#include "ortools/base/helpers.h"
|
||||
#include "ortools/base/init_google.h"
|
||||
#include "ortools/base/logging.h"
|
||||
#include "ortools/base/timer.h"
|
||||
#include "ortools/linear_solver/linear_solver.pb.h"
|
||||
#include "ortools/lp_data/lp_data.h"
|
||||
#include "ortools/lp_data/mps_reader.h"
|
||||
#include "ortools/lp_data/proto_utils.h"
|
||||
#include "ortools/sat/boolean_problem.h"
|
||||
#include "ortools/sat/boolean_problem.pb.h"
|
||||
#include "ortools/sat/cp_model.pb.h"
|
||||
#include "ortools/sat/cp_model_solver.h"
|
||||
#include "ortools/sat/lp_utils.h"
|
||||
#include "ortools/sat/model.h"
|
||||
#include "ortools/sat/optimization.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"
|
||||
#include "ortools/sat/simplification.h"
|
||||
#include "ortools/sat/symmetry.h"
|
||||
#include "ortools/util/file_util.h"
|
||||
#include "ortools/util/logging.h"
|
||||
#include "ortools/util/strong_integers.h"
|
||||
#include "ortools/util/time_limit.h"
|
||||
|
||||
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).");
|
||||
|
||||
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, 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.");
|
||||
|
||||
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) {
|
||||
if (absl::EndsWith(filename, ".opb") ||
|
||||
absl::EndsWith(filename, ".opb.bz2")) {
|
||||
OpbReader reader;
|
||||
if (!reader.Load(filename, problem)) {
|
||||
LOG(FATAL) << "Cannot load file '" << filename << "'.";
|
||||
}
|
||||
} else if (absl::EndsWith(filename, ".cnf") ||
|
||||
absl::EndsWith(filename, ".cnf.gz") ||
|
||||
absl::EndsWith(filename, ".wcnf") ||
|
||||
absl::EndsWith(filename, ".wcnf.gz")) {
|
||||
SatCnfReader reader;
|
||||
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 << "'.";
|
||||
}
|
||||
}
|
||||
} else if (absl::GetFlag(FLAGS_use_cp_model)) {
|
||||
LOG(INFO) << "Reading a CpModelProto.";
|
||||
*cp_model = ReadFileToProtoOrDie<CpModelProto>(filename);
|
||||
} else {
|
||||
LOG(INFO) << "Reading a LinearBooleanProblem.";
|
||||
*problem = ReadFileToProtoOrDie<LinearBooleanProblem>(filename);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
std::string SolutionString(const LinearBooleanProblem& problem,
|
||||
const std::vector<bool>& 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()) {
|
||||
LOG(FATAL) << "Please supply a data file with --input=";
|
||||
}
|
||||
|
||||
// Parse the --params flag.
|
||||
parameters.set_log_search_progress(true);
|
||||
if (!absl::GetFlag(FLAGS_params).empty()) {
|
||||
CHECK(google::protobuf::TextFormat::MergeFromString(
|
||||
absl::GetFlag(FLAGS_params), ¶meters))
|
||||
<< absl::GetFlag(FLAGS_params);
|
||||
}
|
||||
|
||||
// Initialize the solver.
|
||||
std::unique_ptr<SatSolver> solver(new SatSolver());
|
||||
solver->SetParameters(parameters);
|
||||
|
||||
// Read the problem.
|
||||
LinearBooleanProblem problem;
|
||||
CpModelProto cp_model;
|
||||
if (!LoadBooleanProblem(absl::GetFlag(FLAGS_input), &problem, &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()));
|
||||
}
|
||||
}
|
||||
|
||||
// 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<std::unique_ptr<SparsePermutation>> generators;
|
||||
FindLinearBooleanProblemSymmetries(problem, &generators);
|
||||
std::unique_ptr<SymmetryPropagator> 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<bool> 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<SatSolver>();
|
||||
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<TimeLimit> 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));
|
||||
}
|
||||
} 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,
|
||||
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());
|
||||
|
||||
return EXIT_SUCCESS;
|
||||
}
|
||||
|
||||
} // namespace
|
||||
} // namespace sat
|
||||
} // namespace operations_research
|
||||
|
||||
static const char kUsage[] =
|
||||
"Usage: see flags.\n"
|
||||
"This program solves a given Boolean linear problem.";
|
||||
|
||||
int main(int argc, char** argv) {
|
||||
// By default, we want to show how the solver progress. Note that this needs
|
||||
// to be set before InitGoogle() which has the nice side-effect of allowing
|
||||
// the user to override it.
|
||||
InitGoogle(kUsage, &argc, &argv, /*remove_flags=*/true);
|
||||
absl::SetFlag(&FLAGS_logtostderr, true);
|
||||
return operations_research::sat::Run();
|
||||
}
|
||||
Reference in New Issue
Block a user