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"
24 #include "ortools/sat/sat_base.h"
25 #include "ortools/sat/sat_solver.h"
26 #include "ortools/sat/util.h"
28 
29 namespace operations_research {
30 namespace 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 
41 bool 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 
55 bool 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 
179 bool 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 
196 bool 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);
201  wall_timer.Start();
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 
270 bool LookForTrivialSatSolution(double deterministic_time_limit, Model* model,
271  bool log_info) {
272  log_info |= VLOG_IS_ON(1);
274  wall_timer.Start();
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 
352  wall_timer.Start();
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;
396  absl::StrongVector<LiteralIndex, int> position_in_order;
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
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
bool LookForTrivialSatSolution(double deterministic_time_limit, Model *model, bool log_info)
Definition: probing.cc:270
const LiteralIndex kNoLiteralIndex(-1)
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
const IntegerVariable kNoIntegerVariable(-1)
IntegerVariable PositiveVariable(IntegerVariable i)
Definition: integer.h:134
bool FailedLiteralProbingRound(ProbingOptions options, Model *model)
Definition: probing.cc:350
bool VariableIsPositive(IntegerVariable i)
Definition: integer.h:130
void RandomizeDecisionHeuristic(URBG *random, SatParameters *parameters)
Definition: sat/util.h:100
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