1 /*++ 2 Copyright (c) 2011 Microsoft Corporation 3 4 Module Name: 5 6 sat_scc.cpp 7 8 Abstract: 9 10 Use binary clauses to compute strongly connected components. 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2011-05-26. 15 16 Revision History: 17 18 --*/ 19 #include "sat/sat_scc.h" 20 #include "sat/sat_solver.h" 21 #include "sat/sat_elim_eqs.h" 22 #include "util/stopwatch.h" 23 #include "util/trace.h" 24 #include "sat/sat_scc_params.hpp" 25 26 namespace sat { 27 scc(solver & s,params_ref const & p)28 scc::scc(solver & s, params_ref const & p): 29 m_solver(s), 30 m_big(s.m_rand) { 31 reset_statistics(); 32 updt_params(p); 33 } 34 35 struct frame { 36 unsigned m_lidx; 37 unsigned m_succ_idx; 38 bool m_first; 39 watched * m_it; 40 watched * m_end; framesat::frame41 frame(unsigned lidx, watched * it, watched * end, unsigned sidx = 0):m_lidx(lidx), m_succ_idx(sidx), m_first(true), m_it(it), m_end(end) {} 42 }; 43 typedef svector<frame> frames; 44 45 struct scc::report { 46 scc & m_scc; 47 stopwatch m_watch; 48 unsigned m_num_elim; 49 unsigned m_num_elim_bin; 50 unsigned m_trail_size; reportsat::scc::report51 report(scc & c): 52 m_scc(c), 53 m_num_elim(c.m_num_elim), 54 m_num_elim_bin(c.m_num_elim_bin), 55 m_trail_size(c.m_solver.init_trail_size()) { 56 m_watch.start(); 57 } ~reportsat::scc::report58 ~report() { 59 m_watch.stop(); 60 unsigned elim_bin = m_scc.m_num_elim_bin - m_num_elim_bin; 61 unsigned num_units = m_scc.m_solver.init_trail_size() - m_trail_size; 62 IF_VERBOSE(2, 63 verbose_stream() << " (sat-scc :elim-vars " << (m_scc.m_num_elim - m_num_elim); 64 if (elim_bin > 0) verbose_stream() << " :elim-bin " << elim_bin; 65 if (num_units > 0) verbose_stream() << " :units " << num_units; 66 verbose_stream() << m_watch << ")\n";); 67 } 68 }; 69 operator ()()70 unsigned scc::operator()() { 71 if (m_solver.m_inconsistent) 72 return 0; 73 if (!m_scc) 74 return 0; 75 CASSERT("scc_bug", m_solver.check_invariant()); 76 report rpt(*this); 77 TRACE("scc", m_solver.display(tout);); 78 TRACE("scc_details", m_solver.display_watches(tout);); 79 unsigned_vector index; 80 unsigned_vector lowlink; 81 unsigned_vector s; 82 svector<char> in_s; 83 unsigned num_lits = m_solver.num_vars() * 2; 84 index.resize(num_lits, UINT_MAX); 85 lowlink.resize(num_lits, UINT_MAX); 86 in_s.resize(num_lits, false); 87 literal_vector roots, lits; 88 roots.resize(m_solver.num_vars(), null_literal); 89 unsigned next_index = 0; 90 svector<frame> frames; 91 bool_var_vector to_elim; 92 93 for (unsigned l_idx = 0; l_idx < num_lits; l_idx++) { 94 if (index[l_idx] != UINT_MAX) 95 continue; 96 if (m_solver.was_eliminated(to_literal(l_idx).var())) 97 continue; 98 99 m_solver.checkpoint(); 100 101 #define NEW_NODE(LIDX) { \ 102 index[LIDX] = next_index; \ 103 lowlink[LIDX] = next_index; \ 104 next_index++; \ 105 s.push_back(LIDX); \ 106 in_s[LIDX] = true; \ 107 watch_list & wlist = m_solver.get_wlist(LIDX); \ 108 frames.push_back(frame(LIDX, wlist.begin(), wlist.end())); \ 109 } 110 111 NEW_NODE(l_idx); 112 113 while (!frames.empty()) { 114 loop: 115 frame & fr = frames.back(); 116 unsigned l_idx = fr.m_lidx; 117 if (!fr.m_first) { 118 SASSERT(fr.m_it->is_binary_clause()); 119 // after visiting child 120 literal l2 = fr.m_it->get_literal(); 121 unsigned l2_idx = l2.index(); 122 SASSERT(index[l2_idx] != UINT_MAX); 123 if (lowlink[l2_idx] < lowlink[l_idx]) 124 lowlink[l_idx] = lowlink[l2_idx]; 125 fr.m_it++; 126 } 127 fr.m_first = false; 128 while (fr.m_it != fr.m_end) { 129 if (!fr.m_it->is_binary_clause()) { 130 fr.m_it++; 131 continue; 132 } 133 literal l2 = fr.m_it->get_literal(); 134 unsigned l2_idx = l2.index(); 135 if (index[l2_idx] == UINT_MAX) { 136 NEW_NODE(l2_idx); 137 goto loop; 138 } 139 else if (in_s[l2_idx]) { 140 if (index[l2_idx] < lowlink[l_idx]) 141 lowlink[l_idx] = index[l2_idx]; 142 } 143 fr.m_it++; 144 } 145 // visited all successors 146 if (lowlink[l_idx] == index[l_idx]) { 147 // found new SCC 148 CTRACE("scc_cycle", s.back() != l_idx, { 149 tout << "cycle: "; 150 unsigned j = s.size() - 1; 151 unsigned l2_idx; 152 do { 153 l2_idx = s[j]; 154 j--; 155 tout << to_literal(l2_idx) << " "; 156 } while (l2_idx != l_idx); 157 tout << "\n"; 158 }); 159 160 SASSERT(!s.empty()); 161 literal l = to_literal(l_idx); 162 bool_var v = l.var(); 163 if (roots[v] != null_literal) { 164 // variable was already assigned... just consume stack 165 TRACE("scc_detail", tout << "consuming stack...\n";); 166 unsigned l2_idx; 167 do { 168 l2_idx = s.back(); 169 s.pop_back(); 170 in_s[l2_idx] = false; 171 SASSERT(roots[to_literal(l2_idx).var()].var() == roots[v].var()); 172 } while (l2_idx != l_idx); 173 } 174 else { 175 // check if the SCC has an external variable, and check for conflicts 176 TRACE("scc_detail", tout << "assigning roots...\n";); 177 literal r = null_literal; 178 unsigned j = s.size() - 1; 179 unsigned l2_idx; 180 do { 181 l2_idx = s[j]; 182 j--; 183 if (to_literal(l2_idx) == ~l) { 184 m_solver.set_conflict(); 185 return 0; 186 } 187 if (m_solver.is_external(to_literal(l2_idx).var())) { 188 r = to_literal(l2_idx); 189 break; 190 } 191 } while (l2_idx != l_idx); 192 193 if (r == null_literal) { 194 // SCC does not contain external variable 195 r = to_literal(l_idx); 196 } 197 198 TRACE("scc_detail", tout << "r: " << r << "\n";); 199 200 do { 201 l2_idx = s.back(); 202 s.pop_back(); 203 in_s[l2_idx] = false; 204 literal l2 = to_literal(l2_idx); 205 bool_var v2 = l2.var(); 206 207 if (roots[v2] == null_literal) { 208 if (l2.sign()) { 209 roots[v2] = ~r; 210 } 211 else { 212 roots[v2] = r; 213 } 214 if (v2 != r.var()) 215 to_elim.push_back(v2); 216 } 217 } while (l2_idx != l_idx); 218 } 219 } 220 frames.pop_back(); 221 } 222 } 223 224 for (unsigned i = 0; i < m_solver.num_vars(); ++i) { 225 if (roots[i] == null_literal) { 226 roots[i] = literal(i, false); 227 } 228 } 229 TRACE("scc", for (unsigned i = 0; i < roots.size(); i++) { tout << i << " -> " << roots[i] << "\n"; } 230 tout << "to_elim: "; for (unsigned v : to_elim) tout << v << " "; tout << "\n";); 231 m_num_elim += to_elim.size(); 232 elim_eqs eliminator(m_solver); 233 eliminator(roots, to_elim); 234 TRACE("scc_detail", m_solver.display(tout);); 235 CASSERT("scc_bug", m_solver.check_invariant()); 236 237 if (m_scc_tr) { 238 reduce_tr(); 239 } 240 TRACE("scc_detail", m_solver.display(tout);); 241 return to_elim.size(); 242 } 243 reduce_tr(bool learned)244 unsigned scc::reduce_tr(bool learned) { 245 init_big(learned); 246 unsigned num_elim = m_big.reduce_tr(m_solver); 247 m_num_elim_bin += num_elim; 248 return num_elim; 249 } 250 reduce_tr()251 void scc::reduce_tr() { 252 unsigned quota = 0, num_reduced = 0, count = 0; 253 while ((num_reduced = reduce_tr(false)) > quota && count++ < 10) { quota = std::max(100u, num_reduced / 2); } 254 quota = 0; count = 0; 255 while ((num_reduced = reduce_tr(true)) > quota && count++ < 10) { quota = std::max(100u, num_reduced / 2); } 256 } 257 collect_statistics(statistics & st) const258 void scc::collect_statistics(statistics & st) const { 259 st.update("sat scc elim vars", m_num_elim); 260 st.update("sat scc elim binary", m_num_elim_bin); 261 } 262 reset_statistics()263 void scc::reset_statistics() { 264 m_num_elim = 0; 265 m_num_elim_bin = 0; 266 } 267 updt_params(params_ref const & _p)268 void scc::updt_params(params_ref const & _p) { 269 sat_scc_params p(_p); 270 m_scc = p.scc(); 271 m_scc_tr = p.scc_tr(); 272 } 273 collect_param_descrs(param_descrs & d)274 void scc::collect_param_descrs(param_descrs & d) { 275 sat_scc_params::collect_param_descrs(d); 276 } 277 278 }; 279