21#include "absl/synchronization/mutex.h"
27using ::operations_research::sat::LinearBooleanProblem;
28using ::operations_research::sat::LinearObjective;
42 return "OPTIMAL_SOLUTION_FOUND";
44 return "SOLUTION_FOUND";
48 return "LIMIT_REACHED";
50 return "INFORMATION_FOUND";
58 LOG(DFATAL) <<
"Invalid Status " <<
static_cast<int>(status);
59 return "UNKNOWN Status";
68 : original_problem_(problem),
70 update_stamp_(kInitialStampValue + 1),
71 is_fixed_(problem.num_variables(), false),
72 fixed_values_(problem.num_variables(), false),
74 solution_(problem,
"AllZero"),
75 assignment_preference_(),
76 lower_bound_(
std::numeric_limits<int64_t>::
min()),
77 upper_bound_(
std::numeric_limits<int64_t>::
max()) {
80 const LinearObjective& objective = problem.objective();
82 for (
int i = 0; i < objective.coefficients_size(); ++i) {
84 lower_bound_ += std::min<int64_t>(int64_t{0}, objective.coefficients(i));
95 const std::string kIndent(25,
' ');
97 bool new_lp_values =
false;
99 if (lp_values_ != learned_info.
lp_values) {
101 new_lp_values =
true;
102 VLOG(1) << kIndent +
"New LP values.";
106 bool new_binary_clauses =
false;
108 const int old_num = binary_clause_manager_.
NumClauses();
110 const int num_vars = original_problem_.num_variables();
112 binary_clause_manager_.
Add(c);
115 if (binary_clause_manager_.
NumClauses() > old_num) {
116 new_binary_clauses =
true;
117 VLOG(1) << kIndent +
"Num binary clauses: "
122 bool new_solution =
false;
128 VLOG(1) << kIndent +
"New solution.";
131 bool new_lower_bound =
false;
134 new_lower_bound =
true;
135 VLOG(1) << kIndent +
"New lower bound.";
142 parameters_.relative_gap_limit() *
153 int num_newly_fixed_variables = 0;
155 const VariableIndex
var(
literal.Variable().value());
156 if (
var >= original_problem_.num_variables()) {
160 if (is_fixed_[
var]) {
166 is_fixed_[
var] =
true;
168 ++num_newly_fixed_variables;
171 if (num_newly_fixed_variables > 0) {
172 int num_fixed_variables = 0;
173 for (
const bool is_fixed : is_fixed_) {
175 ++num_fixed_variables;
178 VLOG(1) << kIndent << num_newly_fixed_variables
179 <<
" newly fixed variables (" << num_fixed_variables <<
" / "
180 << is_fixed_.size() <<
").";
181 if (num_fixed_variables == is_fixed_.size()) {
184 for (VariableIndex
var(0);
var < is_fixed_.size(); ++
var) {
188 solution_ = fixed_solution;
192 VLOG(1) << kIndent <<
"Optimal";
199 bool known_status =
false;
208 const bool updated = new_lp_values || new_binary_clauses || new_solution ||
209 new_lower_bound || num_newly_fixed_variables > 0 ||
211 if (updated) ++update_stamp_;
218 if (is_fixed_[
var]) {
244 lower_bound_ = upper_bound_ - 1;
#define VLOG(verboselevel)
std::string StatString() const
static std::string GetStatusString(Status status)
virtual ~BopOptimizerBase()
BopOptimizerBase(const std::string &name)
void SetValue(VariableIndex var, bool value)
int64_t lower_bound() const
bool MergeLearnedInfo(const LearnedInfo &learned_info, BopOptimizerBase::Status optimization_status)
const std::vector< sat::BinaryClause > & NewlyAddedBinaryClauses() const
LearnedInfo GetLearnedInfo() const
static const int64_t kInitialStampValue
const absl::StrongVector< VariableIndex, bool > & is_fixed() const
ProblemState(const sat::LinearBooleanProblem &problem)
void SynchronizationDone()
int64_t upper_bound() const
const std::vector< BinaryClause > & newly_added() const
BooleanVariable Variable() const
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
#define IF_STATS_ENABLED(instructions)
#define SCOPED_TIME_STAT(stats)
std::vector< sat::Literal > fixed_literals
std::vector< sat::BinaryClause > binary_clauses