Bellman-Ford don't try to return as many cycles

1 files changed, 71 insertions, 123 deletions

diff --git a/src/theory/arith/idl/idl_extension.cpp b/src/theory/arith/idl/idl_extension.cpp
index 5682c0b75..b3b435fa3 100644
--- a/src/theory/arith/idl/idl_extension.cpp
+++ b/src/theory/arith/idl/idl_extension.cpp
@@ -344,45 +344,17 @@ void IdlExtension::processAssertion(TNode assertion)
 }
 
 
-// Getting a solid set of conflicts out of this is really annoying. What we
-// _really_ want is to return a set of negative-weight cycles such that any
-// other negative cycle completely contains one of the ones in our set. But
-// it's not obvious how to do that.
-//
-// The overall idea so far is to get as many small conflicts here as possible,
-// so the SAT solver (and the other theories) are more constrained, i.e., we
-// don't have to keep going into the theory solvers as much, i.e., we're as
-// eager as possible/reasonable with the SAT encoding.
-//
-// What I think is relatively easy to do is find a set of cycles such that any
-// other negative-weight cycle reaches one of them (basically, Bellman-Ford and
-// then trace back from each node that was updated in the final iteration). But
-// the problem with that is that for constraints like (<= x 0) (>= x 1) (<= y
-// 10) (>= y 11), all of the cycles overlap with the skolem_0 node so only a
-// single cycle will ever be produced.
-//
-// Another issue is if we have equality constraints, they get rewritten into
-// two different paths, whereas the cycle-finding will only find one of them.
-// But I think that's a constant overhead (and maybe the solver will keep them
-// 'paired' anyways so it actually doesn't have overhead?).
-//
-// So the approach taken below is as follows:
-// 1. Run Bellman-Ford |V| times, keeping a list of nodes touched on the final
-//    iteration.
-// 2. From those nodes, trace back non-intersecting negative cycles.
-// 3. From each of those cycles, pick the lowest-degree node and mark it
-//    'removed.' (Do lowest-degree so, e.g., the zero node is never removed. We
-//    want as many cycles as possible.)
-// 4. Repeat from (1), except ignoring the nodes marked 'removed.' Finish when
-//    no negative cycles are found.
-//
-// Now a problem is that we find cycles like A->B->C->D->A, then A->C->D->A,
-// etc.
+// From different attempts:
+// 1. Reporting more cycles here doesn't necessarily help (and can often hurt).
+//    Hence moving to Floyd-Warshall where we only return one.
+// 2. Bellman-Ford stops early on sat, but has worst-case on unsat.
+//    Floyd-Warshall is the opposite. It seems to be more important to stop
+//    early on unsat, because (roughly) all but the last theory propagation is
+//    going to be unsat.
 std::vector<std::vector<TNode>> IdlExtension::negativeCycles()
 {
-  std::vector<bool> ignored(d_numVars, false);
+  std::vector<std::vector<TNode>> cycles;
   Rational zero = Rational();
-  std::vector<std::vector<TNode>> conflict_cycles;
 
   std::vector<std::pair<size_t, size_t>> edges;
   for (size_t i = 0; i < d_numVars; i++) {
@@ -391,100 +363,76 @@ std::vector<std::vector<TNode>> IdlExtension::negativeCycles()
       edges.push_back(std::make_pair(i, j));
     }
   }
-  for (size_t _t = 0; _t < 5; _t++) { // Essentially a timeout
-    // Setup
-    std::vector<Rational> distance(d_numVars, Rational());
-    std::vector<size_t> predecessor(d_numVars, 0);
-    for (size_t i = 0; i < d_numVars; i++) {
-      predecessor[i] = i;
-    }
-    std::vector<size_t> degree(d_numVars, 0);
-    std::vector<std::pair<size_t, size_t>> sub_edges;
-    for (const auto &edge : edges) {
-      if (ignored[edge.first] || ignored[edge.second]) continue;
-      sub_edges.push_back(edge);
-      degree[edge.first]++;
-      degree[edge.second]++;
-    }
-    edges = std::move(sub_edges);
-    size_t n_edges = edges.size();
-
-    // Do the actual Bellman-Ford
-    std::set<size_t> reach_cycle;
-    for (size_t iter = 0; iter < d_numVars; iter++) {
-      bool any_changed = false;
-      for (size_t e = 0; e < n_edges; e++) {
-        size_t from = edges[e].first,
-               to = edges[e].second;
-        if (distance[to] > distance[from] + d_matrix[from][to]) {
-          if (iter == d_numVars - 1) {
-            reach_cycle.emplace(to);
-          }
-          distance[to] = distance[from] + d_matrix[from][to];
-          predecessor[to] = from;
-          any_changed = true;
+
+  // Setup
+  std::vector<Rational> distance(d_numVars, Rational());
+  std::vector<size_t> predecessor(d_numVars, 0);
+  for (size_t i = 0; i < d_numVars; i++) predecessor[i] = i;
+
+  // Do the actual Bellman-Ford
+  std::set<size_t> reach_cycle;
+  for (size_t iter = 0; iter < d_numVars; iter++) {
+    bool any_changed = false;
+    for (size_t e = 0; e < edges.size(); e++) {
+      size_t from = edges[e].first,
+             to = edges[e].second;
+      if (distance[to] > distance[from] + d_matrix[from][to]) {
+        if (iter == d_numVars - 1) {
+          reach_cycle.emplace(to);
         }
+        distance[to] = distance[from] + d_matrix[from][to];
+        predecessor[to] = from;
+        any_changed = true;
       }
-      if (!any_changed) break;
     }
+    if (!any_changed) return cycles;
+  }
 
-    // Stopping condition
-    if (reach_cycle.empty()) return conflict_cycles;
-
-    // Otherwise, trace back non-intersecting negative cycles, and update the
-    // ignored-set.
-    std::vector<bool> seen(d_numVars, false);
-    for (size_t start_from : reach_cycle) {
-      std::vector<size_t> cycle;
-      std::unordered_map<size_t, size_t> cycle_idx; // var_idx -> cycle_idx
-      cycle.push_back(start_from);
-      cycle_idx[start_from] = 0;
-      seen[start_from] = true;
-      bool abort = false;
-      while (true) {
-        size_t next = predecessor[cycle.back()];
-        if (cycle_idx.count(next)) {
-          cycle.push_back(next);
-          cycle.erase(cycle.begin(), cycle.begin() + cycle_idx[next]);
-          break;
-        } else if (seen[next]) {
-          abort = true;
-          break;
-        } else {
-          seen[next] = true;
-          cycle_idx[next] = cycle.size();
-          cycle.push_back(next);
-        }
-      }
-      if (abort) continue;
-      Assert(cycle.size() >= 2 && cycle.front() == cycle.back());
-
-      // Then get the cycle, and verify that it is indeed negative.
-      Rational weight = Rational();
-      std::vector<TNode> assertion_cycle;
-      for (size_t i = cycle.size(); i --> 1;) {
-        // Edge i -> i - 1.
-        assertion_cycle.push_back(
-            d_matrix_facts[cycle[i]][cycle[i - 1]]);
-        Assert(d_valid[cycle[i]][cycle[i - 1]]);
-        weight += d_matrix[cycle[i]][cycle[i - 1]];
-      }
-      Assert(weight < zero);
-      conflict_cycles.emplace_back(std::move(assertion_cycle));
-
-      // Then ignore the node in the cycle with the least degree.
-      size_t lowest_degree = cycle[0];
-      for (size_t i : cycle) {
-        if (degree[i] < degree[lowest_degree]) {
-          lowest_degree = i;
-        }
+  // Trace back some non-intersecting negative cycles.
+  std::vector<bool> seen(d_numVars, false);
+  for (size_t start_from : reach_cycle) {
+    std::vector<size_t> cycle;
+    std::unordered_map<size_t, size_t> cycle_idx; // var_idx -> cycle_idx
+    cycle.push_back(start_from);
+    cycle_idx[start_from] = 0;
+    seen[start_from] = true;
+    bool abort = false;
+    while (true) {
+      size_t next = predecessor[cycle.back()];
+      if (cycle_idx.count(next)) {
+        cycle.push_back(next);
+        cycle.erase(cycle.begin(), cycle.begin() + cycle_idx[next]);
+        break;
+      } else if (seen[next]) {
+        abort = true;
+        break;
+      } else {
+        seen[next] = true;
+        cycle_idx[next] = cycle.size();
+        cycle.push_back(next);
       }
-      Assert(!ignored[lowest_degree]);
-      ignored[lowest_degree] = true;
     }
-    Assert(!conflict_cycles.empty());
+    if (abort) continue;
+    Assert(cycle.size() >= 2 && cycle.front() == cycle.back());
+
+    // Then get the cycle, and verify that it is indeed negative.
+    Rational weight = Rational();
+    std::vector<TNode> assertion_cycle;
+    for (size_t i = cycle.size(); i --> 1;) {
+      // Edge i -> i - 1.
+      assertion_cycle.push_back(
+          d_matrix_facts[cycle[i]][cycle[i - 1]]);
+      Assert(d_valid[cycle[i]][cycle[i - 1]]);
+      weight += d_matrix[cycle[i]][cycle[i - 1]];
+    }
+    Assert(weight < zero);
+    cycles.emplace_back(std::move(assertion_cycle));
+    // TODO: Breaking early here seems to be a toss-up on whether it helps or
+    // hurts. Should do some more systematic benchmarking.
+    // break;
   }
-  return conflict_cycles;
+  Assert(!cycles.empty());
+  return cycles;
 }
 
 void IdlExtension::printMatrix(const std::vector<std::vector<Rational>>& matrix,