Google OR-Tools v9.14
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
probing.cc
Go to the documentation of this file.
1// Copyright 2010-2025 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 <algorithm>
17#include <cstdint>
18#include <functional>
19#include <utility>
20#include <vector>
21
22#include "absl/container/btree_map.h"
23#include "absl/container/btree_set.h"
24#include "absl/container/inlined_vector.h"
25#include "absl/log/check.h"
26#include "absl/log/log.h"
27#include "absl/log/vlog_is_on.h"
28#include "absl/strings/string_view.h"
29#include "absl/types/span.h"
32#include "ortools/base/timer.h"
33#include "ortools/sat/clause.h"
35#include "ortools/sat/integer.h"
37#include "ortools/sat/model.h"
41#include "ortools/sat/util.h"
42#include "ortools/util/bitset.h"
47
48namespace operations_research {
49namespace sat {
50
52 : trail_(*model->GetOrCreate<Trail>()),
53 assignment_(model->GetOrCreate<SatSolver>()->Assignment()),
54 integer_trail_(model->GetOrCreate<IntegerTrail>()),
55 implied_bounds_(model->GetOrCreate<ImpliedBounds>()),
56 product_detector_(model->GetOrCreate<ProductDetector>()),
57 sat_solver_(model->GetOrCreate<SatSolver>()),
58 time_limit_(model->GetOrCreate<TimeLimit>()),
59 implication_graph_(model->GetOrCreate<BinaryImplicationGraph>()),
60 logger_(model->GetOrCreate<SolverLogger>()) {}
61
62bool Prober::ProbeBooleanVariables(const double deterministic_time_limit) {
63 const int num_variables = sat_solver_->NumVariables();
64 const VariablesAssignment& assignment = sat_solver_->Assignment();
65 std::vector<BooleanVariable> bool_vars;
66 for (BooleanVariable b(0); b < num_variables; ++b) {
67 if (assignment.VariableIsAssigned(b)) continue;
68 const Literal literal(b, true);
69 if (implication_graph_->RepresentativeOf(literal) != literal) {
70 continue;
71 }
72 bool_vars.push_back(b);
73 }
74 return ProbeBooleanVariables(deterministic_time_limit, bool_vars);
75}
76
77bool Prober::ProbeOneVariableInternal(BooleanVariable b) {
78 new_integer_bounds_.clear();
79 propagated_.ResetAllToFalse();
80 for (const Literal decision : {Literal(b, true), Literal(b, false)}) {
81 if (assignment_.LiteralIsAssigned(decision)) continue;
82
83 ++num_decisions_;
84 CHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0);
85 const int saved_index = trail_.Index();
86 sat_solver_->EnqueueDecisionAndBackjumpOnConflict(decision);
87 sat_solver_->AdvanceDeterministicTime(time_limit_);
88
89 if (sat_solver_->ModelIsUnsat()) return false;
90 if (sat_solver_->CurrentDecisionLevel() == 0) continue;
91 if (trail_.Index() > saved_index) {
92 if (callback_ != nullptr) callback_(decision);
93 }
94
95 if (!implied_bounds_->ProcessIntegerTrail(decision)) return false;
96 product_detector_->ProcessTrailAtLevelOne();
97 integer_trail_->AppendNewBounds(&new_integer_bounds_);
98 for (int i = saved_index + 1; i < trail_.Index(); ++i) {
99 const Literal l = trail_[i];
100
101 // We mark on the first run (b.IsPositive()) and check on the second.
102 if (decision.IsPositive()) {
103 propagated_.Set(l.Index());
104 } else {
105 if (propagated_[l]) {
106 to_fix_at_true_.push_back(l);
107 }
108 }
109
110 // Anything not propagated by the BinaryImplicationGraph is a "new"
111 // binary clause. This is because the BinaryImplicationGraph has the
112 // highest priority of all propagators.
113 if (trail_.AssignmentType(l.Variable()) !=
114 implication_graph_->PropagatorId()) {
115 new_binary_clauses_.push_back({decision.Negated(), l});
116 }
117 }
118
119 // Fix variable and add new binary clauses.
120 if (!sat_solver_->ResetToLevelZero()) return false;
121 for (const Literal l : to_fix_at_true_) {
122 if (!sat_solver_->AddUnitClause(l)) return false;
123 }
124 to_fix_at_true_.clear();
125 if (!sat_solver_->FinishPropagation()) return false;
126 num_new_binary_ += new_binary_clauses_.size();
127 for (auto binary : new_binary_clauses_) {
128 sat_solver_->AddBinaryClause(binary.first, binary.second);
129 }
130 new_binary_clauses_.clear();
131 if (!sat_solver_->FinishPropagation()) return false;
132 }
133
134 // We have at most two lower bounds for each variables (one for b==0 and one
135 // for b==1), so the min of the two is a valid level zero bound! More
136 // generally, the domain of a variable can be intersected with the union
137 // of the two propagated domains. This also allow to detect "holes".
138 //
139 // TODO(user): More generally, for any clauses (b or not(b) is one), we
140 // could probe all the literal inside, and for any integer variable, we can
141 // take the union of the propagated domain as a new domain.
142 //
143 // TODO(user): fix binary variable in the same way? It might not be as
144 // useful since probing on such variable will also fix it. But then we might
145 // abort probing early, so it might still be good.
146 std::sort(new_integer_bounds_.begin(), new_integer_bounds_.end(),
147 [](IntegerLiteral a, IntegerLiteral b) { return a.var < b.var; });
148
149 // This is used for the hole detection.
150 IntegerVariable prev_var = kNoIntegerVariable;
151 IntegerValue lb_max = kMinIntegerValue;
152 IntegerValue ub_min = kMaxIntegerValue;
153 new_integer_bounds_.push_back(IntegerLiteral()); // Sentinel.
154
155 const int limit = new_integer_bounds_.size();
156 for (int i = 0; i < limit; ++i) {
157 const IntegerVariable var = new_integer_bounds_[i].var;
158
159 // Hole detection.
160 if (i > 0 && PositiveVariable(var) != prev_var) {
161 if (ub_min + 1 < lb_max) {
162 // The variable cannot take value in (ub_min, lb_max) !
163 //
164 // TODO(user): do not create domain with a complexity that is too
165 // large?
166 const Domain old_domain =
167 integer_trail_->InitialVariableDomain(prev_var);
168 const Domain new_domain = old_domain.IntersectionWith(
169 Domain(ub_min.value() + 1, lb_max.value() - 1).Complement());
170 if (new_domain != old_domain) {
171 ++num_new_holes_;
172 if (!integer_trail_->UpdateInitialDomain(prev_var, new_domain)) {
173 return false;
174 }
175 }
176 }
177
178 // Reinitialize.
179 lb_max = kMinIntegerValue;
180 ub_min = kMaxIntegerValue;
181 }
182
183 prev_var = PositiveVariable(var);
184 if (VariableIsPositive(var)) {
185 lb_max = std::max(lb_max, new_integer_bounds_[i].bound);
186 } else {
187 ub_min = std::min(ub_min, -new_integer_bounds_[i].bound);
188 }
189
190 // Bound tightening.
191 if (i == 0 || new_integer_bounds_[i - 1].var != var) continue;
192 const IntegerValue new_bound = std::min(new_integer_bounds_[i - 1].bound,
193 new_integer_bounds_[i].bound);
194 if (new_bound > integer_trail_->LowerBound(var)) {
195 ++num_new_integer_bounds_;
196 if (!integer_trail_->Enqueue(
197 IntegerLiteral::GreaterOrEqual(var, new_bound), {}, {})) {
198 return false;
199 }
200 }
201 }
202
203 // We might have updated some integer domain, let's propagate.
204 return sat_solver_->FinishPropagation();
205}
206
207bool Prober::ProbeOneVariable(BooleanVariable b) {
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 if (!sat_solver_->ResetToLevelZero()) return false;
214
215 const int initial_num_fixed = sat_solver_->LiteralTrail().Index();
216 if (!ProbeOneVariableInternal(b)) return false;
217
218 // Statistics
219 const int num_fixed = sat_solver_->LiteralTrail().Index();
220 num_new_literals_fixed_ += num_fixed - initial_num_fixed;
221 return true;
222}
223
225 const double deterministic_time_limit,
226 absl::Span<const BooleanVariable> bool_vars) {
227 WallTimer wall_timer;
228 wall_timer.Start();
229
230 // Reset statistics.
231 num_decisions_ = 0;
232 num_new_binary_ = 0;
233 num_new_holes_ = 0;
234 num_new_integer_bounds_ = 0;
235 num_new_literals_fixed_ = 0;
236
237 // Resize the propagated sparse bitset.
238 const int num_variables = sat_solver_->NumVariables();
239 propagated_.ClearAndResize(LiteralIndex(2 * num_variables));
240
241 // Reset the solver in case it was already used.
242 if (!sat_solver_->ResetToLevelZero()) return false;
243
244 const int initial_num_fixed = sat_solver_->LiteralTrail().Index();
245 const double initial_deterministic_time =
246 time_limit_->GetElapsedDeterministicTime();
247 const double limit = initial_deterministic_time + deterministic_time_limit;
248
249 bool limit_reached = false;
250 int num_probed = 0;
251
252 for (const BooleanVariable b : bool_vars) {
253 const Literal literal(b, true);
254 if (implication_graph_->RepresentativeOf(literal) != literal) {
255 continue;
256 }
257
258 // TODO(user): Instead of an hard deterministic limit, we should probably
259 // use a lower one, but reset it each time we have found something useful.
260 if (time_limit_->LimitReached() ||
261 time_limit_->GetElapsedDeterministicTime() > limit) {
262 limit_reached = true;
263 break;
264 }
265
266 // Propagate b=1 and then b=0.
267 ++num_probed;
268 if (!ProbeOneVariableInternal(b)) {
269 return false;
270 }
271 }
272
273 // Update stats.
274 const int num_fixed = sat_solver_->LiteralTrail().Index();
275 num_new_literals_fixed_ = num_fixed - initial_num_fixed;
276
277 // Display stats.
278 if (logger_->LoggingIsEnabled()) {
279 const double time_diff =
280 time_limit_->GetElapsedDeterministicTime() - initial_deterministic_time;
281 SOLVER_LOG(logger_, "[Probing] deterministic_time: ", time_diff,
282 " (limit: ", deterministic_time_limit,
283 ") wall_time: ", wall_timer.Get(), " (",
284 (limit_reached ? "Aborted " : ""), num_probed, "/",
285 bool_vars.size(), ")");
286 if (num_new_literals_fixed_ > 0) {
287 SOLVER_LOG(logger_,
288 "[Probing] - new fixed Boolean: ", num_new_literals_fixed_,
289 " (", num_fixed, "/", sat_solver_->NumVariables(), ")");
290 }
291 if (num_new_holes_ > 0) {
292 SOLVER_LOG(logger_, "[Probing] - new integer holes: ", num_new_holes_);
293 }
294 if (num_new_integer_bounds_ > 0) {
295 SOLVER_LOG(logger_,
296 "[Probing] - new integer bounds: ", num_new_integer_bounds_);
297 }
298 if (num_new_binary_ > 0) {
299 SOLVER_LOG(logger_, "[Probing] - new binary clause: ", num_new_binary_);
300 }
301 }
302
303 return true;
304}
305
306bool Prober::ProbeDnf(absl::string_view name,
307 absl::Span<const std::vector<Literal>> dnf) {
308 if (dnf.size() <= 1) return true;
309
310 // Reset the solver in case it was already used.
311 if (!sat_solver_->ResetToLevelZero()) return false;
312
313 always_propagated_bounds_.clear();
314 always_propagated_literals_.clear();
315 int num_valid_conjunctions = 0;
316 for (const std::vector<Literal>& conjunction : dnf) {
317 if (!sat_solver_->ResetToLevelZero()) return false;
318 if (num_valid_conjunctions > 0 && always_propagated_bounds_.empty() &&
319 always_propagated_literals_.empty()) {
320 // We can exit safely as nothing will be propagated.
321 return true;
322 }
323
324 bool conjunction_is_valid = true;
325 int num_literals_enqueued = 0;
326 const int root_trail_index = trail_.Index();
327 const int root_integer_trail_index = integer_trail_->Index();
328 for (const Literal& lit : conjunction) {
329 if (assignment_.LiteralIsAssigned(lit)) {
330 if (assignment_.LiteralIsTrue(lit)) continue;
331 conjunction_is_valid = false;
332 break;
333 }
334 ++num_literals_enqueued;
335 const int decision_level_before_enqueue =
336 sat_solver_->CurrentDecisionLevel();
337 sat_solver_->EnqueueDecisionAndBackjumpOnConflict(lit);
338 sat_solver_->AdvanceDeterministicTime(time_limit_);
339 const int decision_level_after_enqueue =
340 sat_solver_->CurrentDecisionLevel();
341 ++num_decisions_;
342
343 if (sat_solver_->ModelIsUnsat()) return false;
344 // If the literal has been pushed without any conflict, the level should
345 // have been increased.
346 if (decision_level_after_enqueue <= decision_level_before_enqueue) {
347 conjunction_is_valid = false;
348 break;
349 }
350 // TODO(user): Can we use the callback_?
351 }
352 if (conjunction_is_valid) {
353 ++num_valid_conjunctions;
354 } else {
355 continue;
356 }
357
358 // Process propagated literals.
359 new_propagated_literals_.clear();
360 for (int i = root_trail_index; i < trail_.Index(); ++i) {
361 const LiteralIndex literal_index = trail_[i].Index();
362 if (num_valid_conjunctions == 1 ||
363 always_propagated_literals_.contains(literal_index)) {
364 new_propagated_literals_.insert(literal_index);
365 }
366 }
367 std::swap(new_propagated_literals_, always_propagated_literals_);
368
369 // Process propagated integer bounds.
370 new_integer_bounds_.clear();
371 integer_trail_->AppendNewBoundsFrom(root_integer_trail_index,
372 &new_integer_bounds_);
373 new_propagated_bounds_.clear();
374 for (const IntegerLiteral entry : new_integer_bounds_) {
375 const auto it = always_propagated_bounds_.find(entry.var);
376 if (num_valid_conjunctions == 1) { // First loop.
377 new_propagated_bounds_[entry.var] = entry.bound;
378 } else if (it != always_propagated_bounds_.end()) {
379 new_propagated_bounds_[entry.var] = std::min(entry.bound, it->second);
380 }
381 }
382 std::swap(new_propagated_bounds_, always_propagated_bounds_);
383 }
384
385 if (!sat_solver_->ResetToLevelZero()) return false;
386 // Fix literals implied by the dnf.
387 const int previous_num_literals_fixed = num_new_literals_fixed_;
388 for (const LiteralIndex literal_index : always_propagated_literals_) {
389 const Literal lit(literal_index);
390 if (assignment_.LiteralIsTrue(lit)) continue;
391 ++num_new_literals_fixed_;
392 if (!sat_solver_->AddUnitClause(lit)) return false;
393 }
394
395 // Fix integer bounds implied by the dnf.
396 int previous_num_integer_bounds = num_new_integer_bounds_;
397 for (const auto& [var, bound] : always_propagated_bounds_) {
398 if (bound > integer_trail_->LowerBound(var)) {
399 ++num_new_integer_bounds_;
400 if (!integer_trail_->Enqueue(IntegerLiteral::GreaterOrEqual(var, bound),
401 {}, {})) {
402 return false;
403 }
404 }
405 }
406
407 if (!sat_solver_->FinishPropagation()) return false;
408
409 if (num_new_integer_bounds_ > previous_num_integer_bounds ||
410 num_new_literals_fixed_ > previous_num_literals_fixed) {
411 VLOG(1) << "ProbeDnf(" << name << ", num_fixed_literals="
412 << num_new_literals_fixed_ - previous_num_literals_fixed
413 << ", num_pushed_integer_bounds="
414 << num_new_integer_bounds_ - previous_num_integer_bounds
415 << ", num_valid_conjunctions=" << num_valid_conjunctions << "/"
416 << dnf.size() << ")";
417 }
418
419 return true;
420}
421
422bool LookForTrivialSatSolution(double deterministic_time_limit, Model* model,
423 SolverLogger* logger) {
424 WallTimer wall_timer;
425 wall_timer.Start();
426
427 // Hack to not have empty logger.
428 if (logger == nullptr) logger = model->GetOrCreate<SolverLogger>();
429
430 // Reset the solver in case it was already used.
431 auto* sat_solver = model->GetOrCreate<SatSolver>();
432 if (!sat_solver->ResetToLevelZero()) return false;
433
434 auto* time_limit = model->GetOrCreate<TimeLimit>();
435 const int initial_num_fixed = sat_solver->LiteralTrail().Index();
436
437 // Note that this code do not care about the non-Boolean part and just try to
438 // assign the existing Booleans.
439 SatParameters initial_params = *model->GetOrCreate<SatParameters>();
440 SatParameters new_params = initial_params;
441 new_params.set_log_search_progress(false);
442 new_params.set_max_number_of_conflicts(1);
443 new_params.set_max_deterministic_time(deterministic_time_limit);
444
445 double elapsed_dtime = 0.0;
446
447 const int num_times = 1000;
448 bool limit_reached = false;
449 auto* random = model->GetOrCreate<ModelRandomGenerator>();
450 for (int i = 0; i < num_times; ++i) {
451 if (time_limit->LimitReached() ||
452 elapsed_dtime > deterministic_time_limit) {
453 limit_reached = true;
454 break;
455 }
456
457 // SetParameters() reset the deterministic time to zero inside time_limit.
458 sat_solver->SetParameters(new_params);
459 sat_solver->ResetDecisionHeuristic();
460 const SatSolver::Status result = sat_solver->SolveWithTimeLimit(time_limit);
461 elapsed_dtime += time_limit->GetElapsedDeterministicTime();
462
463 if (result == SatSolver::FEASIBLE) {
464 SOLVER_LOG(logger, "Trivial exploration found feasible solution!");
465 time_limit->AdvanceDeterministicTime(elapsed_dtime);
466 return true;
467 }
468
469 if (!sat_solver->ResetToLevelZero()) {
470 SOLVER_LOG(logger, "UNSAT during trivial exploration heuristic.");
471 time_limit->AdvanceDeterministicTime(elapsed_dtime);
472 return false;
473 }
474
475 // We randomize at the end so that the default params is executed
476 // at least once.
477 RandomizeDecisionHeuristic(*random, &new_params);
478 new_params.set_random_seed(i);
479 new_params.set_max_deterministic_time(deterministic_time_limit -
480 elapsed_dtime);
481 }
482
483 // Restore the initial parameters.
484 sat_solver->SetParameters(initial_params);
485 sat_solver->ResetDecisionHeuristic();
486 time_limit->AdvanceDeterministicTime(elapsed_dtime);
487 if (!sat_solver->ResetToLevelZero()) return false;
488
489 if (logger->LoggingIsEnabled()) {
490 const int num_fixed = sat_solver->LiteralTrail().Index();
491 const int num_newly_fixed = num_fixed - initial_num_fixed;
492 const int num_variables = sat_solver->NumVariables();
493 SOLVER_LOG(logger, "[Random exploration]", " num_fixed: +", num_newly_fixed,
494 " (", num_fixed, "/", num_variables, ")",
495 " dtime: ", elapsed_dtime, "/", deterministic_time_limit,
496 " wtime: ", wall_timer.Get(),
497 (limit_reached ? " (Aborted)" : ""));
498 }
499 return sat_solver->FinishPropagation();
500}
501
503 WallTimer wall_timer;
504 wall_timer.Start();
505 options.log_info |= VLOG_IS_ON(1);
506
507 // Reset the solver in case it was already used.
508 auto* sat_solver = model->GetOrCreate<SatSolver>();
509 if (!sat_solver->ResetToLevelZero()) return false;
510
511 // When called from Inprocessing, the implication graph should already be a
512 // DAG, so these two calls should return right away. But we do need them to
513 // get the topological order if this is used in isolation.
514 auto* implication_graph = model->GetOrCreate<BinaryImplicationGraph>();
515 if (!implication_graph->DetectEquivalences()) return false;
516 if (!sat_solver->FinishPropagation()) return false;
517
518 auto* time_limit = model->GetOrCreate<TimeLimit>();
519 const int initial_num_fixed = sat_solver->LiteralTrail().Index();
520 const double initial_deterministic_time =
521 time_limit->GetElapsedDeterministicTime();
522 const double limit = initial_deterministic_time + options.deterministic_limit;
523
524 const int num_variables = sat_solver->NumVariables();
525 SparseBitset<LiteralIndex> processed(LiteralIndex(2 * num_variables));
526
527 int64_t num_probed = 0;
528 int64_t num_explicit_fix = 0;
529 int64_t num_conflicts = 0;
530 int64_t num_new_binary = 0;
531 int64_t num_subsumed = 0;
532
533 const auto& trail = *(model->Get<Trail>());
534 const auto& assignment = trail.Assignment();
535 auto* clause_manager = model->GetOrCreate<ClauseManager>();
536 const int id = implication_graph->PropagatorId();
537 const int clause_id = clause_manager->PropagatorId();
538
539 // This is only needed when options.use_queue is true.
540 struct SavedNextLiteral {
541 LiteralIndex literal_index; // kNoLiteralIndex if we need to backtrack.
542 int rank; // Cached position_in_order, we prefer lower positions.
543
544 bool operator<(const SavedNextLiteral& o) const { return rank < o.rank; }
545 };
546 std::vector<SavedNextLiteral> queue;
548
549 // This is only needed when options use_queue is false;
551 if (!options.use_queue) starts.resize(2 * num_variables, 0);
552
553 // We delay fixing of already assigned literal once we go back to level
554 // zero.
555 std::vector<Literal> to_fix;
556
557 // Depending on the options. we do not use the same order.
558 // With tree look, it is better to start with "leaf" first since we try
559 // to reuse propagation as much as possible. This is also interesting to
560 // do when extracting binary clauses since we will need to propagate
561 // everyone anyway, and this should result in less clauses that can be
562 // removed later by transitive reduction.
563 //
564 // However, without tree-look and without the need to extract all binary
565 // clauses, it is better to just probe the root of the binary implication
566 // graph. This is exactly what happen when we probe using the topological
567 // order.
568 int order_index(0);
569 std::vector<LiteralIndex> probing_order =
570 implication_graph->ReverseTopologicalOrder();
571 if (!options.use_tree_look && !options.extract_binary_clauses) {
572 std::reverse(probing_order.begin(), probing_order.end());
573 }
574
575 // We only use this for the queue version.
576 if (options.use_queue) {
577 position_in_order.assign(2 * num_variables, -1);
578 for (int i = 0; i < probing_order.size(); ++i) {
579 position_in_order[probing_order[i]] = i;
580 }
581 }
582
583 while (!time_limit->LimitReached() &&
584 time_limit->GetElapsedDeterministicTime() <= limit) {
585 // We only enqueue literal at level zero if we don't use "tree look".
586 if (!options.use_tree_look) sat_solver->Backtrack(0);
587
588 LiteralIndex next_decision = kNoLiteralIndex;
589 if (options.use_queue && sat_solver->CurrentDecisionLevel() > 0) {
590 // TODO(user): Instead of minimizing index in topo order (which might be
591 // nice for binary extraction), we could try to maximize reusability in
592 // some way.
593 const Literal prev_decision =
594 sat_solver->Decisions()[sat_solver->CurrentDecisionLevel() - 1]
595 .literal;
596 const auto& list =
597 implication_graph->Implications(prev_decision.Negated());
598 const int saved_queue_size = queue.size();
599 for (const Literal l : list) {
600 const Literal candidate = l.Negated();
601 if (processed[candidate]) continue;
602 if (position_in_order[candidate] == -1) continue;
603 if (assignment.LiteralIsAssigned(candidate)) {
604 if (assignment.LiteralIsFalse(candidate)) {
605 to_fix.push_back(Literal(candidate.Negated()));
606 }
607 continue;
608 }
609 queue.push_back({candidate.Index(), -position_in_order[candidate]});
610 }
611 std::sort(queue.begin() + saved_queue_size, queue.end());
612
613 // Probe a literal that implies previous decision.
614 while (!queue.empty()) {
615 const LiteralIndex index = queue.back().literal_index;
616 queue.pop_back();
617 if (index == kNoLiteralIndex) {
618 // This is a backtrack marker, go back one level.
619 CHECK_GT(sat_solver->CurrentDecisionLevel(), 0);
620 sat_solver->Backtrack(sat_solver->CurrentDecisionLevel() - 1);
621 continue;
622 }
623 const Literal candidate(index);
624 if (processed[candidate]) continue;
625 if (assignment.LiteralIsAssigned(candidate)) {
626 if (assignment.LiteralIsFalse(candidate)) {
627 to_fix.push_back(Literal(candidate.Negated()));
628 }
629 continue;
630 }
631 next_decision = candidate.Index();
632 break;
633 }
634 }
635
636 if (sat_solver->CurrentDecisionLevel() == 0) {
637 // Fix any delayed fixed literal.
638 for (const Literal literal : to_fix) {
639 if (!assignment.LiteralIsTrue(literal)) {
640 ++num_explicit_fix;
641 if (!sat_solver->AddUnitClause(literal)) return false;
642 }
643 }
644 to_fix.clear();
645 if (!sat_solver->FinishPropagation()) return false;
646
647 // Probe an unexplored node.
648 for (; order_index < probing_order.size(); ++order_index) {
649 const Literal candidate(probing_order[order_index]);
650 if (processed[candidate]) continue;
651 if (assignment.LiteralIsAssigned(candidate)) continue;
652 next_decision = candidate.Index();
653 break;
654 }
655
656 // The pass is finished.
657 if (next_decision == kNoLiteralIndex) break;
658 } else if (next_decision == kNoLiteralIndex) {
659 const int level = sat_solver->CurrentDecisionLevel();
660 const Literal prev_decision = sat_solver->Decisions()[level - 1].literal;
661 const auto& list =
662 implication_graph->Implications(prev_decision.Negated());
663
664 // Probe a literal that implies previous decision.
665 //
666 // Note that contrary to the queue based implementation, this do not
667 // process them in a particular order.
668 int j = starts[prev_decision.NegatedIndex()];
669 for (int i = 0; i < list.size(); ++i, ++j) {
670 j %= list.size();
671 const Literal candidate = Literal(list[j]).Negated();
672 if (processed[candidate]) continue;
673 if (assignment.LiteralIsFalse(candidate)) {
674 // candidate => previous => not(candidate), so we can fix it.
675 to_fix.push_back(Literal(candidate.Negated()));
676 continue;
677 }
678 // This shouldn't happen if extract_binary_clauses is false.
679 // We have an equivalence.
680 if (assignment.LiteralIsTrue(candidate)) continue;
681 next_decision = candidate.Index();
682 break;
683 }
684 starts[prev_decision.NegatedIndex()] = j;
685 if (next_decision == kNoLiteralIndex) {
686 sat_solver->Backtrack(level - 1);
687 continue;
688 }
689 }
690
691 ++num_probed;
692 processed.Set(next_decision);
693 CHECK_NE(next_decision, kNoLiteralIndex);
694 queue.push_back({kNoLiteralIndex, 0}); // Backtrack marker.
695 const int level = sat_solver->CurrentDecisionLevel();
696 const int first_new_trail_index =
697 sat_solver->EnqueueDecisionAndBackjumpOnConflict(
698 Literal(next_decision));
699 const int new_level = sat_solver->CurrentDecisionLevel();
700 sat_solver->AdvanceDeterministicTime(time_limit);
701 if (sat_solver->ModelIsUnsat()) return false;
702 if (new_level <= level) {
703 ++num_conflicts;
704
705 // Sync the queue with the new level.
706 if (options.use_queue) {
707 if (new_level == 0) {
708 queue.clear();
709 } else {
710 int queue_level = level + 1;
711 while (queue_level > new_level) {
712 CHECK(!queue.empty());
713 if (queue.back().literal_index == kNoLiteralIndex) --queue_level;
714 queue.pop_back();
715 }
716 }
717 }
718
719 // Fix `next_decision` to `false` if not already done.
720 //
721 // Even if we fixed something at level zero, next_decision might not be
722 // fixed! But we can fix it. It can happen because when we propagate
723 // with clauses, we might have `a => b` but not `not(b) => not(a)`. Like
724 // `a => b` and clause `(not(a), not(b), c)`, propagating `a` will set
725 // `c`, but propagating `not(c)` will not do anything.
726 //
727 // We "delay" the fixing if we are not at level zero so that we can
728 // still reuse the current propagation work via tree look.
729 //
730 // TODO(user): Can we be smarter here? Maybe we can still fix the
731 // literal without going back to level zero by simply enqueuing it with
732 // no reason? it will be backtracked over, but we will still lazily fix
733 // it later.
734 if (sat_solver->CurrentDecisionLevel() != 0 ||
735 assignment.LiteralIsFalse(Literal(next_decision))) {
736 to_fix.push_back(Literal(next_decision).Negated());
737 }
738 }
739
740 // Inspect the newly propagated literals. Depending on the options, try to
741 // extract binary clauses via hyper binary resolution and/or mark the
742 // literals on the trail so that they do not need to be probed later.
743 if (new_level == 0) continue;
744 const Literal last_decision =
745 sat_solver->Decisions()[new_level - 1].literal;
746 int num_new_subsumed = 0;
747 for (int i = first_new_trail_index; i < trail.Index(); ++i) {
748 const Literal l = trail[i];
749 if (l == last_decision) continue;
750
751 // If we can extract a binary clause that subsume the reason clause, we
752 // do add the binary and remove the subsumed clause.
753 //
754 // TODO(user): We could be slightly more generic and subsume some
755 // clauses that do not contains last_decision.Negated().
756 bool subsumed = false;
757 if (options.subsume_with_binary_clause &&
758 trail.AssignmentType(l.Variable()) == clause_id) {
759 for (const Literal lit : trail.Reason(l.Variable())) {
760 if (lit == last_decision.Negated()) {
761 subsumed = true;
762 break;
763 }
764 }
765 if (subsumed) {
766 ++num_new_subsumed;
767 ++num_new_binary;
768 CHECK(implication_graph->AddBinaryClause(last_decision.Negated(), l));
769 const int trail_index = trail.Info(l.Variable()).trail_index;
770
771 int test = 0;
772 for (const Literal lit :
773 clause_manager->ReasonClause(trail_index)->AsSpan()) {
774 if (lit == l) ++test;
775 if (lit == last_decision.Negated()) ++test;
776 }
777 CHECK_EQ(test, 2);
778 clause_manager->LazyDetach(clause_manager->ReasonClause(trail_index));
779
780 // We need to change the reason now that the clause is cleared.
781 implication_graph->ChangeReason(trail_index, last_decision);
782 }
783 }
784
785 if (options.extract_binary_clauses) {
786 // Anything not propagated by the BinaryImplicationGraph is a "new"
787 // binary clause. This is because the BinaryImplicationGraph has the
788 // highest priority of all propagators.
789 //
790 // Note(user): This is not 100% true, since when we launch the clause
791 // propagation for one literal we do finish it before calling again
792 // the binary propagation.
793 //
794 // TODO(user): Think about trying to extract clause that will not
795 // get removed by transitive reduction later. If we can both extract
796 // a => c and b => c , ideally we don't want to extract a => c first
797 // if we already know that a => b.
798 //
799 // TODO(user): Similar to previous point, we could find the LCA
800 // of all literals in the reason for this propagation. And use this
801 // as a reason for later hyber binary resolution. Like we do when
802 // this clause subsume the reason.
803 if (!subsumed && trail.AssignmentType(l.Variable()) != id) {
804 ++num_new_binary;
805 CHECK(implication_graph->AddBinaryClause(last_decision.Negated(), l));
806 }
807 } else {
808 // If we don't extract binary, we don't need to explore any of
809 // these literal until more variables are fixed.
810 processed.Set(l.Index());
811 }
812 }
813
814 // Inspect the watcher list for last_decision, If we have a blocking
815 // literal at true (implied by last decision), then we have subsumptions.
816 //
817 // The intuition behind this is that if a binary clause (a,b) subsume a
818 // clause, and we watch a.Negated() for this clause with a blocking
819 // literal b, then this watch entry will never change because we always
820 // propagate binary clauses first and the blocking literal will always be
821 // true. So after many propagations, we hope to have such configuration
822 // which is quite cheap to test here.
823 if (options.subsume_with_binary_clause) {
824 // Tricky: If we have many "decision" and we do not extract the binary
825 // clause, then the fact that last_decision => literal might not be
826 // currently encoded in the problem clause, so if we use that relation
827 // to subsume, we should make sure it is added.
828 //
829 // Note that it is okay to add duplicate binary clause, we will clean that
830 // later.
831 const bool always_add_binary = sat_solver->CurrentDecisionLevel() > 1 &&
832 !options.extract_binary_clauses;
833
834 for (const auto& w :
835 clause_manager->WatcherListOnFalse(last_decision.Negated())) {
836 if (assignment.LiteralIsTrue(w.blocking_literal)) {
837 if (w.clause->IsRemoved()) continue;
838 CHECK_NE(w.blocking_literal, last_decision.Negated());
839
840 // Add the binary clause if needed. Note that we change the reason
841 // to a binary one so that we never add the same clause twice.
842 //
843 // Tricky: while last_decision would be a valid reason, we need a
844 // reason that was assigned before this literal, so we use the
845 // decision at the level where this literal was assigned which is an
846 // even better reason. Maybe it is just better to change all the
847 // reason above to a binary one so we don't have an issue here.
848 if (always_add_binary ||
849 trail.AssignmentType(w.blocking_literal.Variable()) != id) {
850 // If the variable was true at level zero, there is no point
851 // adding the clause.
852 const auto& info = trail.Info(w.blocking_literal.Variable());
853 if (info.level > 0) {
854 ++num_new_binary;
855 CHECK(implication_graph->AddBinaryClause(last_decision.Negated(),
856 w.blocking_literal));
857
858 const Literal d = sat_solver->Decisions()[info.level - 1].literal;
859 if (d != w.blocking_literal) {
860 implication_graph->ChangeReason(info.trail_index, d);
861 }
862 }
863 }
864
865 ++num_new_subsumed;
866 clause_manager->LazyDetach(w.clause);
867 }
868 }
869 }
870
871 if (num_new_subsumed > 0) {
872 // TODO(user): We might just want to do that even more lazily by
873 // checking for detached clause while propagating here? and do a big
874 // cleanup at the end.
875 clause_manager->CleanUpWatchers();
876 num_subsumed += num_new_subsumed;
877 }
878 }
879
880 if (!sat_solver->ResetToLevelZero()) return false;
881 for (const Literal literal : to_fix) {
882 ++num_explicit_fix;
883 if (!sat_solver->AddUnitClause(literal)) return false;
884 }
885 to_fix.clear();
886 if (!sat_solver->FinishPropagation()) return false;
887
888 // Display stats.
889 const int num_fixed = sat_solver->LiteralTrail().Index();
890 const int num_newly_fixed = num_fixed - initial_num_fixed;
891 const double time_diff =
892 time_limit->GetElapsedDeterministicTime() - initial_deterministic_time;
893 const bool limit_reached = time_limit->LimitReached() ||
894 time_limit->GetElapsedDeterministicTime() > limit;
895 LOG_IF(INFO, options.log_info)
896 << "Probing. "
897 << " num_probed: " << num_probed << "/" << probing_order.size()
898 << " num_fixed: +" << num_newly_fixed << " (" << num_fixed << "/"
899 << num_variables << ")"
900 << " explicit_fix:" << num_explicit_fix
901 << " num_conflicts:" << num_conflicts
902 << " new_binary_clauses: " << num_new_binary
903 << " subsumed: " << num_subsumed << " dtime: " << time_diff
904 << " wtime: " << wall_timer.Get() << (limit_reached ? " (Aborted)" : "");
905 return sat_solver->FinishPropagation();
906}
907
908} // namespace sat
909} // namespace operations_research
double Get() const
Definition timer.h:44
void Start()
When Start() is called multiple times, only the most recent is used.
Definition timer.h:30
bool LoggingIsEnabled() const
Returns true iff logging is enabled.
Definition logging.h:50
void Set(IntegerType index)
Definition bitset.h:878
bool ProcessIntegerTrail(Literal first_decision)
void AppendNewBounds(std::vector< IntegerLiteral > *output) const
Definition integer.cc:2058
LiteralIndex NegatedIndex() const
Definition sat_base.h:92
LiteralIndex Index() const
Definition sat_base.h:91
BooleanVariable Variable() const
Definition sat_base.h:87
T Get(std::function< T(const Model &)> f) const
Similar to Add() but this is const.
Definition model.h:93
bool ProbeBooleanVariables(double deterministic_time_limit)
Definition probing.cc:62
bool ProbeDnf(absl::string_view name, absl::Span< const std::vector< Literal > > dnf)
Definition probing.cc:306
bool ProbeOneVariable(BooleanVariable b)
Definition probing.cc:207
int EnqueueDecisionAndBackjumpOnConflict(Literal true_literal)
void AdvanceDeterministicTime(TimeLimit *limit)
Definition sat_solver.h:478
bool VariableIsAssigned(BooleanVariable var) const
Returns true iff the given variable is assigned.
Definition sat_base.h:196
bool LiteralIsAssigned(Literal literal) const
Definition sat_base.h:191
void assign(size_type n, const value_type &val)
void resize(size_type new_size)
time_limit
Definition solve.cc:22
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
void RandomizeDecisionHeuristic(absl::BitGenRef random, SatParameters *parameters)
Randomizes the decision heuristic of the given SatParameters.
Definition util.cc:101
const LiteralIndex kNoLiteralIndex(-1)
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue.value())
const IntegerVariable kNoIntegerVariable(-1)
bool LookForTrivialSatSolution(double deterministic_time_limit, Model *model, SolverLogger *logger)
Definition probing.cc:422
IntegerVariable PositiveVariable(IntegerVariable i)
bool FailedLiteralProbingRound(ProbingOptions options, Model *model)
Definition probing.cc:502
bool VariableIsPositive(IntegerVariable i)
In SWIG mode, we don't want anything besides these top-level includes.
trees with all degrees equal w the current value of w
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
bool log_info
We assume this is also true if –v 1 is activated.
Definition probing.h:228
#define SOLVER_LOG(logger,...)
Definition logging.h:110