OR-Tools  8.2
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"
21
22namespace operations_research {
23namespace 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
127void 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].
143void 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
362void 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
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
471std::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
513std::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
#define CHECK(condition)
Definition: base/logging.h:495
#define DCHECK_NE(val1, val2)
Definition: base/logging.h:886
#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 DCHECK(condition)
Definition: base/logging.h:884
#define VLOG(verboselevel)
Definition: base/logging.h:978
An Assignment is a variable -> domains mapping, used to report solutions to the user.
CircuitCoveringPropagator(std::vector< std::vector< Literal > > graph, const std::vector< int > &distinguished_nodes, Model *model)
Definition: circuit.cc:308
bool IncrementalPropagate(const std::vector< int > &watch_indices) final
Definition: circuit.cc:353
void RegisterWith(GenericLiteralWatcher *watcher)
Definition: circuit.cc:320
bool IncrementalPropagate(const std::vector< int > &watch_indices) final
Definition: circuit.cc:153
void RegisterWith(GenericLiteralWatcher *watcher)
Definition: circuit.cc:92
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
void RegisterReversibleClass(int id, ReversibleInterface *rev)
Definition: integer.cc:1978
void WatchLiteral(Literal l, int id, int watch_index=-1)
Definition: integer.h:1365
int Register(PropagatorInterface *propagator)
Definition: integer.cc:1939
LiteralIndex Index() const
Definition: sat_base.h:84
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
std::vector< Literal > * GetEmptyVectorToStoreReason(int trail_index) const
Definition: sat_base.h:320
void EnqueueWithSameReasonAs(Literal true_literal, BooleanVariable reference_var)
Definition: sat_base.h:272
const VariablesAssignment & Assignment() const
Definition: sat_base.h:380
ABSL_MUST_USE_RESULT bool EnqueueWithStoredReason(Literal true_literal)
Definition: sat_base.h:284
std::vector< Literal > * MutableConflict()
Definition: sat_base.h:361
bool LiteralIsTrue(Literal literal) const
Definition: sat_base.h:150
bool LiteralIsFalse(Literal literal) const
Definition: sat_base.h:147
GRBmodel * model
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
const LiteralIndex kFalseLiteralIndex(-3)
const LiteralIndex kNoLiteralIndex(-1)
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
std::function< void(Model *)> CircuitCovering(const std::vector< std::vector< Literal > > &graph, const std::vector< int > &distinguished_nodes)
Definition: circuit.cc:513
std::function< void(Model *)> ExactlyOnePerRowAndPerColumn(const std::vector< std::vector< Literal > > &graph)
Definition: circuit.cc:452
const BooleanVariable kNoBooleanVariable(-1)
std::function< void(Model *)> ExactlyOneConstraint(const std::vector< Literal > &literals)
Definition: sat_solver.h:876
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
std::pair< int64, int64 > Arc
Definition: search.cc:3361
STL namespace.
Literal literal
Definition: optimization.cc:84
int64 tail
int64 head