From acb26d0cf9ce675d816f74d0f4b8446c2c0c767d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 4 Nov 2013 16:00:50 -0800 Subject: [PATCH] review of network flow Signed-off-by: Nikolaj Bjorner --- src/opt/fu_malik.cpp | 42 +++++++------- src/opt/opt_context.cpp | 1 + src/smt/network_flow.h | 9 ++- src/smt/network_flow_def.h | 111 ++++++++++++++++++++++++++---------- src/smt/smt_farkas_util.cpp | 2 +- 5 files changed, 111 insertions(+), 54 deletions(-) diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp index 10fbc05c5..306b3e579 100644 --- a/src/opt/fu_malik.cpp +++ b/src/opt/fu_malik.cpp @@ -140,28 +140,28 @@ namespace opt { s.push(); fu_malik fm(m, s, soft_constraints); - lbool is_sat = l_true; + lbool is_sat = l_true; do { - is_sat = fm.step(); - } - while (is_sat == l_false); - - if (is_sat == l_true) { - // Get a list of satisfying soft_constraints - model_ref model; - s.get_model(model); - - expr_ref_vector result(m); - for (unsigned i = 0; i < soft_constraints.size(); ++i) { - expr_ref val(m); - VERIFY(model->eval(soft_constraints[i].get(), val)); - if (!m.is_false(val)) { - result.push_back(soft_constraints[i].get()); - } - } - soft_constraints.reset(); - soft_constraints.append(result); - } + is_sat = fm.step(); + } + while (is_sat == l_false); + + if (is_sat == l_true) { + // Get a list of satisfying soft_constraints + model_ref model; + s.get_model(model); + + expr_ref_vector result(m); + for (unsigned i = 0; i < soft_constraints.size(); ++i) { + expr_ref val(m); + VERIFY(model->eval(soft_constraints[i].get(), val)); + if (!m.is_false(val)) { + result.push_back(soft_constraints[i].get()); + } + } + soft_constraints.reset(); + soft_constraints.append(result); + } s.pop(1); } // We are done and soft_constraints has diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index e1b664f4c..fbc2981ca 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -60,6 +60,7 @@ namespace opt { expr_ref_vector fmls_copy(fmls); lbool is_sat; if (!fmls.empty()) { + // TBD: bug when cancel flag is set, fu_malik returns is_sat == l_true instead of l_undef if (is_maxsat_problem()) { is_sat = opt::fu_malik_maxsat(*s, fmls_copy); } diff --git a/src/smt/network_flow.h b/src/smt/network_flow.h index 8d3a9a75b..405b5c7c6 100644 --- a/src/smt/network_flow.h +++ b/src/smt/network_flow.h @@ -77,8 +77,6 @@ namespace smt { svector m_depth; // Store the pointer from node i to the next node in depth-first search order svector m_thread; - // Reverse orders of m_thread - svector m_rev_thread; // Store a final node of the sub tree rooted at node i svector m_final; @@ -115,6 +113,13 @@ namespace smt { bool edge_in_tree(edge_id id) const; bool edge_in_tree(node src, node dst) const; + bool is_ancestor_of(node ancestor, node child) const; + + /** + \brief find node that points to 'n' in m_thread + */ + node find_rev_thread(node n, node ancestor) const; + bool check_well_formed(); public: diff --git a/src/smt/network_flow_def.h b/src/smt/network_flow_def.h index 25ff6ee0c..6fa6ac03e 100644 --- a/src/smt/network_flow_def.h +++ b/src/smt/network_flow_def.h @@ -68,7 +68,6 @@ namespace smt { m_pred.resize(num_nodes); m_depth.resize(num_nodes); m_thread.resize(num_nodes); - m_rev_thread.resize(num_nodes); m_final.resize(num_nodes); m_step = 0; @@ -84,7 +83,6 @@ namespace smt { m_pred[root] = -1; m_depth[root] = 0; m_thread[root] = 0; - m_rev_thread[0] = root; m_final[root] = root - 1; m_potentials[root] = numeral::zero(); @@ -108,7 +106,6 @@ namespace smt { m_depth[i] = 1; m_thread[i] = i + 1; m_final[i] = i; - m_rev_thread[i + 1] = i; m_states[num_edges + i] = BASIS; node src = m_upwards[i] ? i : root; node tgt = m_upwards[i] ? root : i; @@ -128,7 +125,7 @@ namespace smt { TRACE("network_flow", { tout << pp_vector("Predecessors", m_pred, true) << pp_vector("Threads", m_thread); - tout << pp_vector("Reverse Threads", m_rev_thread) << pp_vector("Last Successors", m_final); + tout << pp_vector("Last Successors", m_final); tout << pp_vector("Depths", m_depth) << pp_vector("Upwards", m_upwards); tout << pp_vector("Potentials", m_potentials) << pp_vector("Flows", m_flows); }); @@ -263,12 +260,63 @@ namespace smt { return false; } + template + bool network_flow::is_ancestor_of(node ancestor, node child) const { + for (node n = child; n != -1; n = m_pred[n]) { + // q should be in T_v so swap p and q + if (n == ancestor) { + return true; + } + } + return false; + } + + template + dl_var network_flow::find_rev_thread(node n, node ancestor) const { + while (m_thread[ancestor] != n) { + ancestor = m_thread[ancestor]; + } + return ancestor; + } + + /** + \brief add entering_edge, remove leaving_edge from spanning tree. + + Old tree: + root + / \ + x y + / \ / \ + u w' + | / + v w + / \ \ + z p + \ + q + + New tree: + root + / \ + x y + / \ / \ + u w' + / + v w + / \ \ + z p + \ / + q + + */ + template void network_flow::update_spanning_tree() { node p = m_graph.get_source(m_entering_edge); node q = m_graph.get_target(m_entering_edge); node u = m_graph.get_source(m_leaving_edge); node v = m_graph.get_target(m_leaving_edge); + bool q_upwards = false; // v is parent of u so T_u does not contain root node if (m_pred[u] == v) { @@ -276,13 +324,11 @@ namespace smt { } SASSERT(m_pred[v] == u); - for (node n = p; n != -1; n = m_pred[n]) { - // q should be in T_v so swap p and q - if (n == v) { - std::swap(p, q); - break; - } + if (is_ancestor_of(v, p)) { + std::swap(p, q); + q_upwards = true; } + SASSERT(is_ancestor_of(v, q)); TRACE("network_flow", { tout << "update_spanning_tree: (" << p << ", " << q << ") enters, ("; @@ -291,24 +337,34 @@ namespace smt { // Update m_pred (for nodes in the stem from q to v) - node n = q; - node last = m_pred[v]; // review: m_pred[v] == u holds, so why not 'u'? - node prev = p; - while (n != last && n != -1) { + // Note: m_pred[v] == u + // Initialize m_upwards[q] = q_upwards + + bool prev_upwards = q_upwards; + for (node n = q, prev = p; n != u; ) { + SASSERT(m_pred[n] != u || n == v); // the last processed node is v node next = m_pred[n]; - m_pred[n] = prev; - m_upwards[n] = !m_upwards[prev]; + m_pred[n] = prev; + std::swap(m_upwards[n], prev_upwards); + prev_upwards = !prev_upwards; // flip previous version of upwards. prev = n; n = next; + SASSERT(n != -1); } + // At this point m_pred and m_upwards have been updated. + TRACE("network_flow", tout << pp_vector("Predecessors", m_pred, true) << pp_vector("Upwards", m_upwards);); + + // node x = m_final[p]; node y = m_thread[x]; node z = m_final[q]; - + // ---- + // update m_final. + // Do this before updating data structures node gamma_p = m_pred[m_thread[m_final[p]]]; node gamma_v = m_pred[m_thread[m_final[v]]]; @@ -322,7 +378,7 @@ namespace smt { break; } } - node phi = m_rev_thread[v]; + node phi = find_rev_thread(v, u); node delta = found_final_u ? phi : m_final[u]; TRACE("network_flow", tout << "Graft T_q and T_r'\n";); @@ -333,12 +389,13 @@ namespace smt { m_final[n] = z; } + // + m_thread[x] = q; - m_rev_thread[q] = x; m_thread[z] = y; - m_rev_thread[y] = z; // Increase depths of all children in T_q - last = m_thread[m_final[q]]; + node last = m_thread[m_final[q]]; + // NSB review: depth update looks wrong to me for (node n = q; n != last; n = m_thread[n]) { m_depth[n] += 1 + m_depth[p] - m_depth[q]; } @@ -347,7 +404,6 @@ namespace smt { // Update T_r' m_thread[phi] = theta; - m_rev_thread[theta] = phi; for (node n = u; n != gamma_v && n != -1; n = m_pred[n]) { TRACE("network_flow", tout << "2: m_final[" << n << "] |-> " << delta << "\n";); @@ -387,12 +443,8 @@ namespace smt { m_thread[m_final[q]] = prev; } - for (unsigned i = 0; i < m_thread.size(); ++i) { - m_rev_thread[m_thread[i]] = i; - } - TRACE("network_flow", { - tout << pp_vector("Threads", m_thread, true) << pp_vector("Reverse Threads", m_rev_thread); + tout << pp_vector("Threads", m_thread, true); }); } @@ -530,11 +582,8 @@ namespace smt { svector m_pred; node |-> node svector m_depth; node |-> int svector m_thread; node |-> node - svector m_rev_thread; node |-> node svector m_final; node |-> node - m_thread[m_rev_thread[n]] == n for each node n - Tree is determined by m_pred: - m_pred[root] == -1 - m_pred[n] = m != n for each node n, acyclic until reaching root. @@ -545,6 +594,8 @@ namespace smt { depth-first traversal order. m_final[n] is deepest most node in a sub-tree rooted at n. + + m_upwards direction of edge from i to m_pred[i] m_graph */ diff --git a/src/smt/smt_farkas_util.cpp b/src/smt/smt_farkas_util.cpp index eb854294b..c1a303299 100644 --- a/src/smt/smt_farkas_util.cpp +++ b/src/smt/smt_farkas_util.cpp @@ -11,7 +11,7 @@ Abstract: Author: - Nikolaj Bjorner (nbjorne) 2013-11-2. + Nikolaj Bjorner (nbjorner) 2013-11-2. Revision History: