29static const int kMaxLubyIndex = 30;
30static const int kMaxBoost = 30;
35bool InternalLoadStateProblemToSatSolver(
const ProblemState& problem_state,
36 sat::SatSolver* sat_solver) {
37 const bool first_time = (sat_solver->NumVariables() == 0);
39 sat_solver->SetNumVariables(
40 problem_state.original_problem().num_variables());
43 sat_solver->Backtrack(0);
47 for (VariableIndex
var(0);
var < problem_state.is_fixed().size(); ++
var) {
48 if (problem_state.is_fixed()[
var]) {
49 if (!sat_solver->AddUnitClause(
50 sat::Literal(sat::BooleanVariable(
var.value()),
51 problem_state.fixed_values()[
var]))) {
69 problem_state.original_problem(),
71 sat::Coefficient(problem_state.lower_bound()),
73 sat::Coefficient(problem_state.upper_bound() - 1), sat_solver)) {
78 sat_solver->TrackBinaryClauses(
true);
79 if (!sat_solver->AddBinaryClauses(problem_state.NewlyAddedBinaryClauses())) {
82 sat_solver->ClearNewlyAddedBinaryClauses();
90 if (InternalLoadStateProblemToSatSolver(problem_state, sat_solver)) {
101 CHECK(
nullptr != solver);
102 CHECK(
nullptr != info);
111 ? propagation_trail.
Index()
112 : solver->
Decisions().front().trail_index;
113 for (
int trail_index = 0; trail_index < root_size; ++trail_index) {
124 CHECK(solution !=
nullptr);
128 for (sat::BooleanVariable
var(0);
var < solution->
Size(); ++
var) {
131 const VariableIndex bop_var_id(
var.value());
140 : value_(initial_value), num_changes_(0) {}
146 const double factor = 1.0 + 1.0 / (num_changes_ / 2.0 + 1);
147 value_ =
std::min(1.0 - (1.0 - value_) / factor, value_ * factor);
152 const double factor = 1.0 + 1.0 / (num_changes_ / 2.0 + 1);
153 value_ =
std::max(value_ / factor, 1.0 - (1.0 - value_) * factor);
171 for (
int i = 0; i < difficulties_.size(); ++i) {
172 difficulties_[i].Reset();
178 difficulties_[luby_msb].Increase();
183 difficulties_[luby_msb].Decrease();
188 return difficulties_[luby_msb].value();
193 return luby_boost_ >= kMaxBoost;
198 luby_value_ =
sat::SUniv(luby_id_) << luby_boost_;
#define CHECK_LE(val1, val2)
AdaptiveParameterValue(double initial_value)
void SetValue(VariableIndex var, bool value)
LubyAdaptiveParameterValue(double initial_value)
double GetParameterValue() const
const BopSolution & solution() const
const std::vector< BinaryClause > & NewlyAddedBinaryClauses()
const std::vector< Decision > & Decisions() const
const Trail & LiteralTrail() const
bool IsModelUnsat() const
int CurrentDecisionLevel() const
void ClearNewlyAddedBinaryClauses()
bool VariableIsAssigned(BooleanVariable var) const
bool LiteralIsTrue(Literal literal) const
int NumberOfVariables() const
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)
bool AddObjectiveConstraint(const LinearBooleanProblem &problem, bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, 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...
int MostSignificantBitPosition64(uint64 n)
std::vector< sat::Literal > fixed_literals
std::vector< sat::BinaryClause > binary_clauses