21 #include "absl/memory/memory.h"
22 #include "absl/strings/str_format.h"
23 #include "google/protobuf/text_format.h"
40 using ::operations_research::glop::ColIndex;
42 using ::operations_research::glop::GlopParameters;
43 using ::operations_research::glop::RowIndex;
46 int64_t lower_bound) {
49 return solution.IsFeasible() ? (solution.GetCost() <= lower_bound
55 bool AllIntegralValues(
const DenseRow& values,
double tolerance) {
59 if (
value >= tolerance &&
value + tolerance < 1.0) {
66 void DenseRowToBopSolution(
const DenseRow& values, BopSolution* solution) {
67 CHECK(solution !=
nullptr);
68 CHECK_EQ(solution->Size(), values.size());
69 for (VariableIndex
var(0);
var < solution->Size(); ++
var) {
70 solution->SetValue(
var, round(values[ColIndex(
var.value())]));
91 if (state_update_stamp_ == problem_state.
update_stamp()) {
98 sat_solver_ = absl::make_unique<sat::SatSolver>();
102 .exploit_symmetry_in_sat_first_solution()) {
103 std::vector<std::unique_ptr<SparsePermutation>> generators;
106 std::unique_ptr<sat::SymmetryPropagator> propagator(
108 for (
int i = 0; i < generators.size(); ++i) {
109 propagator->AddSymmetry(std::move(generators[i]));
111 sat_solver_->AddPropagator(propagator.get());
112 sat_solver_->TakePropagatorOwnership(std::move(propagator));
126 sat_solver_->SetAssignmentPreference(
127 sat::Literal(sat::BooleanVariable(
col.value()), round(
value) == 1),
137 sat_solver_->SetAssignmentPreference(
138 sat::Literal(sat::BooleanVariable(i),
149 if (abort_)
return false;
163 CHECK(learned_info !=
nullptr);
165 learned_info->
Clear();
168 SynchronizeIfNeeded(problem_state);
171 sat::SatParameters sat_params;
172 sat_params.set_max_time_in_seconds(
time_limit->GetTimeLeft());
173 sat_params.set_max_deterministic_time(
time_limit->GetDeterministicTimeLeft());
174 sat_params.set_random_seed(
parameters.random_seed());
180 sat_params.set_max_number_of_conflicts(
182 sat_solver_->SetParameters(sat_params);
184 const double initial_deterministic_time = sat_solver_->deterministic_time();
186 time_limit->AdvanceDeterministicTime(sat_solver_->deterministic_time() -
187 initial_deterministic_time);
218 sat_propagator_(sat_propagator) {}
231 CHECK(learned_info !=
nullptr);
233 learned_info->
Clear();
236 const sat::SatParameters saved_params = sat_propagator_->
parameters();
237 const std::vector<std::pair<sat::Literal, double>> saved_prefs =
240 const int kMaxNumConflicts = 10;
244 int64_t remaining_num_conflicts =
245 parameters.max_number_of_conflicts_in_random_solution_generation();
246 int64_t old_num_failures = 0;
250 bool objective_need_to_be_overconstrained =
253 bool solution_found =
false;
254 while (remaining_num_conflicts > 0 && !
time_limit->LimitReached()) {
258 sat::SatParameters sat_params = saved_params;
260 sat_params.set_max_number_of_conflicts(kMaxNumConflicts);
264 if (objective_need_to_be_overconstrained) {
267 true, sat::Coefficient(best_cost) - 1, sat_propagator_)) {
274 objective_need_to_be_overconstrained =
false;
278 const int preference = random_->
Uniform(4);
279 if (preference == 0) {
282 }
else if (preference == 1 && !problem_state.
lp_values().
empty()) {
295 objective_need_to_be_overconstrained =
true;
296 solution_found =
true;
311 remaining_num_conflicts -=
344 const std::string&
name)
348 lp_model_loaded_(false),
354 num_fixed_variables_(-1),
355 problem_already_solved_(false),
356 scaled_solution_cost_(glop::
kInfinity) {}
362 if (state_update_stamp_ == problem_state.
update_stamp()) {
370 parameters_.max_lp_solve_for_feasibility_problems() >= 0 &&
371 num_full_solves_ >= parameters_.max_lp_solve_for_feasibility_problems()) {
377 int num_fixed_variables = 0;
378 for (
const bool is_fixed : problem_state.
is_fixed()) {
380 ++num_fixed_variables;
383 problem_already_solved_ =
384 problem_already_solved_ && num_fixed_variables_ >= num_fixed_variables;
388 num_fixed_variables_ = num_fixed_variables;
389 if (!lp_model_loaded_) {
393 lp_model_loaded_ =
true;
404 if (parameters_.use_learned_binary_clauses_in_lp()) {
405 for (
const sat::BinaryClause& clause :
408 const int64_t coefficient_a = clause.a.IsPositive() ? 1 : -1;
409 const int64_t coefficient_b = clause.b.IsPositive() ? 1 : -1;
410 const int64_t rhs = 1 + (clause.a.IsPositive() ? 0 : -1) +
411 (clause.b.IsPositive() ? 0 : -1);
412 const ColIndex col_a(clause.a.Variable().value());
413 const ColIndex col_b(clause.b.Variable().value());
419 (clause.a.IsPositive() ? name_a :
"not(" + name_a +
")") +
" or " +
420 (clause.b.IsPositive() ? name_b :
"not(" + name_b +
")"));
429 scaled_solution_cost_ =
444 parameters_.max_lp_solve_for_feasibility_problems() != 0;
450 CHECK(learned_info !=
nullptr);
452 learned_info->
Clear();
455 SynchronizeIfNeeded(problem_state);
468 problem_already_solved_ =
true;
485 if (parameters_.use_lp_strong_branching()) {
487 ComputeLowerBoundUsingStrongBranching(learned_info,
time_limit);
489 << absl::StrFormat(
"%.6f", lower_bound)
490 <<
" using strong branching.";
493 const int tolerance_sign = scaling_ < 0 ? 1 : -1;
494 const double unscaled_cost =
497 lp_solver_.
GetParameters().solution_feasibility_tolerance()) /
500 learned_info->
lower_bound =
static_cast<int64_t
>(ceil(unscaled_cost));
502 if (AllIntegralValues(
504 lp_solver_.
GetParameters().primal_feasibility_tolerance())) {
520 GlopParameters glop_params;
521 if (incremental_solve) {
522 glop_params.set_use_dual_simplex(
true);
523 glop_params.set_allow_simplex_algorithm_change(
true);
524 glop_params.set_use_preprocessing(
false);
528 parameters_.lp_max_deterministic_time());
530 lp_model_, nested_time_limit.GetTimeLimit());
534 double LinearRelaxation::ComputeLowerBoundUsingStrongBranching(
535 LearnedInfo* learned_info, TimeLimit*
time_limit) {
537 const double tolerance =
540 for (glop::ColIndex
col(0);
col < initial_lp_values.size(); ++
col) {
564 (initial_lp_values[
col] < tolerance ||
565 initial_lp_values[
col] + tolerance > 1)) {
569 double objective_true = best_lp_objective;
570 double objective_false = best_lp_objective;
594 std::max(objective_true, objective_false))
595 : std::
max(best_lp_objective,
596 std::
min(objective_true, objective_false));
600 if (CostIsWorseThanSolution(objective_true, tolerance)) {
604 learned_info->fixed_literals.push_back(
605 sat::Literal(sat::BooleanVariable(
col.value()),
false));
606 }
else if (CostIsWorseThanSolution(objective_false, tolerance)) {
610 learned_info->fixed_literals.push_back(
611 sat::Literal(sat::BooleanVariable(
col.value()),
true));
617 return best_lp_objective;
620 bool LinearRelaxation::CostIsWorseThanSolution(
double scaled_cost,
621 double tolerance)
const {
#define CHECK_LT(val1, val2)
#define CHECK_EQ(val1, val2)
#define VLOG(verboselevel)
Provides a way to nest time limits for algorithms where a certain part of the computation is bounded ...
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
bool ShouldBeRun(const ProblemState &problem_state) const override
BopRandomFirstSolutionGenerator(const std::string &name, const BopParameters ¶meters, sat::SatSolver *sat_propagator, MTRandom *random)
Status Optimize(const BopParameters ¶meters, const ProblemState &problem_state, LearnedInfo *learned_info, TimeLimit *time_limit) override
~BopRandomFirstSolutionGenerator() override
double GetScaledCost() const
bool ShouldBeRun(const ProblemState &problem_state) const override
GuidedSatFirstSolutionGenerator(const std::string &name, Policy policy)
~GuidedSatFirstSolutionGenerator() override
Status Optimize(const BopParameters ¶meters, const ProblemState &problem_state, LearnedInfo *learned_info, TimeLimit *time_limit) override
bool ShouldBeRun(const ProblemState &problem_state) const override
Status Optimize(const BopParameters ¶meters, const ProblemState &problem_state, LearnedInfo *learned_info, TimeLimit *time_limit) override
LinearRelaxation(const BopParameters ¶meters, const std::string &name)
~LinearRelaxation() override
const BopParameters & GetParameters() const
const sat::LinearBooleanProblem & original_problem() const
const std::vector< bool > assignment_preference() const
int64_t lower_bound() const
const glop::DenseRow & lp_values() const
const std::vector< sat::BinaryClause > & NewlyAddedBinaryClauses() const
bool IsVariableFixed(VariableIndex var) const
bool GetVariableFixedValue(VariableIndex var) const
int64_t update_stamp() const
const BopSolution & solution() const
int64_t upper_bound() const
const absl::StrongVector< VariableIndex, bool > & is_fixed() const
const GlopParameters & GetParameters() const
const DenseRow & variable_values() const
Fractional GetObjectiveValue() const
ABSL_MUST_USE_RESULT ProblemStatus SolveWithTimeLimit(const LinearProgram &lp, TimeLimit *time_limit)
void SetParameters(const GlopParameters ¶meters)
void SetVariableBounds(ColIndex col, Fractional lower_bound, Fractional upper_bound)
std::string GetVariableName(ColIndex col) const
void SetConstraintName(RowIndex row, absl::string_view name)
void SetCoefficient(RowIndex row, ColIndex col, Fractional value)
const DenseRow & variable_lower_bounds() const
void SetConstraintBounds(RowIndex row, Fractional lower_bound, Fractional upper_bound)
bool IsMaximizationProblem() const
const DenseRow & variable_upper_bounds() const
RowIndex CreateNewConstraint()
std::vector< std::pair< Literal, double > > AllPreferences() const
const SatParameters & parameters() const
void ResetDecisionHeuristicAndSetAllPreferences(const std::vector< std::pair< Literal, double >> &prefs)
void ResetDecisionHeuristic()
Status SolveWithTimeLimit(TimeLimit *time_limit)
int64 num_failures() const
int AssumptionLevel() const
void SetAssignmentPreference(Literal literal, double weight)
const VariablesAssignment & Assignment() const
void SetParameters(const SatParameters ¶meters)
void Backtrack(int target_level)
bool RestoreSolverToAssumptionLevel()
bool IsModelUnsat() const
SharedTimeLimit * time_limit
BopOptimizerBase::Status LoadStateProblemToSatSolver(const ProblemState &problem_state, sat::SatSolver *sat_solver)
void SatAssignmentToBopSolution(const sat::VariablesAssignment &assignment, BopSolution *solution)
void ExtractLearnedInfoFromSatSolver(sat::SatSolver *solver, LearnedInfo *info)
StrictITIVector< ColIndex, Fractional > DenseRow
std::string GetProblemStatusString(ProblemStatus problem_status)
bool AddObjectiveConstraint(const LinearBooleanProblem &problem, bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, SatSolver *solver)
void UseObjectiveForSatAssignmentPreference(const LinearBooleanProblem &problem, SatSolver *solver)
void ConvertBooleanProblemToLinearProgram(const LinearBooleanProblem &problem, glop::LinearProgram *lp)
void FindLinearBooleanProblemSymmetries(const LinearBooleanProblem &problem, std::vector< std::unique_ptr< SparsePermutation >> *generators)
void RandomizeDecisionHeuristic(URBG *random, SatParameters *parameters)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...