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