From 66eda866ca6efa54a1e3cea7666e3e7e2bcb5f1f Mon Sep 17 00:00:00 2001 From: Anh-Dung Phan Date: Mon, 11 Nov 2013 18:23:21 -0800 Subject: [PATCH] Fix bugs on candidate list pivot rule --- src/smt/network_flow.h | 76 ++++++++++++++++++++----------------- src/smt/spanning_tree_def.h | 24 +++++++----- 2 files changed, 57 insertions(+), 43 deletions(-) diff --git a/src/smt/network_flow.h b/src/smt/network_flow.h index 5390f53ea..461312985 100644 --- a/src/smt/network_flow.h +++ b/src/smt/network_flow.h @@ -156,24 +156,29 @@ namespace smt { private: edge_id m_next_edge; svector m_candidates; - unsigned num_candidates; + unsigned m_num_candidates; + unsigned m_minor_step; + unsigned m_current_length; static const unsigned NUM_CANDIDATES = 10; + static const unsigned MINOR_STEP_LIMIT = 5; public: candidate_list_pivot(graph & g, vector & potentials, svector & states, edge_id & enter_id) : pivot_rule_impl(g, potentials, states, enter_id), m_next_edge(0), - num_candidates(NUM_CANDIDATES), - m_candidates(num_candidates) { + m_minor_step(0), + m_current_length(0), + m_num_candidates(NUM_CANDIDATES), + m_candidates(m_num_candidates) { } bool choose_entering_edge() { - if (m_candidates.empty()) { + if (m_current_length == 0 || m_minor_step == MINOR_STEP_LIMIT) { // Build the candidate list unsigned num_edges = m_graph.get_num_edges(); numeral max = numeral::zero(); - unsigned count = 0; + m_current_length = 0; for (unsigned i = m_next_edge; i < m_next_edge + num_edges; ++i) { edge_id id = (i >= num_edges) ? i - num_edges : i; node src = m_graph.get_source(id); @@ -181,16 +186,18 @@ namespace smt { if (m_states[id] != BASIS) { numeral cost = m_potentials[src] - m_potentials[tgt] - m_graph.get_weight(id); if (cost.is_pos()) { - m_candidates[count++] = id; + m_candidates[m_current_length] = id; + ++m_current_length; if (cost > max) { max = cost; m_enter_id = id; } } - if (count >= num_candidates) break; + if (m_current_length >= m_num_candidates) break; } } m_next_edge = m_enter_id; + m_minor_step = 1; if (max.is_pos()) { TRACE("network_flow", { tout << "Found entering edge " << m_enter_id << " between node "; @@ -202,36 +209,37 @@ namespace smt { TRACE("network_flow", tout << "Found no entering edge...\n";); return false; } - else { - numeral max = numeral::zero(); - unsigned last = m_candidates.size(); - for (unsigned i = 0; i < last; ++i) { - edge_id id = m_candidates[i]; - node src = m_graph.get_source(id); - node tgt = m_graph.get_target(id); - if (m_states[id] != BASIS) { - numeral cost = m_potentials[src] - m_potentials[tgt] - m_graph.get_weight(id); - if (cost > max) { - max = cost; - m_enter_id = id; - } - // Remove stale candidates - if (!cost.is_pos()) { - m_candidates[i] = m_candidates[--last]; - } + + ++m_minor_step; + numeral max = numeral::zero(); + for (unsigned i = 0; i < m_current_length; ++i) { + edge_id id = m_candidates[i]; + node src = m_graph.get_source(id); + node tgt = m_graph.get_target(id); + if (m_states[id] != BASIS) { + numeral cost = m_potentials[src] - m_potentials[tgt] - m_graph.get_weight(id); + if (cost > max) { + max = cost; + m_enter_id = id; + } + // Remove stale candidates + if (!cost.is_pos()) { + --m_current_length; + m_candidates[i] = m_candidates[m_current_length]; + --i; } } - if (max.is_pos()) { - TRACE("network_flow", { - tout << "Found entering edge " << m_enter_id << " between node "; - tout << m_graph.get_source(m_enter_id) << " and node " << m_graph.get_target(m_enter_id); - tout << " with reduced cost = " << max << "...\n"; - }); - return true; - } - TRACE("network_flow", tout << "Found no entering edge...\n";); - return false; } + if (max.is_pos()) { + TRACE("network_flow", { + tout << "Found entering edge " << m_enter_id << " between node "; + tout << m_graph.get_source(m_enter_id) << " and node " << m_graph.get_target(m_enter_id); + tout << " with reduced cost = " << max << "...\n"; + }); + return true; + } + TRACE("network_flow", tout << "Found no entering edge...\n";); + return false; }; }; diff --git a/src/smt/spanning_tree_def.h b/src/smt/spanning_tree_def.h index be668d91d..c1e05ba3b 100644 --- a/src/smt/spanning_tree_def.h +++ b/src/smt/spanning_tree_def.h @@ -333,23 +333,29 @@ namespace smt { SASSERT(m_pred[q] == v); SASSERT(is_preorder_traversal(v, get_final(v))); node prev = find_rev_thread(v); - node final_q = get_final(q); - node final_v = get_final(v); - node next = m_thread[final_v]; + node f_q = get_final(q); + node f_v = get_final(v); + node next = m_thread[f_v]; node alpha = find_rev_thread(q); - if (final_q == final_v) { - m_thread[final_q] = v; + if (f_q == f_v) { + SASSERT(f_q != v && alpha != next); + m_thread[f_q] = v; m_thread[alpha] = next; + f_q = alpha; } - else { - node beta = m_thread[final_q]; - m_thread[final_q] = v; + else { + node beta = m_thread[f_q]; + SASSERT(f_q != v && alpha != beta); + m_thread[f_q] = v; m_thread[alpha] = beta; + f_q = f_v; } + SASSERT(prev != q); m_thread[prev] = q; m_pred[v] = q; - SASSERT(is_preorder_traversal(q, get_final(q))); + // Notes: f_q has to be used since m_depth hasn't been updated yet. + SASSERT(is_preorder_traversal(q, f_q)); } /**