OR-Tools  8.1
circuit.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/circuit.h"
15 
16 #include <algorithm>
17 
18 #include "absl/container/flat_hash_map.h"
19 #include "ortools/base/map_util.h"
20 #include "ortools/sat/sat_solver.h"
21 
22 namespace operations_research {
23 namespace sat {
24 
26  const std::vector<int>& tails,
27  const std::vector<int>& heads,
28  const std::vector<Literal>& literals,
29  Options options, Model* model)
30  : num_nodes_(num_nodes),
31  options_(options),
32  trail_(model->GetOrCreate<Trail>()),
33  assignment_(trail_->Assignment()) {
34  CHECK(!tails.empty()) << "Empty constraint, shouldn't be constructed!";
35  next_.resize(num_nodes_, -1);
36  prev_.resize(num_nodes_, -1);
37  next_literal_.resize(num_nodes_);
38  must_be_in_cycle_.resize(num_nodes_);
39  absl::flat_hash_map<LiteralIndex, int> literal_to_watch_index;
40 
41  const int num_arcs = tails.size();
42  graph_.reserve(num_arcs);
43  self_arcs_.resize(num_nodes_,
44  model->GetOrCreate<IntegerEncoder>()->GetFalseLiteral());
45  for (int arc = 0; arc < num_arcs; ++arc) {
46  const int head = heads[arc];
47  const int tail = tails[arc];
48  const Literal literal = literals[arc];
49  if (assignment_.LiteralIsFalse(literal)) continue;
50 
51  if (tail == head) {
52  self_arcs_[tail] = literal;
53  } else {
54  graph_[{tail, head}] = literal;
55  }
56 
57  if (assignment_.LiteralIsTrue(literal)) {
58  if (next_[tail] != -1 || prev_[head] != -1) {
59  VLOG(1) << "Trivially UNSAT or duplicate arcs while adding " << tail
60  << " -> " << head;
61  model->GetOrCreate<SatSolver>()->NotifyThatModelIsUnsat();
62  return;
63  }
64  AddArc(tail, head, kNoLiteralIndex);
65  continue;
66  }
67 
68  // Tricky: For self-arc, we watch instead when the arc become false.
69  const Literal watched_literal = tail == head ? literal.Negated() : literal;
70  int watch_index = gtl::FindWithDefault(literal_to_watch_index,
71  watched_literal.Index(), -1);
72  if (watch_index == -1) {
73  watch_index = watch_index_to_literal_.size();
74  literal_to_watch_index[watched_literal.Index()] = watch_index;
75  watch_index_to_literal_.push_back(watched_literal);
76  watch_index_to_arcs_.push_back(std::vector<Arc>());
77  }
78  watch_index_to_arcs_[watch_index].push_back({tail, head});
79  }
80 
81  for (int node = 0; node < num_nodes_; ++node) {
82  if (assignment_.LiteralIsFalse(self_arcs_[node])) {
83  // For the multiple_subcircuit_through_zero case, must_be_in_cycle_ will
84  // be const and only contains zero.
85  if (node == 0 || !options_.multiple_subcircuit_through_zero) {
86  must_be_in_cycle_[rev_must_be_in_cycle_size_++] = node;
87  }
88  }
89  }
90 }
91 
93  const int id = watcher->Register(this);
94  for (int w = 0; w < watch_index_to_literal_.size(); ++w) {
95  watcher->WatchLiteral(watch_index_to_literal_[w], id, w);
96  }
97  watcher->RegisterReversibleClass(id, this);
98  watcher->RegisterReversibleInt(id, &propagation_trail_index_);
99  watcher->RegisterReversibleInt(id, &rev_must_be_in_cycle_size_);
100 
101  // This is needed in case a Literal is used for more than one arc, we may
102  // propagate it to false/true here, and it might trigger more propagation.
103  //
104  // TODO(user): come up with a test that fail when this is not here.
106 }
107 
109  if (level == level_ends_.size()) return;
110  if (level > level_ends_.size()) {
111  while (level > level_ends_.size()) {
112  level_ends_.push_back(added_arcs_.size());
113  }
114  return;
115  }
116 
117  // Backtrack.
118  for (int i = level_ends_[level]; i < added_arcs_.size(); ++i) {
119  const Arc arc = added_arcs_[i];
120  next_[arc.tail] = -1;
121  prev_[arc.head] = -1;
122  }
123  added_arcs_.resize(level_ends_[level]);
124  level_ends_.resize(level);
125 }
126 
127 void CircuitPropagator::FillReasonForPath(int start_node,
128  std::vector<Literal>* reason) const {
129  CHECK_NE(start_node, -1);
130  reason->clear();
131  int node = start_node;
132  while (next_[node] != -1) {
133  if (next_literal_[node] != kNoLiteralIndex) {
134  reason->push_back(Literal(next_literal_[node]).Negated());
135  }
136  node = next_[node];
137  if (node == start_node) break;
138  }
139 }
140 
141 // If multiple_subcircuit_through_zero is true, we never fill next_[0] and
142 // prev_[0].
143 void CircuitPropagator::AddArc(int tail, int head, LiteralIndex literal_index) {
144  if (tail != 0 || !options_.multiple_subcircuit_through_zero) {
145  next_[tail] = head;
146  next_literal_[tail] = literal_index;
147  }
148  if (head != 0 || !options_.multiple_subcircuit_through_zero) {
149  prev_[head] = tail;
150  }
151 }
152 
154  const std::vector<int>& watch_indices) {
155  for (const int w : watch_indices) {
156  const Literal literal = watch_index_to_literal_[w];
157  for (const Arc arc : watch_index_to_arcs_[w]) {
158  // Special case for self-arc.
159  if (arc.tail == arc.head) {
160  must_be_in_cycle_[rev_must_be_in_cycle_size_++] = arc.tail;
161  continue;
162  }
163 
164  // Get rid of the trivial conflicts: At most one incoming and one outgoing
165  // arc for each nodes.
166  if (next_[arc.tail] != -1) {
167  std::vector<Literal>* conflict = trail_->MutableConflict();
168  if (next_literal_[arc.tail] != kNoLiteralIndex) {
169  *conflict = {Literal(next_literal_[arc.tail]).Negated(),
170  literal.Negated()};
171  } else {
172  *conflict = {literal.Negated()};
173  }
174  return false;
175  }
176  if (prev_[arc.head] != -1) {
177  std::vector<Literal>* conflict = trail_->MutableConflict();
178  if (next_literal_[prev_[arc.head]] != kNoLiteralIndex) {
179  *conflict = {Literal(next_literal_[prev_[arc.head]]).Negated(),
180  literal.Negated()};
181  } else {
182  *conflict = {literal.Negated()};
183  }
184  return false;
185  }
186 
187  // Add the arc.
188  AddArc(arc.tail, arc.head, literal.Index());
189  added_arcs_.push_back(arc);
190  }
191  }
192  return Propagate();
193 }
194 
195 // This function assumes that next_, prev_, next_literal_ and must_be_in_cycle_
196 // are all up to date.
198  processed_.assign(num_nodes_, false);
199  for (int n = 0; n < num_nodes_; ++n) {
200  if (processed_[n]) continue;
201  if (next_[n] == n) continue;
202  if (next_[n] == -1 && prev_[n] == -1) continue;
203 
204  // TODO(user): both this and the loop on must_be_in_cycle_ might take some
205  // time on large graph. Optimize if this become an issue.
206  in_current_path_.assign(num_nodes_, false);
207 
208  // Find the start and end of the path containing node n. If this is a
209  // circuit, we will have start_node == end_node.
210  int start_node = n;
211  int end_node = n;
212  in_current_path_[n] = true;
213  processed_[n] = true;
214  while (next_[end_node] != -1) {
215  end_node = next_[end_node];
216  in_current_path_[end_node] = true;
217  processed_[end_node] = true;
218  if (end_node == n) break;
219  }
220  while (prev_[start_node] != -1) {
221  start_node = prev_[start_node];
222  in_current_path_[start_node] = true;
223  processed_[start_node] = true;
224  if (start_node == n) break;
225  }
226 
227  // Check if we miss any node that must be in the circuit. Note that the ones
228  // for which self_arcs_[i] is kFalseLiteralIndex are first. This is good as
229  // it will produce shorter reason. Otherwise we prefer the first that was
230  // assigned in the trail.
231  bool miss_some_nodes = false;
232  LiteralIndex extra_reason = kFalseLiteralIndex;
233  for (int i = 0; i < rev_must_be_in_cycle_size_; ++i) {
234  const int node = must_be_in_cycle_[i];
235  if (!in_current_path_[node]) {
236  miss_some_nodes = true;
237  extra_reason = self_arcs_[node].Index();
238  break;
239  }
240  }
241 
242  if (miss_some_nodes) {
243  // A circuit that miss a mandatory node is a conflict.
244  if (start_node == end_node) {
245  FillReasonForPath(start_node, trail_->MutableConflict());
246  if (extra_reason != kFalseLiteralIndex) {
247  trail_->MutableConflict()->push_back(Literal(extra_reason));
248  }
249  return false;
250  }
251 
252  // We have an unclosed path. Propagate the fact that it cannot
253  // be closed into a cycle, i.e. not(end_node -> start_node).
254  if (start_node != end_node) {
255  const auto it = graph_.find({end_node, start_node});
256  if (it == graph_.end()) continue;
257  const Literal literal = it->second;
258  if (assignment_.LiteralIsFalse(literal)) continue;
259 
260  std::vector<Literal>* reason = trail_->GetEmptyVectorToStoreReason();
261  FillReasonForPath(start_node, reason);
262  if (extra_reason != kFalseLiteralIndex) {
263  reason->push_back(Literal(extra_reason));
264  }
265  const bool ok = trail_->EnqueueWithStoredReason(literal.Negated());
266  if (!ok) return false;
267  continue;
268  }
269  }
270 
271  // If we have a cycle, we can propagate all the other nodes to point to
272  // themselves. Otherwise there is nothing else to do.
273  if (start_node != end_node) continue;
274  if (options_.multiple_subcircuit_through_zero) continue;
275  BooleanVariable variable_with_same_reason = kNoBooleanVariable;
276  for (int node = 0; node < num_nodes_; ++node) {
277  if (in_current_path_[node]) continue;
278  if (assignment_.LiteralIsTrue(self_arcs_[node])) continue;
279 
280  // This shouldn't happen because ExactlyOnePerRowAndPerColumn() should
281  // have executed first and propagated self_arcs_[node] to false.
282  CHECK_EQ(next_[node], -1);
283 
284  // We should have detected that above (miss_some_nodes == true). But we
285  // still need this for corner cases where the same literal is used for
286  // many arcs, and we just propagated it here.
287  if (assignment_.LiteralIsFalse(self_arcs_[node])) {
288  FillReasonForPath(start_node, trail_->MutableConflict());
289  trail_->MutableConflict()->push_back(self_arcs_[node]);
290  return false;
291  }
292 
293  // Propagate.
294  const Literal literal(self_arcs_[node]);
295  if (variable_with_same_reason == kNoBooleanVariable) {
296  variable_with_same_reason = literal.Variable();
297  FillReasonForPath(start_node, trail_->GetEmptyVectorToStoreReason());
298  const bool ok = trail_->EnqueueWithStoredReason(literal);
299  if (!ok) return false;
300  } else {
301  trail_->EnqueueWithSameReasonAs(literal, variable_with_same_reason);
302  }
303  }
304  }
305  return true;
306 }
307 
309  std::vector<std::vector<Literal>> graph,
310  const std::vector<int>& distinguished_nodes, Model* model)
311  : graph_(std::move(graph)),
312  num_nodes_(graph_.size()),
313  trail_(model->GetOrCreate<Trail>()) {
314  node_is_distinguished_.resize(num_nodes_, false);
315  for (const int node : distinguished_nodes) {
316  node_is_distinguished_[node] = true;
317  }
318 }
319 
321  const int watcher_id = watcher->Register(this);
322 
323  // Fill fixed_arcs_ with arcs that are initially fixed to true,
324  // assign arcs to watch indices.
325  for (int node1 = 0; node1 < num_nodes_; node1++) {
326  for (int node2 = 0; node2 < num_nodes_; node2++) {
327  const Literal l = graph_[node1][node2];
328  if (trail_->Assignment().LiteralIsFalse(l)) continue;
329  if (trail_->Assignment().LiteralIsTrue(l)) {
330  fixed_arcs_.emplace_back(node1, node2);
331  } else {
332  watcher->WatchLiteral(l, watcher_id, watch_index_to_arc_.size());
333  watch_index_to_arc_.emplace_back(node1, node2);
334  }
335  }
336  }
337  watcher->RegisterReversibleClass(watcher_id, this);
338 }
339 
341  if (level == level_ends_.size()) return;
342  if (level > level_ends_.size()) {
343  while (level > level_ends_.size()) {
344  level_ends_.push_back(fixed_arcs_.size());
345  }
346  } else {
347  // Backtrack.
348  fixed_arcs_.resize(level_ends_[level]);
349  level_ends_.resize(level);
350  }
351 }
352 
354  const std::vector<int>& watch_indices) {
355  for (const int w : watch_indices) {
356  const auto& arc = watch_index_to_arc_[w];
357  fixed_arcs_.push_back(arc);
358  }
359  return Propagate();
360 }
361 
362 void CircuitCoveringPropagator::FillFixedPathInReason(
363  int start, int end, std::vector<Literal>* reason) {
364  reason->clear();
365  int current = start;
366  do {
367  DCHECK_NE(next_[current], -1);
368  DCHECK(trail_->Assignment().LiteralIsTrue(graph_[current][next_[current]]));
369  reason->push_back(graph_[current][next_[current]].Negated());
370  current = next_[current];
371  } while (current != end);
372 }
373 
375  // Gather next_ and prev_ from fixed arcs.
376  next_.assign(num_nodes_, -1);
377  prev_.assign(num_nodes_, -1);
378  for (const auto& arc : fixed_arcs_) {
379  // Two arcs go out of arc.first, forbidden.
380  if (next_[arc.first] != -1) {
381  *trail_->MutableConflict() = {
382  graph_[arc.first][next_[arc.first]].Negated(),
383  graph_[arc.first][arc.second].Negated()};
384  return false;
385  }
386  next_[arc.first] = arc.second;
387  // Two arcs come into arc.second, forbidden.
388  if (prev_[arc.second] != -1) {
389  *trail_->MutableConflict() = {
390  graph_[prev_[arc.second]][arc.second].Negated(),
391  graph_[arc.first][arc.second].Negated()};
392  return false;
393  }
394  prev_[arc.second] = arc.first;
395  }
396 
397  // For every node, find partial path/circuit in which the node is.
398  // Use visited_ to visit each path/circuit only once.
399  visited_.assign(num_nodes_, false);
400  for (int node = 0; node < num_nodes_; node++) {
401  // Skip if already visited, isolated or loop.
402  if (visited_[node]) continue;
403  if (prev_[node] == -1 && next_[node] == -1) continue;
404  if (prev_[node] == node) continue;
405 
406  // Find start of path/circuit.
407  int start = node;
408  for (int current = prev_[node]; current != -1 && current != node;
409  current = prev_[current]) {
410  start = current;
411  }
412 
413  // Find distinguished node of path. Fail if there are several,
414  // fail if this is a non loop circuit and there are none.
415  int distinguished = node_is_distinguished_[start] ? start : -1;
416  int current = next_[start];
417  int end = start;
418  visited_[start] = true;
419  while (current != -1 && current != start) {
420  if (node_is_distinguished_[current]) {
421  if (distinguished != -1) {
422  FillFixedPathInReason(distinguished, current,
423  trail_->MutableConflict());
424  return false;
425  }
426  distinguished = current;
427  }
428  visited_[current] = true;
429  end = current;
430  current = next_[current];
431  }
432 
433  // Circuit with no distinguished nodes, forbidden.
434  if (start == current && distinguished == -1) {
435  FillFixedPathInReason(start, start, trail_->MutableConflict());
436  return false;
437  }
438 
439  // Path with no distinguished node: forbid to close it.
440  if (current == -1 && distinguished == -1 &&
441  !trail_->Assignment().LiteralIsFalse(graph_[end][start])) {
442  auto* reason = trail_->GetEmptyVectorToStoreReason();
443  FillFixedPathInReason(start, end, reason);
444  const bool ok =
445  trail_->EnqueueWithStoredReason(graph_[end][start].Negated());
446  if (!ok) return false;
447  }
448  }
449  return true;
450 }
451 
452 std::function<void(Model*)> ExactlyOnePerRowAndPerColumn(
453  const std::vector<std::vector<Literal>>& graph) {
454  return [=](Model* model) {
455  const int n = graph.size();
456  std::vector<Literal> exactly_one_constraint;
457  exactly_one_constraint.reserve(n);
458  for (const bool transpose : {false, true}) {
459  for (int i = 0; i < n; ++i) {
460  exactly_one_constraint.clear();
461  for (int j = 0; j < n; ++j) {
462  exactly_one_constraint.push_back(transpose ? graph[j][i]
463  : graph[i][j]);
464  }
465  model->Add(ExactlyOneConstraint(exactly_one_constraint));
466  }
467  }
468  };
469 }
470 
471 std::function<void(Model*)> SubcircuitConstraint(
472  int num_nodes, const std::vector<int>& tails, const std::vector<int>& heads,
473  const std::vector<Literal>& literals,
474  bool multiple_subcircuit_through_zero) {
475  return [=](Model* model) {
476  const int num_arcs = tails.size();
477  CHECK_GT(num_arcs, 0);
478  CHECK_EQ(heads.size(), num_arcs);
479  CHECK_EQ(literals.size(), num_arcs);
480 
481  // If a node has no outgoing or no incoming arc, the model will be unsat
482  // as soon as we add the corresponding ExactlyOneConstraint().
483  auto sat_solver = model->GetOrCreate<SatSolver>();
484 
485  std::vector<std::vector<Literal>> exactly_one_incoming(num_nodes);
486  std::vector<std::vector<Literal>> exactly_one_outgoing(num_nodes);
487  for (int arc = 0; arc < num_arcs; arc++) {
488  const int tail = tails[arc];
489  const int head = heads[arc];
490  exactly_one_outgoing[tail].push_back(literals[arc]);
491  exactly_one_incoming[head].push_back(literals[arc]);
492  }
493  for (int i = 0; i < exactly_one_incoming.size(); ++i) {
494  if (i == 0 && multiple_subcircuit_through_zero) continue;
495  model->Add(ExactlyOneConstraint(exactly_one_incoming[i]));
496  if (sat_solver->IsModelUnsat()) return;
497  }
498  for (int i = 0; i < exactly_one_outgoing.size(); ++i) {
499  if (i == 0 && multiple_subcircuit_through_zero) continue;
500  model->Add(ExactlyOneConstraint(exactly_one_outgoing[i]));
501  if (sat_solver->IsModelUnsat()) return;
502  }
503 
505  options.multiple_subcircuit_through_zero = multiple_subcircuit_through_zero;
506  CircuitPropagator* constraint = new CircuitPropagator(
507  num_nodes, tails, heads, literals, options, model);
508  constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
509  model->TakeOwnership(constraint);
510  };
511 }
512 
513 std::function<void(Model*)> CircuitCovering(
514  const std::vector<std::vector<Literal>>& graph,
515  const std::vector<int>& distinguished_nodes) {
516  return [=](Model* model) {
517  CircuitCoveringPropagator* constraint =
518  new CircuitCoveringPropagator(graph, distinguished_nodes, model);
519  constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
520  model->TakeOwnership(constraint);
521  };
522 }
523 
524 } // namespace sat
525 } // namespace operations_research
tail
int64 tail
Definition: routing_flow.cc:127
operations_research::sat::GenericLiteralWatcher::Register
int Register(PropagatorInterface *propagator)
Definition: integer.cc:1910
map_util.h
VLOG
#define VLOG(verboselevel)
Definition: base/logging.h:978
operations_research::Arc
std::pair< int64, int64 > Arc
Definition: search.cc:3361
operations_research::sat::kNoLiteralIndex
const LiteralIndex kNoLiteralIndex(-1)
operations_research::sat::CircuitCoveringPropagator::SetLevel
void SetLevel(int level) final
Definition: circuit.cc:340
operations_research::sat::GenericLiteralWatcher::RegisterReversibleClass
void RegisterReversibleClass(int id, ReversibleInterface *rev)
Definition: integer.cc:1949
operations_research::sat::SatSolver
Definition: sat_solver.h:58
operations_research::sat::GenericLiteralWatcher::RegisterReversibleInt
void RegisterReversibleInt(int id, int *rev)
Definition: integer.cc:1954
CHECK_GT
#define CHECK_GT(val1, val2)
Definition: base/logging.h:702
operations_research::sat::ExactlyOnePerRowAndPerColumn
std::function< void(Model *)> ExactlyOnePerRowAndPerColumn(const std::vector< std::vector< Literal >> &graph)
Definition: circuit.cc:452
gtl::FindWithDefault
const Collection::value_type::second_type & FindWithDefault(const Collection &collection, const typename Collection::value_type::first_type &key, const typename Collection::value_type::second_type &value)
Definition: map_util.h:26
operations_research
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Definition: dense_doubly_linked_list.h:21
operations_research::sat::ExactlyOneConstraint
std::function< void(Model *)> ExactlyOneConstraint(const std::vector< Literal > &literals)
Definition: sat_solver.h:877
circuit.h
operations_research::sat::CircuitPropagator::IncrementalPropagate
bool IncrementalPropagate(const std::vector< int > &watch_indices) final
Definition: circuit.cc:153
operations_research::sat::VariablesAssignment::LiteralIsTrue
bool LiteralIsTrue(Literal literal) const
Definition: sat_base.h:150
operations_research::sat::CircuitCoveringPropagator::CircuitCoveringPropagator
CircuitCoveringPropagator(std::vector< std::vector< Literal >> graph, const std::vector< int > &distinguished_nodes, Model *model)
Definition: circuit.cc:308
operations_research::sat::Literal::Negated
Literal Negated() const
Definition: sat_base.h:91
sat_solver.h
operations_research::sat::CircuitPropagator
Definition: circuit.h:44
operations_research::sat::GenericLiteralWatcher
Definition: integer.h:1091
operations_research::sat::SubcircuitConstraint
std::function< void(Model *)> SubcircuitConstraint(int num_nodes, const std::vector< int > &tails, const std::vector< int > &heads, const std::vector< Literal > &literals, bool multiple_subcircuit_through_zero)
Definition: circuit.cc:471
DCHECK_NE
#define DCHECK_NE(val1, val2)
Definition: base/logging.h:886
operations_research::Assignment
An Assignment is a variable -> domains mapping, used to report solutions to the user.
Definition: constraint_solver.h:5033
operations_research::sat::CircuitPropagator::RegisterWith
void RegisterWith(GenericLiteralWatcher *watcher)
Definition: circuit.cc:92
operations_research::sat::GenericLiteralWatcher::NotifyThatPropagatorMayNotReachFixedPointInOnePass
void NotifyThatPropagatorMayNotReachFixedPointInOnePass(int id)
Definition: integer.cc:1940
operations_research::sat::Trail::Assignment
const VariablesAssignment & Assignment() const
Definition: sat_base.h:380
operations_research::sat::kFalseLiteralIndex
const LiteralIndex kFalseLiteralIndex(-3)
CHECK_EQ
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
operations_research::sat::Literal::Index
LiteralIndex Index() const
Definition: sat_base.h:84
operations_research::sat::Trail::EnqueueWithSameReasonAs
void EnqueueWithSameReasonAs(Literal true_literal, BooleanVariable reference_var)
Definition: sat_base.h:272
operations_research::sat::Model
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
operations_research::sat::CircuitCoveringPropagator::Propagate
bool Propagate() final
Definition: circuit.cc:374
operations_research::sat::CircuitCovering
std::function< void(Model *)> CircuitCovering(const std::vector< std::vector< Literal >> &graph, const std::vector< int > &distinguished_nodes)
Definition: circuit.cc:513
operations_research::sat::kNoBooleanVariable
const BooleanVariable kNoBooleanVariable(-1)
DCHECK
#define DCHECK(condition)
Definition: base/logging.h:884
operations_research::sat::CircuitCoveringPropagator
Definition: circuit.h:131
operations_research::sat::Trail::MutableConflict
std::vector< Literal > * MutableConflict()
Definition: sat_base.h:361
model
GRBmodel * model
Definition: gurobi_interface.cc:269
operations_research::sat::Literal
Definition: sat_base.h:64
operations_research::sat::CircuitPropagator::SetLevel
void SetLevel(int level) final
Definition: circuit.cc:108
operations_research::sat::GenericLiteralWatcher::WatchLiteral
void WatchLiteral(Literal l, int id, int watch_index=-1)
Definition: integer.h:1348
operations_research::sat::CircuitCoveringPropagator::RegisterWith
void RegisterWith(GenericLiteralWatcher *watcher)
Definition: circuit.cc:320
operations_research::sat::CircuitPropagator::Options::multiple_subcircuit_through_zero
bool multiple_subcircuit_through_zero
Definition: circuit.h:49
operations_research::sat::Trail::EnqueueWithStoredReason
ABSL_MUST_USE_RESULT bool EnqueueWithStoredReason(Literal true_literal)
Definition: sat_base.h:284
operations_research::sat::CircuitPropagator::CircuitPropagator
CircuitPropagator(int num_nodes, const std::vector< int > &tails, const std::vector< int > &heads, const std::vector< Literal > &literals, Options options, Model *model)
Definition: circuit.cc:25
operations_research::sat::CircuitPropagator::Options
Definition: circuit.h:46
CHECK_NE
#define CHECK_NE(val1, val2)
Definition: base/logging.h:698
operations_research::sat::CircuitPropagator::Propagate
bool Propagate() final
Definition: circuit.cc:197
head
int64 head
Definition: routing_flow.cc:128
literal
Literal literal
Definition: optimization.cc:84
operations_research::sat::IntegerEncoder::GetFalseLiteral
Literal GetFalseLiteral()
Definition: integer.h:447
operations_research::sat::CircuitCoveringPropagator::IncrementalPropagate
bool IncrementalPropagate(const std::vector< int > &watch_indices) final
Definition: circuit.cc:353
CHECK
#define CHECK(condition)
Definition: base/logging.h:495
operations_research::sat::IntegerEncoder
Definition: integer.h:276
operations_research::sat::VariablesAssignment::LiteralIsFalse
bool LiteralIsFalse(Literal literal) const
Definition: sat_base.h:147
operations_research::sat::Trail
Definition: sat_base.h:233
operations_research::sat::Trail::GetEmptyVectorToStoreReason
std::vector< Literal > * GetEmptyVectorToStoreReason(int trail_index) const
Definition: sat_base.h:320