44 std::vector<BooleanVariable> bool_vars;
45 for (BooleanVariable
b(0);
b < num_variables; ++
b) {
50 bool_vars.push_back(
b);
55bool Prober::ProbeOneVariableInternal(BooleanVariable
b) {
56 new_integer_bounds_.clear();
62 const int saved_index = trail_.
Index();
71 for (
int i = saved_index + 1; i < trail_.
Index(); ++i) {
72 const Literal l = trail_[i];
75 if (decision.IsPositive()) {
76 propagated_.
Set(l.Index());
78 if (propagated_[l.Index()]) {
79 to_fix_at_true_.push_back(l);
88 new_binary_clauses_.push_back({decision.Negated(), l});
94 for (
const Literal l : to_fix_at_true_) {
97 to_fix_at_true_.clear();
99 num_new_binary_ += new_binary_clauses_.size();
100 for (
auto binary : new_binary_clauses_) {
103 new_binary_clauses_.clear();
119 std::sort(new_integer_bounds_.begin(), new_integer_bounds_.end(),
120 [](IntegerLiteral
a, IntegerLiteral
b) { return a.var < b.var; });
126 new_integer_bounds_.push_back(IntegerLiteral());
128 for (
int i = 0; i < new_integer_bounds_.size(); ++i) {
129 const IntegerVariable
var = new_integer_bounds_[i].var;
133 if (ub_min + 1 < lb_max) {
138 const Domain old_domain =
141 Domain(ub_min.value() + 1, lb_max.value() - 1).Complement());
142 if (new_domain != old_domain) {
163 if (i == 0 || new_integer_bounds_[i - 1].
var !=
var)
continue;
164 const IntegerValue new_bound =
std::min(new_integer_bounds_[i - 1].
bound,
165 new_integer_bounds_[i].
bound);
167 ++num_new_integer_bounds_;
183 num_new_integer_bounds_ = 0;
193 return ProbeOneVariableInternal(
b);
197 absl::Span<const BooleanVariable> bool_vars,
206 num_new_integer_bounds_ = 0;
217 const double initial_deterministic_time =
219 const double limit = initial_deterministic_time + deterministic_time_limit;
221 bool limit_reached =
false;
224 for (
const BooleanVariable
b : bool_vars) {
234 limit_reached =
true;
240 if (!ProbeOneVariableInternal(
b)) {
247 const double time_diff =
250 const int num_newly_fixed = num_fixed - initial_num_fixed;
251 LOG(
INFO) <<
"Probing deterministic_time: " << time_diff
252 <<
" (limit: " << deterministic_time_limit
254 << (limit_reached ?
"Aborted " :
"") << num_probed <<
"/"
255 << bool_vars.size() <<
")";
257 <<
" - new fixed Boolean: " << num_newly_fixed <<
" (" << num_fixed
260 <<
" - new integer holes: " << num_new_holes_;
262 <<
" - new integer bounds: " << num_new_integer_bounds_;
264 <<
" - new binary clause: " << num_new_binary_;
279 if (!sat_solver->RestoreSolverToAssumptionLevel())
return false;
282 const int initial_num_fixed = sat_solver->LiteralTrail().Index();
286 SatParameters initial_params = *
model->GetOrCreate<SatParameters>();
287 SatParameters new_params = initial_params;
288 new_params.set_log_search_progress(
false);
289 new_params.set_max_number_of_conflicts(1);
290 new_params.set_max_deterministic_time(deterministic_time_limit);
292 double elapsed_dtime = 0.0;
294 const int num_times = 1000;
295 bool limit_reached =
false;
297 for (
int i = 0; i < num_times; ++i) {
299 elapsed_dtime > deterministic_time_limit) {
300 limit_reached =
true;
305 sat_solver->SetParameters(new_params);
306 sat_solver->ResetDecisionHeuristic();
308 elapsed_dtime +=
time_limit->GetElapsedDeterministicTime();
311 LOG_IF(
INFO, log_info) <<
"Trivial exploration found feasible solution!";
312 time_limit->AdvanceDeterministicTime(elapsed_dtime);
316 if (!sat_solver->RestoreSolverToAssumptionLevel()) {
317 LOG_IF(
INFO, log_info) <<
"UNSAT during trivial exploration heuristic.";
318 time_limit->AdvanceDeterministicTime(elapsed_dtime);
325 new_params.set_random_seed(i);
326 new_params.set_max_deterministic_time(deterministic_time_limit -
331 sat_solver->SetParameters(initial_params);
332 sat_solver->ResetDecisionHeuristic();
333 time_limit->AdvanceDeterministicTime(elapsed_dtime);
334 if (!sat_solver->RestoreSolverToAssumptionLevel())
return false;
337 const int num_fixed = sat_solver->LiteralTrail().Index();
338 const int num_newly_fixed = num_fixed - initial_num_fixed;
339 const int num_variables = sat_solver->NumVariables();
340 LOG(
INFO) <<
"Random exploration."
341 <<
" num_fixed: +" << num_newly_fixed <<
" (" << num_fixed <<
"/"
342 << num_variables <<
")"
343 <<
" dtime: " << elapsed_dtime <<
"/" << deterministic_time_limit
345 << (limit_reached ?
" (Aborted)" :
"");
347 return sat_solver->FinishPropagation();
358 if (!sat_solver->RestoreSolverToAssumptionLevel())
return false;
364 if (!implication_graph->DetectEquivalences())
return false;
365 if (!sat_solver->FinishPropagation())
return false;
368 const int initial_num_fixed = sat_solver->LiteralTrail().Index();
369 const double initial_deterministic_time =
373 const int num_variables = sat_solver->NumVariables();
376 int64 num_probed = 0;
377 int64 num_explicit_fix = 0;
378 int64 num_conflicts = 0;
379 int64 num_new_binary = 0;
380 int64 num_subsumed = 0;
383 const auto& assignment = trail.Assignment();
386 const int clause_id = clause_manager->PropagatorId();
389 struct SavedNextLiteral {
390 LiteralIndex literal_index;
393 bool operator<(
const SavedNextLiteral& o)
const {
return rank < o.rank; }
395 std::vector<SavedNextLiteral> queue;
404 std::vector<Literal> to_fix;
418 std::vector<LiteralIndex> probing_order =
419 implication_graph->ReverseTopologicalOrder();
421 std::reverse(probing_order.begin(), probing_order.end());
426 position_in_order.
assign(2 * num_variables, -1);
427 for (
int i = 0; i < probing_order.size(); ++i) {
428 position_in_order[probing_order[i]] = i;
433 time_limit->GetElapsedDeterministicTime() <= limit) {
438 if (options.
use_queue && sat_solver->CurrentDecisionLevel() > 0) {
443 sat_solver->Decisions()[sat_solver->CurrentDecisionLevel() - 1]
446 implication_graph->Implications(prev_decision.
Negated());
447 const int saved_queue_size = queue.size();
450 if (processed[candidate.
Index()])
continue;
451 if (position_in_order[candidate.
Index()] == -1)
continue;
452 if (assignment.LiteralIsAssigned(candidate)) {
453 if (assignment.LiteralIsFalse(candidate)) {
459 {candidate.
Index(), -position_in_order[candidate.
Index()]});
461 std::sort(queue.begin() + saved_queue_size, queue.end());
464 while (!queue.empty()) {
465 const LiteralIndex
index = queue.back().literal_index;
469 CHECK_GT(sat_solver->CurrentDecisionLevel(), 0);
470 sat_solver->Backtrack(sat_solver->CurrentDecisionLevel() - 1);
474 if (processed[candidate.
Index()])
continue;
475 if (assignment.LiteralIsAssigned(candidate)) {
476 if (assignment.LiteralIsFalse(candidate)) {
481 next_decision = candidate.
Index();
486 if (sat_solver->CurrentDecisionLevel() == 0) {
489 if (!assignment.LiteralIsTrue(
literal)) {
491 sat_solver->AddUnitClause(
literal);
495 if (!sat_solver->FinishPropagation())
return false;
498 for (; order_index < probing_order.size(); ++order_index) {
499 const Literal candidate(probing_order[order_index]);
500 if (processed[candidate.
Index()])
continue;
501 if (assignment.LiteralIsAssigned(candidate))
continue;
502 next_decision = candidate.
Index();
509 const int level = sat_solver->CurrentDecisionLevel();
510 const Literal prev_decision = sat_solver->Decisions()[level - 1].literal;
512 implication_graph->Implications(prev_decision.
Negated());
519 for (
int i = 0; i < list.size(); ++i, ++j) {
522 if (processed[candidate.
Index()])
continue;
523 if (assignment.LiteralIsFalse(candidate)) {
530 if (assignment.LiteralIsTrue(candidate))
continue;
531 next_decision = candidate.
Index();
536 sat_solver->Backtrack(level - 1);
542 processed.
Set(next_decision);
545 const int level = sat_solver->CurrentDecisionLevel();
546 const int first_new_trail_index =
547 sat_solver->EnqueueDecisionAndBackjumpOnConflict(
549 const int new_level = sat_solver->CurrentDecisionLevel();
550 sat_solver->AdvanceDeterministicTime(
time_limit);
551 if (sat_solver->IsModelUnsat())
return false;
552 if (new_level <= level) {
557 if (new_level == 0) {
560 int queue_level = level + 1;
561 while (queue_level > new_level) {
562 CHECK(!queue.empty());
584 if (sat_solver->CurrentDecisionLevel() != 0 ||
585 assignment.LiteralIsFalse(
Literal(next_decision))) {
586 to_fix.push_back(
Literal(next_decision).Negated());
593 if (new_level == 0)
continue;
595 sat_solver->Decisions()[new_level - 1].literal;
596 int num_new_subsumed = 0;
597 for (
int i = first_new_trail_index; i < trail.Index(); ++i) {
599 if (l == last_decision)
continue;
606 bool subsumed =
false;
608 trail.AssignmentType(l.
Variable()) == clause_id) {
610 if (lit == last_decision.
Negated()) {
618 implication_graph->AddBinaryClause(last_decision.
Negated(), l);
619 const int trail_index = trail.Info(l.
Variable()).trail_index;
623 clause_manager->ReasonClause(trail_index)->AsSpan()) {
624 if (lit == l) ++test;
625 if (lit == last_decision.
Negated()) ++test;
628 clause_manager->LazyDetach(clause_manager->ReasonClause(trail_index));
631 implication_graph->ChangeReason(trail_index, last_decision);
653 if (!subsumed && trail.AssignmentType(l.
Variable()) !=
id) {
655 implication_graph->AddBinaryClause(last_decision.
Negated(), l);
675 clause_manager->WatcherListOnFalse(last_decision.
Negated())) {
676 if (assignment.LiteralIsTrue(w.blocking_literal)) {
677 if (w.clause->empty())
continue;
688 if (trail.AssignmentType(w.blocking_literal.Variable()) !=
id) {
690 implication_graph->AddBinaryClause(last_decision.
Negated(),
693 const auto& info = trail.Info(w.blocking_literal.Variable());
694 if (info.level > 0) {
695 const Literal d = sat_solver->Decisions()[info.level - 1].literal;
696 if (d != w.blocking_literal) {
697 implication_graph->ChangeReason(info.trail_index, d);
703 clause_manager->LazyDetach(w.clause);
708 if (num_new_subsumed > 0) {
712 clause_manager->CleanUpWatchers();
713 num_subsumed += num_new_subsumed;
717 if (!sat_solver->ResetToLevelZero())
return false;
720 sat_solver->AddUnitClause(
literal);
723 if (!sat_solver->FinishPropagation())
return false;
726 const int num_fixed = sat_solver->LiteralTrail().
Index();
727 const int num_newly_fixed = num_fixed - initial_num_fixed;
728 const double time_diff =
729 time_limit->GetElapsedDeterministicTime() - initial_deterministic_time;
730 const bool limit_reached =
time_limit->LimitReached() ||
731 time_limit->GetElapsedDeterministicTime() > limit;
734 <<
" num_probed: " << num_probed <<
" num_fixed: +" << num_newly_fixed
735 <<
" (" << num_fixed <<
"/" << num_variables <<
")"
736 <<
" explicit_fix:" << num_explicit_fix
737 <<
" num_conflicts:" << num_conflicts
738 <<
" new_binary_clauses: " << num_new_binary
739 <<
" subsumed: " << num_subsumed <<
" dtime: " << time_diff
740 <<
" wtime: " <<
wall_timer.
Get() << (limit_reached ?
" (Aborted)" :
"");
741 return sat_solver->FinishPropagation();
#define LOG_IF(severity, condition)
#define CHECK_EQ(val1, val2)
#define CHECK_GT(val1, val2)
#define CHECK_NE(val1, val2)
void assign(size_type n, const value_type &val)
void resize(size_type new_size)
An Assignment is a variable -> domains mapping, used to report solutions to the user.
Domain IntersectionWith(const Domain &domain) const
Returns the intersection of D and domain.
void Set(IntegerType index)
void ClearAndResize(IntegerType size)
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
bool LimitReached()
Returns true when the external limit is true, or the deterministic time is over the deterministic lim...
double GetElapsedDeterministicTime() const
Returns the elapsed deterministic time since the construction of this object.
Literal RepresentativeOf(Literal l) const
void ProcessIntegerTrail(Literal first_decision)
ABSL_MUST_USE_RESULT bool Enqueue(IntegerLiteral i_lit, absl::Span< const Literal > literal_reason, absl::Span< const IntegerLiteral > integer_reason)
void AppendNewBounds(std::vector< IntegerLiteral > *output) const
IntegerValue LowerBound(IntegerVariable i) const
const Domain & InitialVariableDomain(IntegerVariable var) const
bool UpdateInitialDomain(IntegerVariable var, Domain domain)
LiteralIndex NegatedIndex() const
LiteralIndex Index() const
BooleanVariable Variable() const
Class that owns everything related to a particular optimization model.
bool ProbeOneVariable(BooleanVariable b)
bool ProbeBooleanVariables(double deterministic_time_limit, bool log_info=false)
const Trail & LiteralTrail() const
void SetAssumptionLevel(int assumption_level)
void AdvanceDeterministicTime(TimeLimit *limit)
int EnqueueDecisionAndBackjumpOnConflict(Literal true_literal)
bool AddBinaryClause(Literal a, Literal b)
bool RestoreSolverToAssumptionLevel()
bool IsModelUnsat() const
int CurrentDecisionLevel() const
bool AddUnitClause(Literal true_literal)
int AssignmentType(BooleanVariable var) const
bool LiteralIsAssigned(Literal literal) const
SharedTimeLimit * time_limit
bool VariableIsPositive(IntegerVariable i)
bool LookForTrivialSatSolution(double deterministic_time_limit, Model *model, bool log_info)
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
const LiteralIndex kNoLiteralIndex(-1)
const IntegerVariable kNoIntegerVariable(-1)
IntegerVariable PositiveVariable(IntegerVariable i)
bool FailedLiteralProbingRound(ProbingOptions options, Model *model)
void RandomizeDecisionHeuristic(URBG *random, SatParameters *parameters)
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
double deterministic_limit
bool subsume_with_binary_clause
bool extract_binary_clauses
#define VLOG_IS_ON(verboselevel)