18 #include "absl/container/flat_hash_map.h"
26 const std::vector<int>& tails,
27 const std::vector<int>& heads,
28 const std::vector<Literal>& literals,
30 : num_nodes_(num_nodes),
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;
41 const int num_arcs = tails.size();
42 graph_.reserve(num_arcs);
43 self_arcs_.resize(num_nodes_,
45 for (
int arc = 0; arc < num_arcs; ++arc) {
46 const int head = heads[arc];
47 const int tail = tails[arc];
58 if (next_[
tail] != -1 || prev_[
head] != -1) {
59 VLOG(1) <<
"Trivially UNSAT or duplicate arcs while adding " <<
tail
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>());
78 watch_index_to_arcs_[watch_index].push_back({
tail,
head});
81 for (
int node = 0; node < num_nodes_; ++node) {
86 must_be_in_cycle_[rev_must_be_in_cycle_size_++] = node;
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);
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());
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;
123 added_arcs_.resize(level_ends_[level]);
124 level_ends_.resize(level);
127 void CircuitPropagator::FillReasonForPath(
int start_node,
128 std::vector<Literal>* reason)
const {
131 int node = start_node;
132 while (next_[node] != -1) {
134 reason->push_back(
Literal(next_literal_[node]).Negated());
137 if (node == start_node)
break;
143 void CircuitPropagator::AddArc(
int tail,
int head, LiteralIndex literal_index) {
146 next_literal_[
tail] = literal_index;
154 const std::vector<int>& watch_indices) {
155 for (
const int w : watch_indices) {
157 for (
const Arc arc : watch_index_to_arcs_[w]) {
159 if (arc.tail == arc.head) {
160 must_be_in_cycle_[rev_must_be_in_cycle_size_++] = arc.tail;
166 if (next_[arc.tail] != -1) {
172 *conflict = {
literal.Negated()};
176 if (prev_[arc.head] != -1) {
182 *conflict = {
literal.Negated()};
188 AddArc(arc.tail, arc.head,
literal.Index());
189 added_arcs_.push_back(arc);
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;
206 in_current_path_.assign(num_nodes_,
false);
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;
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;
231 bool miss_some_nodes =
false;
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();
242 if (miss_some_nodes) {
244 if (start_node == end_node) {
254 if (start_node != end_node) {
255 const auto it = graph_.find({end_node, start_node});
256 if (it == graph_.end())
continue;
261 FillReasonForPath(start_node, reason);
263 reason->push_back(
Literal(extra_reason));
266 if (!ok)
return false;
273 if (start_node != end_node)
continue;
276 for (
int node = 0; node < num_nodes_; ++node) {
277 if (in_current_path_[node])
continue;
296 variable_with_same_reason =
literal.Variable();
299 if (!ok)
return false;
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()),
314 node_is_distinguished_.resize(num_nodes_,
false);
315 for (
const int node : distinguished_nodes) {
316 node_is_distinguished_[node] =
true;
321 const int watcher_id = watcher->
Register(
this);
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];
330 fixed_arcs_.emplace_back(node1, node2);
332 watcher->
WatchLiteral(l, watcher_id, watch_index_to_arc_.size());
333 watch_index_to_arc_.emplace_back(node1, node2);
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());
348 fixed_arcs_.resize(level_ends_[level]);
349 level_ends_.resize(level);
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);
362 void CircuitCoveringPropagator::FillFixedPathInReason(
363 int start,
int end, std::vector<Literal>* reason) {
369 reason->push_back(graph_[current][next_[current]].Negated());
370 current = next_[current];
371 }
while (current != end);
376 next_.assign(num_nodes_, -1);
377 prev_.assign(num_nodes_, -1);
378 for (
const auto& arc : fixed_arcs_) {
380 if (next_[arc.first] != -1) {
382 graph_[arc.first][next_[arc.first]].Negated(),
383 graph_[arc.first][arc.second].Negated()};
386 next_[arc.first] = arc.second;
388 if (prev_[arc.second] != -1) {
390 graph_[prev_[arc.second]][arc.second].Negated(),
391 graph_[arc.first][arc.second].Negated()};
394 prev_[arc.second] = arc.first;
399 visited_.assign(num_nodes_,
false);
400 for (
int node = 0; node < num_nodes_; node++) {
402 if (visited_[node])
continue;
403 if (prev_[node] == -1 && next_[node] == -1)
continue;
404 if (prev_[node] == node)
continue;
408 for (
int current = prev_[node]; current != -1 && current != node;
409 current = prev_[current]) {
415 int distinguished = node_is_distinguished_[start] ? start : -1;
416 int current = next_[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,
426 distinguished = current;
428 visited_[current] =
true;
430 current = next_[current];
434 if (start == current && distinguished == -1) {
440 if (current == -1 && distinguished == -1 &&
443 FillFixedPathInReason(start, end, reason);
446 if (!ok)
return false;
453 const std::vector<std::vector<Literal>>& graph) {
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]
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) {
476 const int num_arcs = tails.size();
479 CHECK_EQ(literals.size(), num_arcs);
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]);
493 for (
int i = 0; i < exactly_one_incoming.size(); ++i) {
494 if (i == 0 && multiple_subcircuit_through_zero)
continue;
496 if (sat_solver->IsModelUnsat())
return;
498 for (
int i = 0; i < exactly_one_outgoing.size(); ++i) {
499 if (i == 0 && multiple_subcircuit_through_zero)
continue;
501 if (sat_solver->IsModelUnsat())
return;
507 num_nodes, tails, heads, literals, options,
model);
509 model->TakeOwnership(constraint);
514 const std::vector<std::vector<Literal>>& graph,
515 const std::vector<int>& distinguished_nodes) {
520 model->TakeOwnership(constraint);