1 /*++ 2 Copyright (c) 2016 Microsoft Corporation 3 4 Module Name: 5 6 max_cliques.h 7 8 Abstract: 9 10 Utility for enumerating locally maximal sub cliques. 11 12 Author: 13 14 Nikolaj Bjorner (nbjorner) 2016-11-18 15 16 Notes: 17 18 19 --*/ 20 21 #include "util/vector.h" 22 #include "util/uint_set.h" 23 24 25 template<class T> 26 class max_cliques : public T { 27 using T::negate; 28 29 vector<unsigned_vector> m_next, m_tc; 30 uint_set m_reachable[2]; 31 uint_set m_seen1, m_seen2; 32 unsigned_vector m_todo; 33 get_reachable(unsigned p,uint_set const & goal,uint_set & reachable)34 void get_reachable(unsigned p, uint_set const& goal, uint_set& reachable) { 35 m_seen1.reset(); 36 m_todo.reset(); 37 m_todo.push_back(p); 38 for (unsigned i = 0; i < m_todo.size(); ++i) { 39 p = m_todo[i]; 40 if (m_seen1.contains(p)) { 41 continue; 42 } 43 m_seen1.insert(p); 44 if (m_seen2.contains(p)) { 45 unsigned_vector const& tc = m_tc[p]; 46 for (unsigned j = 0; j < tc.size(); ++j) { 47 unsigned np = tc[j]; 48 if (goal.contains(np)) { 49 reachable.insert(np); 50 } 51 } 52 } 53 else { 54 unsigned np = negate(p); 55 if (goal.contains(np)) { 56 reachable.insert(np); 57 } 58 m_todo.append(next(np)); 59 } 60 } 61 for (unsigned i = m_todo.size(); i > 0; ) { 62 --i; 63 p = m_todo[i]; 64 if (m_seen2.contains(p)) { 65 continue; 66 } 67 m_seen2.insert(p); 68 unsigned np = negate(p); 69 unsigned_vector& tc = m_tc[p]; 70 if (goal.contains(np)) { 71 tc.push_back(np); 72 } 73 else { 74 unsigned_vector const& succ = next(np); 75 for (unsigned j = 0; j < succ.size(); ++j) { 76 tc.append(m_tc[succ[j]]); 77 } 78 } 79 } 80 } 81 82 83 84 85 next(unsigned vertex)86 unsigned_vector const& next(unsigned vertex) const { return m_next[vertex]; } 87 88 public: max_cliques()89 max_cliques() {} 90 add_edge(unsigned src,unsigned dst)91 void add_edge(unsigned src, unsigned dst) { 92 m_next.reserve(std::max(src, dst) + 1); 93 m_next.reserve(std::max(negate(src), negate(dst)) + 1); 94 m_next[src].push_back(dst); 95 m_next[dst].push_back(src); 96 } 97 cliques(unsigned_vector const & ps,vector<unsigned_vector> & cliques)98 void cliques(unsigned_vector const& ps, vector<unsigned_vector>& cliques) { 99 unsigned max = 0; 100 unsigned num_ps = ps.size(); 101 for (unsigned i = 0; i < num_ps; ++i) { 102 unsigned p = ps[i]; 103 unsigned np = negate(p); 104 max = std::max(max, std::max(np, p) + 1); 105 } 106 m_next.reserve(max); 107 m_tc.reserve(m_next.size()); 108 unsigned_vector clique; 109 uint_set vars; 110 for (unsigned i = 0; i < num_ps; ++i) { 111 vars.insert(ps[i]); 112 } 113 114 while (!vars.empty()) { 115 clique.reset(); 116 bool turn = false; 117 m_reachable[turn] = vars; 118 while (!m_reachable[turn].empty()) { 119 unsigned p = *m_reachable[turn].begin(); 120 m_reachable[turn].remove(p); 121 vars.remove(p); 122 clique.push_back(p); 123 if (m_reachable[turn].empty()) { 124 break; 125 } 126 m_reachable[!turn].reset(); 127 get_reachable(p, m_reachable[turn], m_reachable[!turn]); 128 turn = !turn; 129 } 130 if (clique.size() > 1) { 131 if (clique.size() == 2 && clique[0] == negate(clique[1])) { 132 // no op 133 } 134 else { 135 cliques.push_back(clique); 136 } 137 } 138 } 139 } 140 141 142 }; 143