OR-Tools  8.2
probing.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/sat/probing.h"
15
16#include <set>
17
20#include "ortools/base/timer.h"
21#include "ortools/sat/clause.h"
23#include "ortools/sat/integer.h"
26#include "ortools/sat/util.h"
28
29namespace operations_research {
30namespace sat {
31
33 : trail_(*model->GetOrCreate<Trail>()),
34 assignment_(model->GetOrCreate<SatSolver>()->Assignment()),
35 integer_trail_(model->GetOrCreate<IntegerTrail>()),
36 implied_bounds_(model->GetOrCreate<ImpliedBounds>()),
37 sat_solver_(model->GetOrCreate<SatSolver>()),
38 time_limit_(model->GetOrCreate<TimeLimit>()),
39 implication_graph_(model->GetOrCreate<BinaryImplicationGraph>()) {}
40
41bool Prober::ProbeBooleanVariables(const double deterministic_time_limit,
42 bool log_info) {
43 const int num_variables = sat_solver_->NumVariables();
44 std::vector<BooleanVariable> bool_vars;
45 for (BooleanVariable b(0); b < num_variables; ++b) {
46 const Literal literal(b, true);
47 if (implication_graph_->RepresentativeOf(literal) != literal) {
48 continue;
49 }
50 bool_vars.push_back(b);
51 }
52 return ProbeBooleanVariables(deterministic_time_limit, bool_vars, log_info);
53}
54
55bool Prober::ProbeOneVariableInternal(BooleanVariable b) {
56 new_integer_bounds_.clear();
57 propagated_.SparseClearAll();
58 for (const Literal decision : {Literal(b, true), Literal(b, false)}) {
59 if (assignment_.LiteralIsAssigned(decision)) continue;
60
61 CHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0);
62 const int saved_index = trail_.Index();
63 sat_solver_->EnqueueDecisionAndBackjumpOnConflict(decision);
64 sat_solver_->AdvanceDeterministicTime(time_limit_);
65
66 if (sat_solver_->IsModelUnsat()) return false;
67 if (sat_solver_->CurrentDecisionLevel() == 0) continue;
68
69 implied_bounds_->ProcessIntegerTrail(decision);
70 integer_trail_->AppendNewBounds(&new_integer_bounds_);
71 for (int i = saved_index + 1; i < trail_.Index(); ++i) {
72 const Literal l = trail_[i];
73
74 // We mark on the first run (b.IsPositive()) and check on the second.
75 if (decision.IsPositive()) {
76 propagated_.Set(l.Index());
77 } else {
78 if (propagated_[l.Index()]) {
79 to_fix_at_true_.push_back(l);
80 }
81 }
82
83 // Anything not propagated by the BinaryImplicationGraph is a "new"
84 // binary clause. This is becaue the BinaryImplicationGraph has the
85 // highest priority of all propagators.
86 if (trail_.AssignmentType(l.Variable()) !=
87 implication_graph_->PropagatorId()) {
88 new_binary_clauses_.push_back({decision.Negated(), l});
89 }
90 }
91
92 // Fix variable and add new binary clauses.
93 if (!sat_solver_->RestoreSolverToAssumptionLevel()) return false;
94 for (const Literal l : to_fix_at_true_) {
95 sat_solver_->AddUnitClause(l);
96 }
97 to_fix_at_true_.clear();
98 if (!sat_solver_->FinishPropagation()) return false;
99 num_new_binary_ += new_binary_clauses_.size();
100 for (auto binary : new_binary_clauses_) {
101 sat_solver_->AddBinaryClause(binary.first, binary.second);
102 }
103 new_binary_clauses_.clear();
104 if (!sat_solver_->FinishPropagation()) return false;
105 }
106
107 // We have at most two lower bounds for each variables (one for b==0 and one
108 // for b==1), so the min of the two is a valid level zero bound! More
109 // generally, the domain of a variable can be intersected with the union
110 // of the two propagated domains. This also allow to detect "holes".
111 //
112 // TODO(user): More generally, for any clauses (b or not(b) is one), we
113 // could probe all the literal inside, and for any integer variable, we can
114 // take the union of the propagated domain as a new domain.
115 //
116 // TODO(user): fix binary variable in the same way? It might not be as
117 // useful since probing on such variable will also fix it. But then we might
118 // abort probing early, so it might still be good.
119 std::sort(new_integer_bounds_.begin(), new_integer_bounds_.end(),
120 [](IntegerLiteral a, IntegerLiteral b) { return a.var < b.var; });
121
122 // This is used for the hole detection.
123 IntegerVariable prev_var = kNoIntegerVariable;
124 IntegerValue lb_max = kMinIntegerValue;
125 IntegerValue ub_min = kMaxIntegerValue;
126 new_integer_bounds_.push_back(IntegerLiteral()); // Sentinel.
127
128 for (int i = 0; i < new_integer_bounds_.size(); ++i) {
129 const IntegerVariable var = new_integer_bounds_[i].var;
130
131 // Hole detection.
132 if (i > 0 && PositiveVariable(var) != prev_var) {
133 if (ub_min + 1 < lb_max) {
134 // The variable cannot take value in (ub_min, lb_max) !
135 //
136 // TODO(user): do not create domain with a complexity that is too
137 // large?
138 const Domain old_domain =
139 integer_trail_->InitialVariableDomain(prev_var);
140 const Domain new_domain = old_domain.IntersectionWith(
141 Domain(ub_min.value() + 1, lb_max.value() - 1).Complement());
142 if (new_domain != old_domain) {
143 ++num_new_holes_;
144 if (!integer_trail_->UpdateInitialDomain(prev_var, new_domain)) {
145 return false;
146 }
147 }
148 }
149
150 // Reinitialize.
151 lb_max = kMinIntegerValue;
152 ub_min = kMaxIntegerValue;
153 }
154
155 prev_var = PositiveVariable(var);
156 if (VariableIsPositive(var)) {
157 lb_max = std::max(lb_max, new_integer_bounds_[i].bound);
158 } else {
159 ub_min = std::min(ub_min, -new_integer_bounds_[i].bound);
160 }
161
162 // Bound tightening.
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);
166 if (new_bound > integer_trail_->LowerBound(var)) {
167 ++num_new_integer_bounds_;
168 if (!integer_trail_->Enqueue(
169 IntegerLiteral::GreaterOrEqual(var, new_bound), {}, {})) {
170 return false;
171 }
172 }
173 }
174
175 // We might have updated some integer domain, let's propagate.
176 return sat_solver_->FinishPropagation();
177}
178
179bool Prober::ProbeOneVariable(BooleanVariable b) {
180 // Reset statistics.
181 num_new_binary_ = 0;
182 num_new_holes_ = 0;
183 num_new_integer_bounds_ = 0;
184
185 // Resize the propagated sparse bitset.
186 const int num_variables = sat_solver_->NumVariables();
187 propagated_.ClearAndResize(LiteralIndex(2 * num_variables));
188
189 // Reset the solver in case it was already used.
190 sat_solver_->SetAssumptionLevel(0);
191 if (!sat_solver_->RestoreSolverToAssumptionLevel()) return false;
192
193 return ProbeOneVariableInternal(b);
194}
195
196bool Prober::ProbeBooleanVariables(const double deterministic_time_limit,
197 absl::Span<const BooleanVariable> bool_vars,
198 bool log_info) {
199 log_info |= VLOG_IS_ON(1);
202
203 // Reset statistics.
204 num_new_binary_ = 0;
205 num_new_holes_ = 0;
206 num_new_integer_bounds_ = 0;
207
208 // Resize the propagated sparse bitset.
209 const int num_variables = sat_solver_->NumVariables();
210 propagated_.ClearAndResize(LiteralIndex(2 * num_variables));
211
212 // Reset the solver in case it was already used.
213 sat_solver_->SetAssumptionLevel(0);
214 if (!sat_solver_->RestoreSolverToAssumptionLevel()) return false;
215
216 const int initial_num_fixed = sat_solver_->LiteralTrail().Index();
217 const double initial_deterministic_time =
218 time_limit_->GetElapsedDeterministicTime();
219 const double limit = initial_deterministic_time + deterministic_time_limit;
220
221 bool limit_reached = false;
222 int num_probed = 0;
223
224 for (const BooleanVariable b : bool_vars) {
225 const Literal literal(b, true);
226 if (implication_graph_->RepresentativeOf(literal) != literal) {
227 continue;
228 }
229
230 // TODO(user): Instead of an hard deterministic limit, we should probably
231 // use a lower one, but reset it each time we have found something useful.
232 if (time_limit_->LimitReached() ||
233 time_limit_->GetElapsedDeterministicTime() > limit) {
234 limit_reached = true;
235 break;
236 }
237
238 // Propagate b=1 and then b=0.
239 ++num_probed;
240 if (!ProbeOneVariableInternal(b)) {
241 return false;
242 }
243 }
244
245 // Display stats.
246 if (log_info) {
247 const double time_diff =
248 time_limit_->GetElapsedDeterministicTime() - initial_deterministic_time;
249 const int num_fixed = sat_solver_->LiteralTrail().Index();
250 const int num_newly_fixed = num_fixed - initial_num_fixed;
251 LOG(INFO) << "Probing deterministic_time: " << time_diff
252 << " (limit: " << deterministic_time_limit
253 << ") wall_time: " << wall_timer.Get() << " ("
254 << (limit_reached ? "Aborted " : "") << num_probed << "/"
255 << bool_vars.size() << ")";
256 LOG_IF(INFO, num_newly_fixed > 0)
257 << " - new fixed Boolean: " << num_newly_fixed << " (" << num_fixed
258 << "/" << sat_solver_->NumVariables() << ")";
259 LOG_IF(INFO, num_new_holes_ > 0)
260 << " - new integer holes: " << num_new_holes_;
261 LOG_IF(INFO, num_new_integer_bounds_ > 0)
262 << " - new integer bounds: " << num_new_integer_bounds_;
263 LOG_IF(INFO, num_new_binary_ > 0)
264 << " - new binary clause: " << num_new_binary_;
265 }
266
267 return true;
268}
269
270bool LookForTrivialSatSolution(double deterministic_time_limit, Model* model,
271 bool log_info) {
272 log_info |= VLOG_IS_ON(1);
275
276 // Reset the solver in case it was already used.
277 auto* sat_solver = model->GetOrCreate<SatSolver>();
278 sat_solver->SetAssumptionLevel(0);
279 if (!sat_solver->RestoreSolverToAssumptionLevel()) return false;
280
281 auto* time_limit = model->GetOrCreate<TimeLimit>();
282 const int initial_num_fixed = sat_solver->LiteralTrail().Index();
283
284 // Note that this code do not care about the non-Boolean part and just try to
285 // assign the existing Booleans.
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);
291
292 double elapsed_dtime = 0.0;
293
294 const int num_times = 1000;
295 bool limit_reached = false;
296 auto* random = model->GetOrCreate<ModelRandomGenerator>();
297 for (int i = 0; i < num_times; ++i) {
298 if (time_limit->LimitReached() ||
299 elapsed_dtime > deterministic_time_limit) {
300 limit_reached = true;
301 break;
302 }
303
304 // SetParameters() reset the deterministic time to zero inside time_limit.
305 sat_solver->SetParameters(new_params);
306 sat_solver->ResetDecisionHeuristic();
307 const SatSolver::Status result = sat_solver->SolveWithTimeLimit(time_limit);
308 elapsed_dtime += time_limit->GetElapsedDeterministicTime();
309
310 if (result == SatSolver::FEASIBLE) {
311 LOG_IF(INFO, log_info) << "Trivial exploration found feasible solution!";
312 time_limit->AdvanceDeterministicTime(elapsed_dtime);
313 return true;
314 }
315
316 if (!sat_solver->RestoreSolverToAssumptionLevel()) {
317 LOG_IF(INFO, log_info) << "UNSAT during trivial exploration heuristic.";
318 time_limit->AdvanceDeterministicTime(elapsed_dtime);
319 return false;
320 }
321
322 // We randomize at the end so that the default params is executed
323 // at least once.
324 RandomizeDecisionHeuristic(random, &new_params);
325 new_params.set_random_seed(i);
326 new_params.set_max_deterministic_time(deterministic_time_limit -
327 elapsed_dtime);
328 }
329
330 // Restore the initial parameters.
331 sat_solver->SetParameters(initial_params);
332 sat_solver->ResetDecisionHeuristic();
333 time_limit->AdvanceDeterministicTime(elapsed_dtime);
334 if (!sat_solver->RestoreSolverToAssumptionLevel()) return false;
335
336 if (log_info) {
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
344 << " wtime: " << wall_timer.Get()
345 << (limit_reached ? " (Aborted)" : "");
346 }
347 return sat_solver->FinishPropagation();
348}
349
353 options.log_info |= VLOG_IS_ON(1);
354
355 // Reset the solver in case it was already used.
356 auto* sat_solver = model->GetOrCreate<SatSolver>();
357 sat_solver->SetAssumptionLevel(0);
358 if (!sat_solver->RestoreSolverToAssumptionLevel()) return false;
359
360 // When called from Inprocessing, the implication graph should already be a
361 // DAG, so these two calls should return right away. But we do need them to
362 // get the topological order if this is used in isolation.
363 auto* implication_graph = model->GetOrCreate<BinaryImplicationGraph>();
364 if (!implication_graph->DetectEquivalences()) return false;
365 if (!sat_solver->FinishPropagation()) return false;
366
367 auto* time_limit = model->GetOrCreate<TimeLimit>();
368 const int initial_num_fixed = sat_solver->LiteralTrail().Index();
369 const double initial_deterministic_time =
370 time_limit->GetElapsedDeterministicTime();
371 const double limit = initial_deterministic_time + options.deterministic_limit;
372
373 const int num_variables = sat_solver->NumVariables();
374 SparseBitset<LiteralIndex> processed(LiteralIndex(2 * num_variables));
375
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;
381
382 const auto& trail = *(model->Get<Trail>());
383 const auto& assignment = trail.Assignment();
384 auto* clause_manager = model->GetOrCreate<LiteralWatchers>();
385 const int id = implication_graph->PropagatorId();
386 const int clause_id = clause_manager->PropagatorId();
387
388 // This is only needed when options.use_queue is true.
389 struct SavedNextLiteral {
390 LiteralIndex literal_index; // kNoLiteralIndex if we need to backtrack.
391 int rank; // Cached position_in_order, we prefer lower positions.
392
393 bool operator<(const SavedNextLiteral& o) const { return rank < o.rank; }
394 };
395 std::vector<SavedNextLiteral> queue;
397
398 // This is only needed when options use_queue is false;
400 if (!options.use_queue) starts.resize(2 * num_variables, 0);
401
402 // We delay fixing of already assigned literal once we go back to level
403 // zero.
404 std::vector<Literal> to_fix;
405
406 // Depending on the options. we do not use the same order.
407 // With tree look, it is better to start with "leaf" first since we try
408 // to reuse propagation as much as possible. This is also interesting to
409 // do when extracting binary clauses since we will need to propagate
410 // everyone anyway, and this should result in less clauses that can be
411 // removed later by transitive reduction.
412 //
413 // However, without tree-look and without the need to extract all binary
414 // clauses, it is better to just probe the root of the binary implication
415 // graph. This is exactly what happen when we probe using the topological
416 // order.
417 int order_index(0);
418 std::vector<LiteralIndex> probing_order =
419 implication_graph->ReverseTopologicalOrder();
420 if (!options.use_tree_look && !options.extract_binary_clauses) {
421 std::reverse(probing_order.begin(), probing_order.end());
422 }
423
424 // We only use this for the queue version.
425 if (options.use_queue) {
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;
429 }
430 }
431
432 while (!time_limit->LimitReached() &&
433 time_limit->GetElapsedDeterministicTime() <= limit) {
434 // We only enqueue literal at level zero if we don't use "tree look".
435 if (!options.use_tree_look) sat_solver->Backtrack(0);
436
437 LiteralIndex next_decision = kNoLiteralIndex;
438 if (options.use_queue && sat_solver->CurrentDecisionLevel() > 0) {
439 // TODO(user): Instead of minimizing index in topo order (which might be
440 // nice for binary extraction), we could try to maximize reusability in
441 // some way.
442 const Literal prev_decision =
443 sat_solver->Decisions()[sat_solver->CurrentDecisionLevel() - 1]
444 .literal;
445 const auto& list =
446 implication_graph->Implications(prev_decision.Negated());
447 const int saved_queue_size = queue.size();
448 for (const Literal l : list) {
449 const Literal candidate = l.Negated();
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)) {
454 to_fix.push_back(Literal(candidate.Negated()));
455 }
456 continue;
457 }
458 queue.push_back(
459 {candidate.Index(), -position_in_order[candidate.Index()]});
460 }
461 std::sort(queue.begin() + saved_queue_size, queue.end());
462
463 // Probe a literal that implies previous decision.
464 while (!queue.empty()) {
465 const LiteralIndex index = queue.back().literal_index;
466 queue.pop_back();
467 if (index == kNoLiteralIndex) {
468 // This is a backtrack marker, go back one level.
469 CHECK_GT(sat_solver->CurrentDecisionLevel(), 0);
470 sat_solver->Backtrack(sat_solver->CurrentDecisionLevel() - 1);
471 continue;
472 }
473 const Literal candidate(index);
474 if (processed[candidate.Index()]) continue;
475 if (assignment.LiteralIsAssigned(candidate)) {
476 if (assignment.LiteralIsFalse(candidate)) {
477 to_fix.push_back(Literal(candidate.Negated()));
478 }
479 continue;
480 }
481 next_decision = candidate.Index();
482 break;
483 }
484 }
485
486 if (sat_solver->CurrentDecisionLevel() == 0) {
487 // Fix any delayed fixed literal.
488 for (const Literal literal : to_fix) {
489 if (!assignment.LiteralIsTrue(literal)) {
490 ++num_explicit_fix;
491 sat_solver->AddUnitClause(literal);
492 }
493 }
494 to_fix.clear();
495 if (!sat_solver->FinishPropagation()) return false;
496
497 // Probe an unexplored node.
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();
503 break;
504 }
505
506 // The pass is finished.
507 if (next_decision == kNoLiteralIndex) break;
508 } else if (next_decision == kNoLiteralIndex) {
509 const int level = sat_solver->CurrentDecisionLevel();
510 const Literal prev_decision = sat_solver->Decisions()[level - 1].literal;
511 const auto& list =
512 implication_graph->Implications(prev_decision.Negated());
513
514 // Probe a literal that implies previous decision.
515 //
516 // Note that contrary to the queue based implementation, this do not
517 // process them in a particular order.
518 int j = starts[prev_decision.NegatedIndex()];
519 for (int i = 0; i < list.size(); ++i, ++j) {
520 j %= list.size();
521 const Literal candidate = Literal(list[j]).Negated();
522 if (processed[candidate.Index()]) continue;
523 if (assignment.LiteralIsFalse(candidate)) {
524 // candidate => previous => not(candidate), so we can fix it.
525 to_fix.push_back(Literal(candidate.Negated()));
526 continue;
527 }
528 // This shouldn't happen if extract_binary_clauses is false.
529 // We have an equivalence.
530 if (assignment.LiteralIsTrue(candidate)) continue;
531 next_decision = candidate.Index();
532 break;
533 }
534 starts[prev_decision.NegatedIndex()] = j;
535 if (next_decision == kNoLiteralIndex) {
536 sat_solver->Backtrack(level - 1);
537 continue;
538 }
539 }
540
541 ++num_probed;
542 processed.Set(next_decision);
543 CHECK_NE(next_decision, kNoLiteralIndex);
544 queue.push_back({kNoLiteralIndex, 0}); // Backtrack marker.
545 const int level = sat_solver->CurrentDecisionLevel();
546 const int first_new_trail_index =
547 sat_solver->EnqueueDecisionAndBackjumpOnConflict(
548 Literal(next_decision));
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) {
553 ++num_conflicts;
554
555 // Sync the queue with the new level.
556 if (options.use_queue) {
557 if (new_level == 0) {
558 queue.clear();
559 } else {
560 int queue_level = level + 1;
561 while (queue_level > new_level) {
562 CHECK(!queue.empty());
563 if (queue.back().literal_index == kNoLiteralIndex) --queue_level;
564 queue.pop_back();
565 }
566 }
567 }
568
569 // Fix next_decision to false if not already done.
570 //
571 // Even if we fixed something at evel zero, next_decision might not be
572 // fixed! But we can fix it. It can happen because when we propagate
573 // with clauses, we might have a => b but not not(b) => not(a). Like a
574 // => b and clause (not(a), not(b), c), propagating a will set c, but
575 // propagating not(c) will not do anything.
576 //
577 // We "delay" the fixing if we are not at level zero so that we can
578 // still reuse the current propagation work via tree look.
579 //
580 // TODO(user): Can we be smarter here? Maybe we can still fix the
581 // literal without going back to level zero by simply enqueing it with
582 // no reason? it will be bactracked over, but we will still lazily fix
583 // it later.
584 if (sat_solver->CurrentDecisionLevel() != 0 ||
585 assignment.LiteralIsFalse(Literal(next_decision))) {
586 to_fix.push_back(Literal(next_decision).Negated());
587 }
588 }
589
590 // Inspect the newly propagated literals. Depending on the options, try to
591 // extract binary clauses via hyper binary resolution and/or mark the
592 // literals on the trail so that they do not need to be probed later.
593 if (new_level == 0) continue;
594 const Literal last_decision =
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) {
598 const Literal l = trail[i];
599 if (l == last_decision) continue;
600
601 // If we can extract a binary clause that subsume the reason clause, we
602 // do add the binary and remove the subsumed clause.
603 //
604 // TODO(user): We could be slightly more generic and subsume some
605 // clauses that do not contains last_decision.Negated().
606 bool subsumed = false;
607 if (options.subsume_with_binary_clause &&
608 trail.AssignmentType(l.Variable()) == clause_id) {
609 for (const Literal lit : trail.Reason(l.Variable())) {
610 if (lit == last_decision.Negated()) {
611 subsumed = true;
612 break;
613 }
614 }
615 if (subsumed) {
616 ++num_new_subsumed;
617 ++num_new_binary;
618 implication_graph->AddBinaryClause(last_decision.Negated(), l);
619 const int trail_index = trail.Info(l.Variable()).trail_index;
620
621 int test = 0;
622 for (const Literal lit :
623 clause_manager->ReasonClause(trail_index)->AsSpan()) {
624 if (lit == l) ++test;
625 if (lit == last_decision.Negated()) ++test;
626 }
627 CHECK_EQ(test, 2);
628 clause_manager->LazyDetach(clause_manager->ReasonClause(trail_index));
629
630 // We need to change the reason now that the clause is cleared.
631 implication_graph->ChangeReason(trail_index, last_decision);
632 }
633 }
634
635 if (options.extract_binary_clauses) {
636 // Anything not propagated by the BinaryImplicationGraph is a "new"
637 // binary clause. This is because the BinaryImplicationGraph has the
638 // highest priority of all propagators.
639 //
640 // Note(user): This is not 100% true, since when we launch the clause
641 // propagation for one literal we do finish it before calling again
642 // the binary propagation.
643 //
644 // TODO(user): Think about trying to extract clause that will not
645 // get removed by transitive reduction later. If we can both extract
646 // a => c and b => c , ideally we don't want to extract a => c first
647 // if we already know that a => b.
648 //
649 // TODO(user): Similar to previous point, we could find the LCA
650 // of all literals in the reason for this propagation. And use this
651 // as a reason for later hyber binary resolution. Like we do when
652 // this clause subsume the reason.
653 if (!subsumed && trail.AssignmentType(l.Variable()) != id) {
654 ++num_new_binary;
655 implication_graph->AddBinaryClause(last_decision.Negated(), l);
656 }
657 } else {
658 // If we don't extract binary, we don't need to explore any of
659 // these literal until more variables are fixed.
660 processed.Set(l.Index());
661 }
662 }
663
664 // Inspect the watcher list for last_decision, If we have a blocking
665 // literal at true (implied by last decision), then we have subsumptions.
666 //
667 // The intuition behind this is that if a binary clause (a,b) subsume a
668 // clause, and we watch a.Negated() for this clause with a blocking
669 // literal b, then this watch entry will never change because we always
670 // propagate binary clauses first and the blocking literal will always be
671 // true. So after many propagations, we hope to have such configuration
672 // which is quite cheap to test here.
673 if (options.subsume_with_binary_clause) {
674 for (const auto& w :
675 clause_manager->WatcherListOnFalse(last_decision.Negated())) {
676 if (assignment.LiteralIsTrue(w.blocking_literal)) {
677 if (w.clause->empty()) continue;
678 CHECK_NE(w.blocking_literal, last_decision.Negated());
679
680 // Add the binary clause if needed. Note that we change the reason
681 // to a binary one so that we never add the same clause twice.
682 //
683 // Tricky: while last_decision would be a valid reason, we need a
684 // reason that was assigned before this literal, so we use the
685 // decision at the level where this literal was assigne which is an
686 // even better reasony. Maybe it is just better to change all the
687 // reason above to a binary one so we don't have an issue here.
688 if (trail.AssignmentType(w.blocking_literal.Variable()) != id) {
689 ++num_new_binary;
690 implication_graph->AddBinaryClause(last_decision.Negated(),
691 w.blocking_literal);
692
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);
698 }
699 }
700 }
701
702 ++num_new_subsumed;
703 clause_manager->LazyDetach(w.clause);
704 }
705 }
706 }
707
708 if (num_new_subsumed > 0) {
709 // TODO(user): We might just want to do that even more lazily by
710 // checking for detached clause while propagating here? and do a big
711 // cleanup at the end.
712 clause_manager->CleanUpWatchers();
713 num_subsumed += num_new_subsumed;
714 }
715 }
716
717 if (!sat_solver->ResetToLevelZero()) return false;
718 for (const Literal literal : to_fix) {
719 ++num_explicit_fix;
720 sat_solver->AddUnitClause(literal);
721 }
722 to_fix.clear();
723 if (!sat_solver->FinishPropagation()) return false;
724
725 // Display stats.
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;
732 LOG_IF(INFO, options.log_info)
733 << "Probing. "
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();
742}
743
744} // namespace sat
745} // namespace operations_research
int64 min
Definition: alldiff_cst.cc:138
int64 max
Definition: alldiff_cst.cc:139
#define LOG_IF(severity, condition)
Definition: base/logging.h:479
#define CHECK(condition)
Definition: base/logging.h:495
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
#define CHECK_GT(val1, val2)
Definition: base/logging.h:702
#define CHECK_NE(val1, val2)
Definition: base/logging.h:698
#define LOG(severity)
Definition: base/logging.h:420
void Start()
Definition: timer.h:31
double Get() const
Definition: timer.h:45
void assign(size_type n, const value_type &val)
void resize(size_type new_size)
size_type size() const
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)
Definition: bitset.h:803
void ClearAndResize(IntegerType size)
Definition: bitset.h:778
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
Definition: time_limit.h:105
bool LimitReached()
Returns true when the external limit is true, or the deterministic time is over the deterministic lim...
Definition: time_limit.h:532
double GetElapsedDeterministicTime() const
Returns the elapsed deterministic time since the construction of this object.
Definition: time_limit.h:260
Literal RepresentativeOf(Literal l) const
Definition: clause.h:561
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)
Definition: integer.cc:989
void AppendNewBounds(std::vector< IntegerLiteral > *output) const
Definition: integer.cc:1728
IntegerValue LowerBound(IntegerVariable i) const
Definition: integer.h:1300
const Domain & InitialVariableDomain(IntegerVariable var) const
Definition: integer.cc:644
bool UpdateInitialDomain(IntegerVariable var, Domain domain)
Definition: integer.cc:648
LiteralIndex NegatedIndex() const
Definition: sat_base.h:85
LiteralIndex Index() const
Definition: sat_base.h:84
BooleanVariable Variable() const
Definition: sat_base.h:80
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
bool ProbeOneVariable(BooleanVariable b)
Definition: probing.cc:179
bool ProbeBooleanVariables(double deterministic_time_limit, bool log_info=false)
Definition: probing.cc:41
const Trail & LiteralTrail() const
Definition: sat_solver.h:361
void SetAssumptionLevel(int assumption_level)
Definition: sat_solver.cc:962
void AdvanceDeterministicTime(TimeLimit *limit)
Definition: sat_solver.h:422
int EnqueueDecisionAndBackjumpOnConflict(Literal true_literal)
Definition: sat_solver.cc:499
bool AddBinaryClause(Literal a, Literal b)
Definition: sat_solver.cc:180
bool AddUnitClause(Literal true_literal)
Definition: sat_solver.cc:164
int AssignmentType(BooleanVariable var) const
Definition: sat_base.h:572
bool LiteralIsAssigned(Literal literal) const
Definition: sat_base.h:153
SharedTimeLimit * time_limit
WallTimer * wall_timer
IntVar * var
Definition: expr_array.cc:1858
GRBmodel * model
int64_t int64
const int INFO
Definition: log_severity.h:31
bool VariableIsPositive(IntegerVariable i)
Definition: integer.h:130
bool LookForTrivialSatSolution(double deterministic_time_limit, Model *model, bool log_info)
Definition: probing.cc:270
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
const LiteralIndex kNoLiteralIndex(-1)
const IntegerVariable kNoIntegerVariable(-1)
IntegerVariable PositiveVariable(IntegerVariable i)
Definition: integer.h:134
bool FailedLiteralProbingRound(ProbingOptions options, Model *model)
Definition: probing.cc:350
void RandomizeDecisionHeuristic(URBG *random, SatParameters *parameters)
Definition: sat/util.h:100
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...
Literal literal
Definition: optimization.cc:84
int index
Definition: pack.cc:508
int64 bound
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1264
#define VLOG_IS_ON(verboselevel)
Definition: vlog_is_on.h:41