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

minor fix in CP element; improve time limit support of CP-SAT during presolve; clean up lower bound sharing code in parallel CP-SAT

Browse Source
This commit is contained in:
Laurent Perron
2018-12-10 17:33:20 +01:00
parent 652aae5d71
commit b70c189167
12 changed files with 190 additions and 121 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
ortools/constraint_solver/element.cc
View File

@@ -338,7 +338,8 @@ class IntExprElement : public BaseIntExprElement {
}
int64 ExprMin() const override { return std::max<int64>(0, expr_->Min()); }
int64 ExprMax() const override {
return std::min<int64>(values_.size() - 1, expr_->Max());
return values_.empty() ? 0
: std::min<int64>(values_.size() - 1, expr_->Max());
}
private:

51
ortools/sat/cp_model_presolve.cc
View File

@@ -2217,14 +2217,6 @@ void ExpandObjective(PresolveContext* context) {
}
}
// Convert the objective linear expression to a map for ease of use below.
std::map<int, int64> objective_map;
for (int i = 0; i < context->working_model->objective().vars_size(); ++i) {
const int ref = context->working_model->objective().vars(i);
const int64 coeff = context->working_model->objective().coeffs(i);
objective_map[PositiveRef(ref)] = RefIsPositive(ref) ? coeff : -coeff;
}
// To avoid a bad complexity, we need to compute the number of relevant
// constraints for each variables.
const int num_variables = context->working_model->variables_size();
@@ -2248,22 +2240,39 @@ void ExpandObjective(PresolveContext* context) {
}
}
// Convert the objective linear expression to a map for ease of use below.
std::map<int, int64> objective_map;
std::set<int> var_to_process;
for (int i = 0; i < context->working_model->objective().vars_size(); ++i) {
const int ref = context->working_model->objective().vars(i);
const int64 coeff = context->working_model->objective().coeffs(i);
objective_map[PositiveRef(ref)] = RefIsPositive(ref) ? coeff : -coeff;
if (var_to_num_relevant_constraints[PositiveRef(ref)] != 0) {
var_to_process.insert(PositiveRef(ref));
}
}
// We currently never expand a variable more than once.
int num_expansions = 0;
absl::flat_hash_set<int> processed_vars;
while (!relevant_constraints.empty()) {
// Find a not yet expanded var.
int objective_var = -1;
for (const auto& entry : objective_map) {
const int var = entry.first;
if (processed_vars.count(var)) continue;
if (var_to_num_relevant_constraints[var] == 0) continue;
while (!var_to_process.empty()) {
const int var = *var_to_process.begin();
CHECK(!processed_vars.count(var));
if (var_to_num_relevant_constraints[var] == 0) {
processed_vars.insert(var);
var_to_process.erase(var);
continue;
}
objective_var = var;
break;
}
if (objective_var == -1) break;
CHECK(RefIsPositive(objective_var));
processed_vars.insert(objective_var);
var_to_process.erase(objective_var);
int expanded_linear_index = -1;
int64 objective_coeff_in_expanded_constraint;
@@ -2342,10 +2351,14 @@ void ExpandObjective(PresolveContext* context) {
if (!RefIsPositive(ref)) coeff = -coeff;
if (!gtl::ContainsKey(objective_map, var)) {
context->var_to_constraints[var].insert(-1);
if (!gtl::ContainsKey(processed_vars, var)) {
var_to_process.insert(var);
}
}
objective_map[var] += coeff;
if (objective_map[var] == 0.0) {
objective_map.erase(var);
var_to_process.erase(var);
context->var_to_constraints[var].erase(-1);
}
}
@@ -2735,7 +2748,7 @@ void RemoveUnusedEquivalentVariables(PresolveContext* context) {
// - All the variables domain will be copied to the mapping_model.
// - Everything will be remapped so that only the variables appearing in some
// constraints will be kept and their index will be in [0, num_new_variables).
void PresolveCpModel(const PresolveOptions& options,
bool PresolveCpModel(const PresolveOptions& options,
CpModelProto* presolved_model, CpModelProto* mapping_model,
std::vector<int>* postsolve_mapping) {
PresolveContext context;
@@ -2819,7 +2832,7 @@ void PresolveCpModel(const PresolveOptions& options,
// Set presolved_model to the simplest UNSAT problem (empty clause).
presolved_model->Clear();
presolved_model->add_constraints()->mutable_bool_or();
return;
return true;
}
// Regroup no-overlaps into max-cliques.
@@ -2948,8 +2961,14 @@ void PresolveCpModel(const PresolveOptions& options,
}
}
}
CHECK_EQ("", ValidateCpModel(*presolved_model));
CHECK_EQ("", ValidateCpModel(*mapping_model));
// One possible error that is difficult to avoid here: because of our
// objective expansion, we might detect a possible overflow...
//
// TODO(user): We could abort the expansion when this happen.
if (!ValidateCpModel(*presolved_model).empty()) return false;
if (!ValidateCpModel(*mapping_model).empty()) return false;
return true;
}
void ApplyVariableMapping(const std::vector<int>& mapping,

7
ortools/sat/cp_model_presolve.h
View File

@@ -50,7 +50,12 @@ struct PresolveOptions {
// TODO(user): Identify disconnected components and returns a vector of
// presolved model? If we go this route, it may be nicer to store the indices
// inside the model. We can add a IntegerVariableProto::initial_index;
void PresolveCpModel(const PresolveOptions& options,
//
// Returns false if a non-recoverable error was encountered.
//
// TODO(user): Make sure this can never run into this case provided that the
// initial model is valid!
bool PresolveCpModel(const PresolveOptions& options,
CpModelProto* presolved_model, CpModelProto* mapping_model,
std::vector<int>* postsolve_mapping);

168
ortools/sat/cp_model_solver.cc
View File

@@ -47,6 +47,7 @@
#include "ortools/port/proto_utils.h"
#include "ortools/sat/circuit.h"
#include "ortools/sat/clause.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_checker.h"
#include "ortools/sat/cp_model_expand.h"
#include "ortools/sat/cp_model_lns.h"
@@ -1150,13 +1151,13 @@ void SetSynchronizationFunction(std::function<CpSolverResponse()> f,
model->GetOrCreate<SynchronizationFunction>()->f = std::move(f);
}
void SetObjectiveSynchronizationFunctions(std::function<double()> f,
std::function<double()> g,
Model* model) {
void SetObjectiveSynchronizationFunctions(
std::function<double()> objective_best_solution,
std::function<double()> objective_best_bound, Model* model) {
ObjectiveSynchronizationHelper* helper =
model->GetOrCreate<ObjectiveSynchronizationHelper>();
helper->get_external_bound = std::move(f);
helper->get_external_best_bound = std::move(g);
helper->get_external_best_objective = std::move(objective_best_solution);
helper->get_external_best_bound = std::move(objective_best_bound);
}
#if !defined(__PORTABLE_PLATFORM__)
@@ -1185,6 +1186,63 @@ std::function<SatParameters(Model*)> NewSatParameters(
}
namespace {
void LogNewParallelSolution(const std::string& event_or_solution_count,
double time_in_seconds, double obj_lb,
double obj_ub, const std::string& solution_info) {
VLOG(1) << absl::StrFormat("#%-5s %6.2fs obj:[%0.0f,%0.0f] %s",
event_or_solution_count, time_in_seconds, obj_lb,
obj_ub, solution_info);
}
void RegisterObjectiveLowerBoundWatcher(
const CpModelProto* model_proto,
const std::function<void(const CpSolverResponse&)>&
external_solution_observer,
IntegerVariable objective_var, Model* model) {
const auto broadcast_lower_bound =
[model_proto, external_solution_observer, objective_var,
model](const std::vector<IntegerVariable>& modified_vars) {
CpSolverResponse lb_response;
lb_response.set_status(CpSolverStatus::UNKNOWN);
auto* integer_trail = model->Get<IntegerTrail>();
const ObjectiveSynchronizationHelper* const helper =
model->GetOrCreate<ObjectiveSynchronizationHelper>();
const WorkerInfo* const worker_info = model->GetOrCreate<WorkerInfo>();
const CpObjectiveProto& obj = model_proto->objective();
const double new_best_bound = ScaleObjectiveValue(
obj, integer_trail->LevelZeroLowerBound(objective_var).value());
const double current_best_bound = helper->get_external_best_bound();
const double current_objective_value =
helper->get_external_best_objective();
// TODO(user): Unit test this lambda.
if ((helper->scaling_factor >= 0 && // Unset -> = 0.0 -> minimize.
new_best_bound > current_best_bound) ||
(helper->scaling_factor < 0 &&
new_best_bound < current_best_bound)) {
DCHECK_EQ(0, lb_response.solution_size());
DCHECK_EQ(0, lb_response.solution_lower_bounds_size());
DCHECK_EQ(0, lb_response.solution_upper_bounds_size());
DCHECK_EQ(lb_response.status(), CpSolverStatus::UNKNOWN);
lb_response.set_objective_value(current_objective_value);
lb_response.set_best_objective_bound(new_best_bound);
if (current_objective_value >= new_best_bound) {
LogNewParallelSolution("ObjLb", worker_info->global_timer->Get(),
new_best_bound, current_objective_value,
worker_info->worker_name);
} else {
LogNewParallelSolution("ObjUb", worker_info->global_timer->Get(),
current_objective_value, new_best_bound,
worker_info->worker_name);
}
external_solution_observer(lb_response);
}
};
model->GetOrCreate<GenericLiteralWatcher>()
->RegisterLevelZeroModifiedVariablesCallback(broadcast_lower_bound);
}
// Because we also use this function for postsolve, we call it with
// is_real_solve set to true and avoid doing non-useful work in this case.
@@ -1414,55 +1472,9 @@ CpSolverResponse SolveCpModelInternal(
external_solution_observer(response);
};
CpSolverResponse lb_response;
response.set_status(CpSolverStatus::UNKNOWN);
if (watch_objective_lower_bound) {
const ObjectiveSynchronizationHelper* const helper =
model->GetOrCreate<ObjectiveSynchronizationHelper>();
const WorkerInfo* const worker_info = model->GetOrCreate<WorkerInfo>();
CHECK(helper != nullptr);
CHECK(worker_info != nullptr);
const auto broadcast_lower_bound =
[&model_proto, external_solution_observer, &lb_response, objective_var,
helper, worker_info, &wall_timer,
model](const std::vector<IntegerVariable>& modified_vars) {
auto* integer_trail = model->Get<IntegerTrail>();
const CpObjectiveProto& obj = model_proto.objective();
const double new_best_bound = ScaleObjectiveValue(
obj, integer_trail->LevelZeroLowerBound(objective_var).value());
const double current_best_bound = helper->get_external_best_bound();
const double current_objective_value = helper->get_external_bound();
if ((helper->scaling_factor >= 0 && // Unset -> = 0.0 -> minimize.
new_best_bound > current_best_bound) ||
(helper->scaling_factor < 0 &&
new_best_bound < current_best_bound)) {
DCHECK_EQ(0, lb_response.solution_size());
DCHECK_EQ(0, lb_response.solution_lower_bounds_size());
DCHECK_EQ(0, lb_response.solution_upper_bounds_size());
DCHECK_EQ(lb_response.status(), CpSolverStatus::UNKNOWN);
lb_response.set_objective_value(current_objective_value);
lb_response.set_best_objective_bound(new_best_bound);
if (current_objective_value >= new_best_bound) {
VLOG(1) << absl::StrFormat("#LB %6.2fs obj:[%0.0f,%0.0f] %s",
wall_timer.Get(), new_best_bound,
current_objective_value,
worker_info->worker_name);
} else {
VLOG(1) << absl::StrFormat(
"#UB %6.2fs obj:[%0.0f,%0.0f] %s",
worker_info->global_timer->Get(), current_objective_value,
new_best_bound, worker_info->worker_name);
}
external_solution_observer(lb_response);
}
};
model->GetOrCreate<GenericLiteralWatcher>()
->RegisterLevelZeroModifiedVariablesCallback(broadcast_lower_bound);
RegisterObjectiveLowerBoundWatcher(&model_proto, external_solution_observer,
objective_var, model);
}
// Load solution hint.
@@ -1630,8 +1642,8 @@ void PostsolveResponse(const CpModelProto& model_proto,
postsolve_model.Add(operations_research::sat::NewSatParameters(params));
}
const CpSolverResponse postsolve_response = SolveCpModelInternal(
mapping_proto, false, [](const CpSolverResponse&) {}, false,
&postsolve_model);
mapping_proto, false, [](const CpSolverResponse&) {},
/*watch_objective_lower_bound=*/false, &postsolve_model);
CHECK_EQ(postsolve_response.status(), CpSolverStatus::FEASIBLE);
// We only copy the solution from the postsolve_response to the response.
@@ -1833,8 +1845,9 @@ CpSolverResponse SolveCpModelWithLNS(
if (synchro != nullptr && synchro->f != nullptr) {
response = synchro->f();
} else {
response = SolveCpModelInternal(model_proto, /*is_real_solve=*/true,
observer, false, model);
response =
SolveCpModelInternal(model_proto, /*is_real_solve=*/true, observer,
/*watch_objective_lower_bound=*/false, model);
}
if (response.status() != CpSolverStatus::FEASIBLE) {
return response;
@@ -1922,7 +1935,7 @@ CpSolverResponse SolveCpModelWithLNS(
&postsolve_mapping);
local_response = SolveCpModelInternal(
local_problem, true, [](const CpSolverResponse& response) {},
false, &local_model);
/*watch_objective_lower_bound=*/false, &local_model);
PostsolveResponse(model_proto, mapping_proto, postsolve_mapping,
&local_response);
}
@@ -2046,8 +2059,8 @@ CpSolverResponse SolveCpModelParallel(
local_model.GetOrCreate<TimeLimit>()->RegisterExternalBooleanAsLimit(
stopped);
const CpSolverResponse local_response = SolveCpModelInternal(
model_proto, true, [](const CpSolverResponse& response) {}, false,
&local_model);
model_proto, true, [](const CpSolverResponse& response) {},
/*watch_objective_lower_bound=*/false, &local_model);
absl::MutexLock lock(&mutex);
if (best_response.status() == CpSolverStatus::UNKNOWN) {
@@ -2097,7 +2110,7 @@ CpSolverResponse SolveCpModelParallel(
// solution found so far.
if (MergeOptimizationSolution(r, maximize, &best_response)) {
// Checks that r is not a pure best-bound improving solution.
CHECK(r.status() == CpSolverStatus::FEASIBLE);
CHECK_EQ(r.status(), CpSolverStatus::FEASIBLE);
best_response.set_solution_info(
absl::StrCat(worker_name, " ", r.solution_info()));
@@ -2122,10 +2135,9 @@ CpSolverResponse SolveCpModelParallel(
local_model.GetOrCreate<TimeLimit>()->RegisterExternalBooleanAsLimit(
stopped);
// Stores the name of the worker in the model.
// Stores info that will be used for logs in the local model.
WorkerInfo* worker_info = local_model.GetOrCreate<WorkerInfo>();
worker_info->worker_name = worker_name;
// Stores the global timer used in logs.
worker_info->global_timer = global_timer;
SetSynchronizationFunction(std::move(solution_synchronization),
@@ -2144,7 +2156,8 @@ CpSolverResponse SolveCpModelParallel(
worker_id + random_seed, &local_model);
} else {
thread_response = SolveCpModelInternal(
model_proto, true, solution_observer, true, &local_model);
model_proto, true, solution_observer,
/*watch_objective_lower_bound=*/true, &local_model);
}
// Process final solution. Decide which worker has the 'best'
@@ -2253,7 +2266,14 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
options.log_info = VLOG_IS_ON(1);
options.parameters = *model->GetOrCreate<SatParameters>();
options.time_limit = model->GetOrCreate<TimeLimit>();
PresolveCpModel(options, &new_model, &mapping_proto, &postsolve_mapping);
const bool ok = PresolveCpModel(options, &new_model, &mapping_proto,
&postsolve_mapping);
if (!ok) {
LOG(ERROR) << "Error while presolving, likely due to integer overflow.";
CpSolverResponse response;
response.set_status(CpSolverStatus::MODEL_INVALID);
return response;
}
VLOG(1) << CpModelStats(new_model);
postprocess_solution = [&model_proto, mapping_proto,
postsolve_mapping](CpSolverResponse* response) {
@@ -2284,13 +2304,12 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
[&model_proto, &observers, &num_solutions, &timer,
&postprocess_solution](const CpSolverResponse& response) {
const bool maximize = model_proto.objective().scaling_factor() < 0.0;
VLOG(1) << absl::StrFormat("#%-5i %6.2fs obj:[%0.0f,%0.0f] %s",
++num_solutions, timer.Get(),
maximize ? response.objective_value()
: response.best_objective_bound(),
maximize ? response.best_objective_bound()
: response.objective_value(),
response.solution_info());
LogNewParallelSolution(absl::StrCat(++num_solutions), timer.Get(),
maximize ? response.objective_value()
: response.best_objective_bound(),
maximize ? response.best_objective_bound()
: response.objective_value(),
response.solution_info());
if (observers.empty()) return;
CpSolverResponse copy = response;
@@ -2325,8 +2344,9 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
response = SolveCpModelWithLNS(new_model, observer_function, 1, random_seed,
model);
} else {
response = SolveCpModelInternal(new_model, /*is_real_solve=*/true,
observer_function, false, model);
response = SolveCpModelInternal(
new_model, /*is_real_solve=*/true, observer_function,
/*watch_objective_lower_bound=*/false, model);
}
postprocess_solution(&response);

8
ortools/sat/cp_model_solver.h
View File

@@ -63,11 +63,9 @@ void SetSynchronizationFunction(std::function<CpSolverResponse()> f,
Model* model);
// Sets two funtions to query the state of the shared objective.
// - f will wait and return the best objective value.
// - g will wait and return the best objective 'best bound'.
void SetObjectiveSynchronizationFunctions(std::function<double()> f,
std::function<double()> g,
Model* model);
void SetObjectiveSynchronizationFunctions(
std::function<double()> objective_best_solution,
std::function<double()> objective_best_bound, Model* model);
// Allows to change the default parameters with
// model->Add(NewSatParameters(parameters_as_string_or_proto))

45
ortools/sat/integer.cc
View File

@@ -1267,6 +1267,7 @@ void IntegerTrail::AppendNewBounds(std::vector<IntegerLiteral>* output) const {
GenericLiteralWatcher::GenericLiteralWatcher(Model* model)
: SatPropagator("GenericLiteralWatcher"),
time_limit_(model->GetOrCreate<TimeLimit>()),
integer_trail_(model->GetOrCreate<IntegerTrail>()),
rev_int_repository_(model->GetOrCreate<RevIntRepository>()) {
// TODO(user): This propagator currently needs to be last because it is the
@@ -1325,7 +1326,19 @@ bool GenericLiteralWatcher::Propagate(Trail* trail) {
// Note that the priority may be set to -1 inside the loop in order to restart
// at zero.
int test_limit = 0;
for (int priority = 0; priority < queue_by_priority_.size(); ++priority) {
// We test the time limit from time to time. This is in order to return in
// case of slow propagation.
//
// TODO(user): The queue will not be emptied, but I am not sure the solver
// will be left in an usable state. Fix if it become needed to resume
// the solve from the last time it was interupted.
if (test_limit > 100) {
test_limit = 0;
if (time_limit_->LimitReached()) break;
}
std::deque<int>& queue = queue_by_priority_[priority];
while (!queue.empty()) {
const int id = queue.front();
@@ -1383,29 +1396,25 @@ bool GenericLiteralWatcher::Propagate(Trail* trail) {
UpdateCallingNeeds(trail);
}
// If the propagator pushed an integer bound, we revert to priority = 0.
if (integer_trail_->num_enqueues() > old_integer_timestamp) {
priority = -1; // Because of the ++priority in the for loop.
}
// If the propagator pushed a literal, we have two options.
// If the propagator pushed a literal, we exit in order to rerun all SAT
// only propagators first. Note that since a literal was pushed we are
// guaranteed to be called again, and we will resume from priority 0.
if (trail->Index() > old_boolean_timestamp) {
// Important: for now we need to re-run the clauses propagator each time
// we push a new literal because some propagator like the arc consistent
// all diff relies on this.
//
// However, on some problem, it seems to work better to not do that. One
// possible reason is that the reason of a "natural" propagation might
// be better than one we learned.
const bool run_sat_propagators_at_higher_priority = true;
if (run_sat_propagators_at_higher_priority) {
// We exit in order to rerun all SAT only propagators first. Note that
// since a literal was pushed we are guaranteed to be called again,
// and we will resume from priority 0.
return true;
} else {
priority = -1;
}
// TODO(user): However, on some problem, it seems to work better to not
// do that. One possible reason is that the reason of a "natural"
// propagation might be better than one we learned.
return true;
}
// If the propagator pushed an integer bound, we revert to priority = 0.
if (integer_trail_->num_enqueues() > old_integer_timestamp) {
++test_limit;
priority = -1; // Because of the ++priority in the for loop.
break;
}
}
}

1
ortools/sat/integer.h
View File

@@ -922,6 +922,7 @@ class GenericLiteralWatcher : public SatPropagator {
// called.
void UpdateCallingNeeds(Trail* trail);
TimeLimit* time_limit_;
IntegerTrail* integer_trail_;
RevIntRepository* rev_int_repository_;

4
ortools/sat/integer_search.cc
View File

@@ -391,7 +391,7 @@ SatSolver::Status SolveProblemWithPortfolioSearch(
model->Get<ObjectiveSynchronizationHelper>();
const bool synchronize_objective =
solver->AssumptionLevel() == 0 && helper != nullptr &&
helper->get_external_bound != nullptr &&
helper->get_external_best_objective != nullptr &&
helper->objective_var != kNoIntegerVariable;
// Note that it is important to do the level-zero propagation if it wasn't
@@ -418,7 +418,7 @@ SatSolver::Status SolveProblemWithPortfolioSearch(
// Check external objective, and restart if a better one is supplied.
// TODO(user): Maybe do not check this at each decision.
if (synchronize_objective) {
const double external_bound = helper->get_external_bound();
const double external_bound = helper->get_external_best_objective();
CHECK(helper->get_external_best_bound != nullptr);
const double external_best_bound = helper->get_external_best_bound();
IntegerTrail* const integer_trail = model->GetOrCreate<IntegerTrail>();

2
ortools/sat/integer_search.h
View File

@@ -113,7 +113,7 @@ struct ObjectiveSynchronizationHelper {
double scaling_factor = 1.0;
double offset = 0.0;
IntegerVariable objective_var = kNoIntegerVariable;
std::function<double()> get_external_bound = nullptr;
std::function<double()> get_external_best_objective = nullptr;
std::function<double()> get_external_best_bound = nullptr;
int64 UnscaledObjective(double value) const {

4
ortools/sat/linear_programming_constraint.cc
View File

@@ -48,7 +48,9 @@ LinearProgrammingConstraint::LinearProgrammingConstraint(Model* model)
trail_(model->GetOrCreate<Trail>()),
model_heuristics_(model->GetOrCreate<SearchHeuristicsVector>()),
integer_encoder_(model->GetOrCreate<IntegerEncoder>()),
dispatcher_(model->GetOrCreate<LinearProgrammingDispatcher>()) {
dispatcher_(model->GetOrCreate<LinearProgrammingDispatcher>()),
expanded_lp_solution_(
*model->GetOrCreate<LinearProgrammingConstraintLpSolution>()) {
// Tweak the default parameters to make the solve incremental.
glop::GlopParameters parameters;
parameters.set_use_dual_simplex(true);

15
ortools/sat/linear_programming_constraint.h
View File

@@ -34,6 +34,19 @@
namespace operations_research {
namespace sat {
// Stores for each IntegerVariable its temporary LP solution.
//
// This is shared between all LinearProgrammingConstraint because in the corner
// case where we have many different LinearProgrammingConstraint and a lot of
// variable, we could theoretically use up a quadratic amount of memory
// otherwise.
//
// TODO(user): find a better way?
struct LinearProgrammingConstraintLpSolution
: public gtl::ITIVector<IntegerVariable, double> {
LinearProgrammingConstraintLpSolution() {}
};
// A SAT constraint that enforces a set of linear inequality constraints on
// integer variables using an LP solver.
//
@@ -287,7 +300,7 @@ class LinearProgrammingConstraint : public PropagatorInterface,
std::vector<double> level_zero_lp_solution_;
// Same as lp_solution_ but this vector is indexed differently.
gtl::ITIVector<IntegerVariable, double> expanded_lp_solution_;
LinearProgrammingConstraintLpSolution& expanded_lp_solution_;
// Linear constraints cannot be created or modified after this is registered.
bool lp_constraint_is_registered_ = false;

3
ortools/sat/sat_solver.cc
View File

@@ -2153,7 +2153,8 @@ void SatSolver::MinimizeConflictRecursively(std::vector<Literal>* conflict) {
int index = 1;
for (int i = 1; i < conflict->size(); ++i) {
const BooleanVariable var = (*conflict)[i].Variable();
if (trail_->Info(var).trail_index <=
if (time_limit_->LimitReached() ||
trail_->Info(var).trail_index <=
min_trail_index_per_level_[DecisionLevel(var)] ||
!CanBeInferedFromConflictVariables(var)) {
// Mark the conflict variable as independent. Note that is_marked_[var]