mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 05:41:23 +00:00
Code Activity

Some progress on Network Simplex

Browse source
This commit is contained in:
Phan Anh Dung 2013-10-24 09:50:12 +02:00
parent 1ff373072d
commit be81e77c70
2 changed files with 50 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

49
src/smt/theory_diff_logic.h
View file

@ -397,33 +397,54 @@ namespace smt {
// Denote costs c_ij on edge (i, j) // Denote costs c_ij on edge (i, j)
vector<rational> m_costs; vector<rational> m_costs;
// Denote supply/demand b_i on node i // Denote supply/demand b_i on node i
vector<rational> m_capacities; vector<rational> m_potentials;
// Keep optimal solution of the min cost flow problem // Keep optimal solution of the min cost flow problem
inf_rational m_objective; inf_rational m_objective;
// Data structure of spanning trees
svector<dl_var> m_pred;
svector<int> m_depth;
svector<dl_var> m_thread;
public: public:
// Create a spanning tree using Kruskal algorithm // Initialize the network with a feasible spanning tree
virtual svector<edge_id> & create_spanning_tree(); virtual void initialize();
virtual void compute_potentials();
virtual void compute_flows();
// A spanning tree is a basis in network simplex.
// Check whether the edges' associated costs could be reduced
virtual rational calculate_reduced_costs(svector<edge_id> & spanning_tree);
// If all reduced costs are non-negative, the current flow is optimal // If all reduced costs are non-negative, the current flow is optimal
virtual bool is_optimal(svector<edge_id> & spanning_tree); // If not optimal, return a violated edge in the corresponding variable
virtual bool is_optimal(edge_id & violated_edge);
// Choose an edge with negative reduced cost
virtual edge_id choose_entering_edge();
// Send as much flow as possible around the cycle, the first basic edge with flow 0 will leave // Send as much flow as possible around the cycle, the first basic edge with flow 0 will leave
edge_id choose_leaving_edge(); virtual edge_id choose_leaving_edge();
virtual void update_tree(edge_id entering_edge, edge_id leaving_edge);
virtual bool is_unbounded(); virtual bool is_unbounded();
// Compute the optimal solution
virtual void compute_solution();
// Minimize cost flows // Minimize cost flows
// Return true if found an optimal solution, and return false if unbounded // Return true if found an optimal solution, and return false if unbounded
virtual bool minimize(); bool minimize() {
initialize();
compute_potentials();
compute_flows();
edge_id entering_edge;
while (!is_optimal(entering_edge)) {
edge_id leaving_edge = choose_leaving_edge();
update_tree(entering_edge, leaving_edge);
if (is_unbounded())
return false;
}
return true;
}
}; };
/* Notes: /* Notes:
@ -432,7 +453,7 @@ namespace smt {
and another function to convert from min cost flow solution to DL solution. and another function to convert from min cost flow solution to DL solution.
It remains unclear how to convert DL assignment to a basic feasible solution of Network Simplex. It remains unclear how to convert DL assignment to a basic feasible solution of Network Simplex.
A naive approach is to run Kruskal in order to get a spanning tree. A naive approach is to run an algorithm on max flow in order to get a spanning tree.
The network_simplex class hasn't had multiple pivoting strategies yet. The network_simplex class hasn't had multiple pivoting strategies yet.
*/ */

29
src/smt/theory_diff_logic_def.h
View file

@ -1038,8 +1038,8 @@ void theory_diff_logic<Ext>::internalize_objective(app * n, objective_term & obj
// Compile term into objective_term format // Compile term into objective_term format
rational r; rational r;
if (m_util.is_numeral(n, r)) { if (m_util.is_numeral(n, r)) {
theory_var v = mk_num(n, r); theory_var v = mk_num(n, r);
objective.push_back(std::make_pair(v, r)); objective.push_back(std::make_pair(v, r));
} }
else if (m_util.is_add(n)) { else if (m_util.is_add(n)) {
for (unsigned i = 0; i < n->get_num_args(); ++i) { for (unsigned i = 0; i < n->get_num_args(); ++i) {
@ -1047,22 +1047,23 @@ void theory_diff_logic<Ext>::internalize_objective(app * n, objective_term & obj
}; };
} }
else if (m_util.is_mul(n)) { else if (m_util.is_mul(n)) {
SASSERT(n->get_num_args() == 2); SASSERT(n->get_num_args() == 2);
rational r; rational r;
app * lhs = to_app(n->get_arg(0)); app * lhs = to_app(n->get_arg(0));
app * rhs = to_app(n->get_arg(1)); app * rhs = to_app(n->get_arg(1));
SASSERT(m_util.is_numeral(lhs, r) || m_util.is_numeral(rhs, r)); SASSERT(m_util.is_numeral(lhs, r) || m_util.is_numeral(rhs, r));
if (!m_util.is_numeral(lhs, r)) if (!m_util.is_numeral(lhs, r))
std::swap(lhs, rhs); std::swap(lhs, rhs);
m_util.is_numeral(lhs, r);
theory_var v = mk_var(rhs); m_util.is_numeral(lhs, r);
objective.push_back(std::make_pair(v, r)); theory_var v = mk_var(rhs);
objective.push_back(std::make_pair(v, r));
} }
else { else {
theory_var v = mk_var(n); theory_var v = mk_var(n);
rational r(1); rational r(1);
objective.push_back(std::make_pair(v, r)); objective.push_back(std::make_pair(v, r));
} }
} }