OR-Tools  8.2
bop_lns.cc
Go to the documentation of this file.
1// Copyright 2010-2018 Google LLC
2// Licensed under the Apache License, Version 2.0 (the "License");
3// you may not use this file except in compliance with the License.
4// You may obtain a copy of the License at
5//
6// http://www.apache.org/licenses/LICENSE-2.0
7//
8// Unless required by applicable law or agreed to in writing, software
9// distributed under the License is distributed on an "AS IS" BASIS,
10// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11// See the License for the specific language governing permissions and
12// limitations under the License.
13
14#include "ortools/bop/bop_lns.h"
15
16#include <deque>
17#include <string>
18#include <vector>
19
20#include "absl/memory/memory.h"
21#include "google/protobuf/text_format.h"
30#include "ortools/util/bitset.h"
31
32namespace operations_research {
33namespace bop {
34
35using ::operations_research::glop::ColIndex;
37using ::operations_research::glop::LinearProgram;
38using ::operations_research::glop::LPSolver;
39using ::operations_research::sat::LinearBooleanConstraint;
40using ::operations_research::sat::LinearBooleanProblem;
41
42//------------------------------------------------------------------------------
43// BopCompleteLNSOptimizer
44//------------------------------------------------------------------------------
45
46namespace {
47void UseBopSolutionForSatAssignmentPreference(const BopSolution& solution,
48 sat::SatSolver* solver) {
49 for (int i = 0; i < solution.Size(); ++i) {
50 solver->SetAssignmentPreference(
51 sat::Literal(sat::BooleanVariable(i), solution.Value(VariableIndex(i))),
52 1.0);
53 }
54}
55} // namespace
56
58 const std::string& name, const BopConstraintTerms& objective_terms)
60 state_update_stamp_(ProblemState::kInitialStampValue),
61 objective_terms_(objective_terms) {}
62
64
65BopOptimizerBase::Status BopCompleteLNSOptimizer::SynchronizeIfNeeded(
66 const ProblemState& problem_state, int num_relaxed_vars) {
67 if (state_update_stamp_ == problem_state.update_stamp()) {
69 }
70 state_update_stamp_ = problem_state.update_stamp();
71
72 // Load the current problem to the solver.
73 sat_solver_ = absl::make_unique<sat::SatSolver>();
74 const BopOptimizerBase::Status status =
75 LoadStateProblemToSatSolver(problem_state, sat_solver_.get());
76 if (status != BopOptimizerBase::CONTINUE) return status;
77
78 // Add the constraint that forces the solver to look for a solution
79 // at a distance <= num_relaxed_vars from the current one. Note that not all
80 // the terms appear in this constraint.
81 //
82 // TODO(user): if the current solution didn't change, there is no need to
83 // re-run this optimizer if we already proved UNSAT.
84 std::vector<sat::LiteralWithCoeff> cst;
85 for (BopConstraintTerm term : objective_terms_) {
86 if (problem_state.solution().Value(term.var_id) && term.weight < 0) {
87 cst.push_back(sat::LiteralWithCoeff(
88 sat::Literal(sat::BooleanVariable(term.var_id.value()), false), 1.0));
89 } else if (!problem_state.solution().Value(term.var_id) &&
90 term.weight > 0) {
91 cst.push_back(sat::LiteralWithCoeff(
92 sat::Literal(sat::BooleanVariable(term.var_id.value()), true), 1.0));
93 }
94 }
95 sat_solver_->AddLinearConstraint(
96 /*use_lower_bound=*/false, sat::Coefficient(0),
97 /*use_upper_bound=*/true, sat::Coefficient(num_relaxed_vars), &cst);
98
99 if (sat_solver_->IsModelUnsat()) return BopOptimizerBase::ABORT;
100
101 // It sounds like a good idea to force the solver to find a similar solution
102 // from the current one. On another side, this is already somewhat enforced by
103 // the constraint above, so it will need more investigation.
104 UseBopSolutionForSatAssignmentPreference(problem_state.solution(),
105 sat_solver_.get());
107}
108
109bool BopCompleteLNSOptimizer::ShouldBeRun(
110 const ProblemState& problem_state) const {
111 return problem_state.solution().IsFeasible();
112}
113
114BopOptimizerBase::Status BopCompleteLNSOptimizer::Optimize(
115 const BopParameters& parameters, const ProblemState& problem_state,
116 LearnedInfo* learned_info, TimeLimit* time_limit) {
118 CHECK(learned_info != nullptr);
119 CHECK(time_limit != nullptr);
120 learned_info->Clear();
121
122 const BopOptimizerBase::Status sync_status =
123 SynchronizeIfNeeded(problem_state, parameters.num_relaxed_vars());
124 if (sync_status != BopOptimizerBase::CONTINUE) {
125 return sync_status;
126 }
127
128 CHECK(sat_solver_ != nullptr);
129 const double initial_dt = sat_solver_->deterministic_time();
130 auto advance_dt = ::absl::MakeCleanup([initial_dt, this, &time_limit]() {
131 time_limit->AdvanceDeterministicTime(sat_solver_->deterministic_time() -
132 initial_dt);
133 });
134
135 // Set the parameters for this run.
136 // TODO(user): Because of this, we actually loose the perfect continuity
137 // between runs, and the restart policy is resetted... Fix this.
138 sat::SatParameters sat_params;
139 sat_params.set_max_number_of_conflicts(
140 parameters.max_number_of_conflicts_in_random_lns());
141 sat_params.set_max_time_in_seconds(time_limit->GetTimeLeft());
142 sat_params.set_max_deterministic_time(time_limit->GetDeterministicTimeLeft());
143 sat_params.set_random_seed(parameters.random_seed());
144
145 sat_solver_->SetParameters(sat_params);
146 const sat::SatSolver::Status sat_status = sat_solver_->Solve();
147 if (sat_status == sat::SatSolver::FEASIBLE) {
148 SatAssignmentToBopSolution(sat_solver_->Assignment(),
149 &learned_info->solution);
151 }
152 if (sat_status == sat::SatSolver::LIMIT_REACHED) {
154 }
155
156 // Because of the "LNS" constraint, we can't deduce anything about the problem
157 // in this case.
159}
160
161//------------------------------------------------------------------------------
162// BopAdaptiveLNSOptimizer
163//------------------------------------------------------------------------------
164
165namespace {
166// Returns false if the limit is reached while solving the LP.
167bool UseLinearRelaxationForSatAssignmentPreference(
168 const BopParameters& parameters, const LinearBooleanProblem& problem,
169 sat::SatSolver* sat_solver, TimeLimit* time_limit) {
170 // TODO(user): Re-use the lp_model and lp_solver or build a model with only
171 // needed constraints and variables.
172 glop::LinearProgram lp_model;
174
175 // Set bounds of variables fixed by the sat_solver.
176 const sat::Trail& propagation_trail = sat_solver->LiteralTrail();
177 for (int trail_index = 0; trail_index < propagation_trail.Index();
178 ++trail_index) {
179 const sat::Literal fixed_literal = propagation_trail[trail_index];
180 const glop::Fractional value = fixed_literal.IsPositive() ? 1.0 : 0.0;
181 lp_model.SetVariableBounds(ColIndex(fixed_literal.Variable().value()),
182 value, value);
183 }
184
185 glop::LPSolver lp_solver;
186 NestedTimeLimit nested_time_limit(time_limit, time_limit->GetTimeLeft(),
187 parameters.lp_max_deterministic_time());
188 const glop::ProblemStatus lp_status =
189 lp_solver.SolveWithTimeLimit(lp_model, nested_time_limit.GetTimeLimit());
190
191 if (lp_status != glop::ProblemStatus::OPTIMAL &&
193 lp_status != glop::ProblemStatus::IMPRECISE) {
194 // We have no useful information from the LP, we will abort this LNS.
195 return false;
196 }
197
198 // Set preferences based on the solution of the relaxation.
199 for (ColIndex col(0); col < lp_solver.variable_values().size(); ++col) {
200 const double value = lp_solver.variable_values()[col];
201 sat_solver->SetAssignmentPreference(
202 sat::Literal(sat::BooleanVariable(col.value()), round(value) == 1),
203 1 - fabs(value - round(value)));
204 }
205 return true;
206}
207} // namespace
208
209// Note(user): We prefer to start with a really low difficulty as this works
210// better for large problem, and for small ones, it will be really quickly
211// increased anyway. Maybe a better appproach is to start by relaxing something
212// like 10 variables instead of having a fixed percentage.
214 const std::string& name, bool use_lp_to_guide_sat,
215 NeighborhoodGenerator* neighborhood_generator,
216 sat::SatSolver* sat_propagator)
218 use_lp_to_guide_sat_(use_lp_to_guide_sat),
219 neighborhood_generator_(neighborhood_generator),
220 sat_propagator_(sat_propagator),
221 adaptive_difficulty_(0.001) {
222 CHECK(sat_propagator != nullptr);
223}
224
226
227bool BopAdaptiveLNSOptimizer::ShouldBeRun(
228 const ProblemState& problem_state) const {
229 return problem_state.solution().IsFeasible();
230}
231
232BopOptimizerBase::Status BopAdaptiveLNSOptimizer::Optimize(
233 const BopParameters& parameters, const ProblemState& problem_state,
234 LearnedInfo* learned_info, TimeLimit* time_limit) {
236 CHECK(learned_info != nullptr);
237 CHECK(time_limit != nullptr);
238 learned_info->Clear();
239
240 // Set-up a sat_propagator_ cleanup task to catch all the exit cases.
241 const double initial_dt = sat_propagator_->deterministic_time();
242 auto sat_propagator_cleanup =
243 ::absl::MakeCleanup([initial_dt, this, &learned_info, &time_limit]() {
244 if (!sat_propagator_->IsModelUnsat()) {
245 sat_propagator_->SetAssumptionLevel(0);
246 sat_propagator_->RestoreSolverToAssumptionLevel();
247 ExtractLearnedInfoFromSatSolver(sat_propagator_, learned_info);
248 }
249 time_limit->AdvanceDeterministicTime(
250 sat_propagator_->deterministic_time() - initial_dt);
251 });
252
253 // For the SAT conflicts limit of each LNS, we follow a luby sequence times
254 // the base number of conflicts (num_conflicts_). Note that the numbers of the
255 // Luby sequence are always power of two.
256 //
257 // We dynamically change the size of the neighborhood depending on the
258 // difficulty of the problem. There is one "target" difficulty for each
259 // different numbers in the Luby sequence. Note that the initial value is
260 // reused from the last run.
261 const BopParameters& local_parameters = parameters;
262 int num_tries = 0; // TODO(user): remove? our limit is 1 by default.
263 while (!time_limit->LimitReached() &&
264 num_tries < local_parameters.num_random_lns_tries()) {
265 // Compute the target problem difficulty and generate the neighborhood.
266 adaptive_difficulty_.UpdateLuby();
267 const double difficulty = adaptive_difficulty_.GetParameterValue();
268 neighborhood_generator_->GenerateNeighborhood(problem_state, difficulty,
269 sat_propagator_);
270
271 ++num_tries;
272 VLOG(2) << num_tries << " difficulty:" << difficulty
273 << " luby:" << adaptive_difficulty_.luby_value()
274 << " fixed:" << sat_propagator_->LiteralTrail().Index() << "/"
275 << problem_state.original_problem().num_variables();
276
277 // Special case if the difficulty is too high.
278 if (!sat_propagator_->IsModelUnsat()) {
279 if (sat_propagator_->CurrentDecisionLevel() == 0) {
280 VLOG(2) << "Nothing fixed!";
281 adaptive_difficulty_.DecreaseParameter();
282 continue;
283 }
284 }
285
286 // Since everything is already set-up, we try the sat_propagator_ with
287 // a really low conflict limit. This allow to quickly skip over UNSAT
288 // cases without the costly new problem setup.
289 if (!sat_propagator_->IsModelUnsat()) {
290 sat::SatParameters params;
291 params.set_max_number_of_conflicts(
292 local_parameters.max_number_of_conflicts_for_quick_check());
293 params.set_max_time_in_seconds(time_limit->GetTimeLeft());
294 params.set_max_deterministic_time(time_limit->GetDeterministicTimeLeft());
295 params.set_random_seed(parameters.random_seed());
296 sat_propagator_->SetParameters(params);
297 sat_propagator_->SetAssumptionLevel(
298 sat_propagator_->CurrentDecisionLevel());
299
300 const sat::SatSolver::Status status = sat_propagator_->Solve();
301 if (status == sat::SatSolver::FEASIBLE) {
302 adaptive_difficulty_.IncreaseParameter();
303 SatAssignmentToBopSolution(sat_propagator_->Assignment(),
304 &learned_info->solution);
306 } else if (status == sat::SatSolver::ASSUMPTIONS_UNSAT) {
307 // Local problem is infeasible.
308 adaptive_difficulty_.IncreaseParameter();
309 continue;
310 }
311 }
312
313 // Restore to the assumption level.
314 // This is call is important since all the fixed variable in the
315 // propagator_ will be used to construct the local problem below.
316 // Note that calling RestoreSolverToAssumptionLevel() might actually prove
317 // the infeasibility. It is important to check the UNSAT status afterward.
318 if (!sat_propagator_->IsModelUnsat()) {
319 sat_propagator_->RestoreSolverToAssumptionLevel();
320 }
321
322 // Check if the problem is proved UNSAT, by previous the search or the
323 // RestoreSolverToAssumptionLevel() call above.
324 if (sat_propagator_->IsModelUnsat()) {
325 return problem_state.solution().IsFeasible()
328 }
329
330 // Construct and Solve the LNS subproblem.
331 //
332 // Note that we don't use the sat_propagator_ all the way because using a
333 // clean solver on a really small problem is usually a lot faster (even we
334 // the time to create the subproblem) that running a long solve under
335 // assumption (like we did above with a really low conflit limit).
336 const int conflict_limit =
337 adaptive_difficulty_.luby_value() *
338 parameters.max_number_of_conflicts_in_random_lns();
339
340 sat::SatParameters params;
341 params.set_max_number_of_conflicts(conflict_limit);
342 params.set_max_time_in_seconds(time_limit->GetTimeLeft());
343 params.set_max_deterministic_time(time_limit->GetDeterministicTimeLeft());
344 params.set_random_seed(parameters.random_seed());
345
346 sat::SatSolver sat_solver;
347 sat_solver.SetParameters(params);
348
349 // Starts by adding the unit clauses to fix the variables.
350 const LinearBooleanProblem& problem = problem_state.original_problem();
351 sat_solver.SetNumVariables(problem.num_variables());
352 for (int i = 0; i < sat_propagator_->LiteralTrail().Index(); ++i) {
353 CHECK(sat_solver.AddUnitClause(sat_propagator_->LiteralTrail()[i]));
354 }
355
356 // Load the rest of the problem. This will automatically create the small
357 // local subproblem using the already fixed variable.
358 //
359 // TODO(user): modify LoadStateProblemToSatSolver() so that we can call it
360 // instead and don't need to over constraint the objective below. As a
361 // bonus we will also have the learned binary clauses.
362 if (!LoadBooleanProblem(problem, &sat_solver)) {
363 // The local problem is infeasible.
364 adaptive_difficulty_.IncreaseParameter();
365 continue;
366 }
367
368 if (use_lp_to_guide_sat_) {
369 if (!UseLinearRelaxationForSatAssignmentPreference(
370 parameters, problem, &sat_solver, time_limit)) {
372 }
373 } else {
374 UseObjectiveForSatAssignmentPreference(problem, &sat_solver);
375 }
376
378 problem, sat::Coefficient(problem_state.solution().GetCost()) - 1,
379 &sat_solver)) {
380 // The local problem is infeasible.
381 adaptive_difficulty_.IncreaseParameter();
382 continue;
383 }
384
385 // Solve the local problem.
386 const sat::SatSolver::Status status = sat_solver.Solve();
387 time_limit->AdvanceDeterministicTime(sat_solver.deterministic_time());
388 if (status == sat::SatSolver::FEASIBLE) {
389 // We found a solution! abort now.
390 SatAssignmentToBopSolution(sat_solver.Assignment(),
391 &learned_info->solution);
393 }
394
395 // Adapt the difficulty.
396 if (sat_solver.num_failures() < 0.5 * conflict_limit) {
397 adaptive_difficulty_.IncreaseParameter();
398 } else if (sat_solver.num_failures() > 0.95 * conflict_limit) {
399 adaptive_difficulty_.DecreaseParameter();
400 }
401 }
402
404}
405
406//------------------------------------------------------------------------------
407// Neighborhood generators.
408//------------------------------------------------------------------------------
409
410namespace {
411
412std::vector<sat::Literal> ObjectiveVariablesAssignedToTheirLowCostValue(
413 const ProblemState& problem_state,
414 const BopConstraintTerms& objective_terms) {
415 std::vector<sat::Literal> result;
416 DCHECK(problem_state.solution().IsFeasible());
417 for (const BopConstraintTerm& term : objective_terms) {
418 if (((problem_state.solution().Value(term.var_id) && term.weight < 0) ||
419 (!problem_state.solution().Value(term.var_id) && term.weight > 0))) {
420 result.push_back(
421 sat::Literal(sat::BooleanVariable(term.var_id.value()),
422 problem_state.solution().Value(term.var_id)));
423 }
424 }
425 return result;
426}
427
428} // namespace
429
430void ObjectiveBasedNeighborhood::GenerateNeighborhood(
431 const ProblemState& problem_state, double difficulty,
432 sat::SatSolver* sat_propagator) {
433 // Generate the set of variable we may fix and randomize their order.
434 std::vector<sat::Literal> candidates =
435 ObjectiveVariablesAssignedToTheirLowCostValue(problem_state,
436 objective_terms_);
437 std::shuffle(candidates.begin(), candidates.end(), *random_);
438
439 // We will use the sat_propagator to fix some variables as long as the number
440 // of propagated variables in the solver is under our target.
441 const int num_variables = sat_propagator->NumVariables();
442 const int target = round((1.0 - difficulty) * num_variables);
443
444 sat_propagator->Backtrack(0);
445 for (const sat::Literal literal : candidates) {
446 if (sat_propagator->LiteralTrail().Index() == target) break;
447 if (sat_propagator->LiteralTrail().Index() > target) {
448 // We prefer to error on the large neighborhood side, so we backtrack the
449 // last enqueued literal.
450 sat_propagator->Backtrack(
451 std::max(0, sat_propagator->CurrentDecisionLevel() - 1));
452 break;
453 }
454 sat_propagator->EnqueueDecisionAndBacktrackOnConflict(literal);
455 if (sat_propagator->IsModelUnsat()) return;
456 }
457}
458
459void ConstraintBasedNeighborhood::GenerateNeighborhood(
460 const ProblemState& problem_state, double difficulty,
461 sat::SatSolver* sat_propagator) {
462 // Randomize the set of constraint
463 const LinearBooleanProblem& problem = problem_state.original_problem();
464 const int num_constraints = problem.constraints_size();
465 std::vector<int> ct_ids(num_constraints, 0);
466 for (int ct_id = 0; ct_id < num_constraints; ++ct_id) ct_ids[ct_id] = ct_id;
467 std::shuffle(ct_ids.begin(), ct_ids.end(), *random_);
468
469 // Mark that we want to relax all the variables of these constraints as long
470 // as the number of relaxed variable is lower than our difficulty target.
471 const int num_variables = sat_propagator->NumVariables();
472 const int target = round(difficulty * num_variables);
473 int num_relaxed = 0;
474 std::vector<bool> variable_is_relaxed(problem.num_variables(), false);
475 for (int i = 0; i < ct_ids.size(); ++i) {
476 if (num_relaxed >= target) break;
477 const LinearBooleanConstraint& constraint = problem.constraints(ct_ids[i]);
478
479 // We exclude really large constraints since they are probably note helpful
480 // in picking a nice neighborhood.
481 if (constraint.literals_size() > 0.7 * num_variables) continue;
482
483 for (int j = 0; j < constraint.literals_size(); ++j) {
484 const VariableIndex var_id(constraint.literals(j) - 1);
485 if (!variable_is_relaxed[var_id.value()]) {
486 ++num_relaxed;
487 variable_is_relaxed[var_id.value()] = true;
488 }
489 }
490 }
491
492 // Basic version: simply fix all the "to_fix" variable that are not relaxed.
493 //
494 // TODO(user): Not fixing anything that propagates a variable in
495 // variable_is_relaxed may be better. It is actually a lot better in the
496 // RelationGraphBasedNeighborhood. To investigate.
497 sat_propagator->Backtrack(0);
498 const std::vector<sat::Literal> to_fix =
499 ObjectiveVariablesAssignedToTheirLowCostValue(problem_state,
500 objective_terms_);
501 for (const sat::Literal literal : to_fix) {
502 if (variable_is_relaxed[literal.Variable().value()]) continue;
503 sat_propagator->EnqueueDecisionAndBacktrackOnConflict(literal);
504 if (sat_propagator->IsModelUnsat()) return;
505 }
506}
507
509 const LinearBooleanProblem& problem, MTRandom* random)
510 : random_(random) {
511 const int num_variables = problem.num_variables();
512 columns_.resize(num_variables);
513
514 // We will ignore constraints that have more variables than this percentage of
515 // the total number of variables in this neighborhood computation.
516 //
517 // TODO(user): Factor this out with the similar factor in
518 // ConstraintBasedNeighborhood? also maybe a better approach is to order the
519 // constraint, and stop the neighborhood extension without considering all of
520 // them.
521 const double kSizeThreshold = 0.1;
522 for (int i = 0; i < problem.constraints_size(); ++i) {
523 const LinearBooleanConstraint& constraint = problem.constraints(i);
524 if (constraint.literals_size() > kSizeThreshold * num_variables) continue;
525 for (int j = 0; j < constraint.literals_size(); ++j) {
526 const sat::Literal literal(constraint.literals(j));
527 columns_[VariableIndex(literal.Variable().value())].push_back(
528 ConstraintIndex(i));
529 }
530 }
531}
532
533void RelationGraphBasedNeighborhood::GenerateNeighborhood(
534 const ProblemState& problem_state, double difficulty,
535 sat::SatSolver* sat_propagator) {
536 // Simply walk the graph until enough variable are relaxed.
537 const int num_variables = sat_propagator->NumVariables();
538 const int target = round(difficulty * num_variables);
539 int num_relaxed = 1;
540 std::vector<bool> variable_is_relaxed(num_variables, false);
541 std::deque<int> queue;
542
543 // TODO(user): If one plan to try of lot of different LNS, maybe it will be
544 // better to try to bias the distribution of "center" to be as spread as
545 // possible.
546 queue.push_back(random_->Uniform(num_variables));
547 variable_is_relaxed[queue.back()] = true;
548 while (!queue.empty() && num_relaxed < target) {
549 const int var = queue.front();
550 queue.pop_front();
551 for (ConstraintIndex ct_index : columns_[VariableIndex(var)]) {
552 const LinearBooleanConstraint& constraint =
553 problem_state.original_problem().constraints(ct_index.value());
554 for (int i = 0; i < constraint.literals_size(); ++i) {
555 const sat::Literal literal(constraint.literals(i));
556 const int next_var = literal.Variable().value();
557 if (!variable_is_relaxed[next_var]) {
558 ++num_relaxed;
559 variable_is_relaxed[next_var] = true;
560 queue.push_back(next_var);
561 }
562 }
563 }
564 }
565
566 // Loops over all the variables in order and only fix the ones that don't
567 // propagate any relaxed variables.
568 DCHECK(problem_state.solution().IsFeasible());
569 sat_propagator->Backtrack(0);
570 for (sat::BooleanVariable var(0); var < num_variables; ++var) {
571 const sat::Literal literal(
572 var, problem_state.solution().Value(VariableIndex(var.value())));
573 if (variable_is_relaxed[literal.Variable().value()]) continue;
574 const int index =
576 if (sat_propagator->CurrentDecisionLevel() > 0) {
577 for (int i = index; i < sat_propagator->LiteralTrail().Index(); ++i) {
578 if (variable_is_relaxed
579 [sat_propagator->LiteralTrail()[i].Variable().value()]) {
580 sat_propagator->Backtrack(sat_propagator->CurrentDecisionLevel() - 1);
581 }
582 }
583 }
584 if (sat_propagator->IsModelUnsat()) return;
585 }
586 VLOG(2) << "target:" << target << " relaxed:" << num_relaxed << " actual:"
587 << num_variables - sat_propagator->LiteralTrail().Index();
588}
589
590} // namespace bop
591} // namespace operations_research
int64 max
Definition: alldiff_cst.cc:139
#define CHECK(condition)
Definition: base/logging.h:495
#define DCHECK(condition)
Definition: base/logging.h:884
#define VLOG(verboselevel)
Definition: base/logging.h:978
void resize(size_type new_size)
void push_back(const value_type &x)
uint32 Uniform(uint32 n)
Definition: random.cc:40
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
Definition: time_limit.h:105
BopAdaptiveLNSOptimizer(const std::string &name, bool use_lp_to_guide_sat, NeighborhoodGenerator *neighborhood_generator, sat::SatSolver *sat_propagator)
Definition: bop_lns.cc:213
BopCompleteLNSOptimizer(const std::string &name, const BopConstraintTerms &objective_terms)
Definition: bop_lns.cc:57
bool Value(VariableIndex var) const
Definition: bop_solution.h:46
const BopSolution & solution() const
Definition: bop_base.h:196
const sat::LinearBooleanProblem & original_problem() const
Definition: bop_base.h:201
RelationGraphBasedNeighborhood(const sat::LinearBooleanProblem &problem, MTRandom *random)
Definition: bop_lns.cc:508
const VariablesAssignment & Assignment() const
Definition: sat_solver.h:362
const Trail & LiteralTrail() const
Definition: sat_solver.h:361
void SetAssumptionLevel(int assumption_level)
Definition: sat_solver.cc:962
void SetParameters(const SatParameters &parameters)
Definition: sat_solver.cc:115
int EnqueueDecisionAndBacktrackOnConflict(Literal true_literal)
Definition: sat_solver.cc:861
void Backtrack(int target_level)
Definition: sat_solver.cc:888
SatParameters parameters
SharedTimeLimit * time_limit
const std::string name
int64 value
IntVar * var
Definition: expr_array.cc:1858
ColIndex col
Definition: markowitz.cc:176
absl::Cleanup< absl::decay_t< Callback > > MakeCleanup(Callback &&callback)
Definition: cleanup.h:120
BopOptimizerBase::Status LoadStateProblemToSatSolver(const ProblemState &problem_state, sat::SatSolver *sat_solver)
Definition: bop_util.cc:88
void SatAssignmentToBopSolution(const sat::VariablesAssignment &assignment, BopSolution *solution)
Definition: bop_util.cc:122
absl::StrongVector< SparseIndex, BopConstraintTerm > BopConstraintTerms
Definition: bop_types.h:87
StrictITIVector< ColIndex, Fractional > DenseRow
Definition: lp_types.h:299
void UseObjectiveForSatAssignmentPreference(const LinearBooleanProblem &problem, SatSolver *solver)
void ConvertBooleanProblemToLinearProgram(const LinearBooleanProblem &problem, glop::LinearProgram *lp)
bool AddObjectiveUpperBound(const LinearBooleanProblem &problem, Coefficient upper_bound, SatSolver *solver)
bool LoadBooleanProblem(const LinearBooleanProblem &problem, SatSolver *solver)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Literal literal
Definition: optimization.cc:84
int index
Definition: pack.cc:508
#define SCOPED_TIME_STAT(stats)
Definition: stats.h:438