28 assumptions_already_added_(false) {
30 lower_bound_ = sat::Coefficient(0);
38 if (state_update_stamp_ == problem_state.
update_stamp()) {
56 stratified_lower_bound_ = sat::Coefficient(0);
58 stratified_lower_bound_ =
std::max(stratified_lower_bound_, n->weight());
70 const std::vector<sat::Literal> assumptions =
72 stratified_lower_bound_,
73 &lower_bound_, &nodes_, &solver_);
87 CHECK(learned_info !=
nullptr);
89 learned_info->
Clear();
92 SynchronizeIfNeeded(problem_state);
97 int64_t conflict_limit =
parameters.max_number_of_conflicts_in_random_lns();
100 sat::SatParameters sat_params = solver_.
parameters();
101 sat_params.set_max_time_in_seconds(
time_limit->GetTimeLeft());
102 sat_params.set_max_deterministic_time(
104 sat_params.set_random_seed(
parameters.random_seed());
105 sat_params.set_max_number_of_conflicts(conflict_limit);
108 const int64_t old_num_conflicts = solver_.
num_failures();
110 assumptions_already_added_ ? solver_.
Solve() : SolveWithAssumptions();
112 deterministic_time_at_last_sync);
115 assumptions_already_added_ =
true;
116 conflict_limit -= solver_.
num_failures() - old_num_conflicts;
117 learned_info->
lower_bound = lower_bound_.value() - offset_.value();
131 stratified_lower_bound_ =
136 if (stratified_lower_bound_ > 0) {
137 assumptions_already_added_ =
false;
150 assumptions_already_added_ =
false;
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
const BopSolution & solution() const
const sat::LinearBooleanProblem & original_problem() const
int64_t update_stamp() const
~SatCoreBasedOptimizer() 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
SatCoreBasedOptimizer(const std::string &name)
const SatParameters & parameters() const
Status ResetAndSolveWithGivenAssumptions(const std::vector< Literal > &assumptions)
int64 num_failures() const
const VariablesAssignment & Assignment() const
void SetParameters(const SatParameters ¶meters)
std::vector< Literal > GetLastIncompatibleDecisions()
double deterministic_time() 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)
Coefficient ComputeCoreMinWeight(const std::vector< EncodingNode * > &nodes, const std::vector< Literal > &core)
std::vector< Literal > ReduceNodesAndExtractAssumptions(Coefficient upper_bound, Coefficient stratified_lower_bound, Coefficient *lower_bound, std::vector< EncodingNode * > *nodes, SatSolver *solver)
void MinimizeCore(SatSolver *solver, std::vector< Literal > *core)
void ProcessCore(const std::vector< Literal > &core, Coefficient min_weight, std::deque< EncodingNode > *repository, std::vector< EncodingNode * > *nodes, SatSolver *solver)
const Coefficient kCoefficientMax(std::numeric_limits< Coefficient::ValueType >::max())
Coefficient MaxNodeWeightSmallerThan(const std::vector< EncodingNode * > &nodes, Coefficient upper_bound)
std::vector< EncodingNode * > CreateInitialEncodingNodes(const std::vector< Literal > &literals, const std::vector< Coefficient > &coeffs, Coefficient *offset, std::deque< EncodingNode > *repository)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
#define SCOPED_TIME_STAT(stats)