This work was supported by National Natural Science Foundation of China (Grant Nos. 61690202, 61502022) and State Key Laboratory of Software Development Environment (Grant No. SKLSDE-2017ZX-17).
[1] Andraus Z S, Liffiton M H, Sakallah K A. Reveal: a formal verification tool for verilog designs. In: Proceedings of International Conference on Logic for Programming Artificial Intelligence and Reasoning, 2008. 343--352. Google Scholar
[2] Banda M G D L, Stuckey P J, Wazny J. Finding all minimal unsatisfiable subsets. In: Proceedigns of International ACM Sigplan Conference on Principles and Practice of Declarative Programming, Uppsala, 2003. 32--43. Google Scholar
[3] Tong Y, Chen L, Zhou Z. SLADE: A Smart Large-Scale Task Decomposer in Crowdsourcing. IEEE Trans Knowl Data Eng, 2018, 30: 1588-1601 CrossRef Google Scholar
[4] Janota M, Marques-Silva J. cmMUS: a tool for circumscription-based mus membership testing. In: Proceedigns of International Conference on Logic Programming and Nonmonotonic Reasoning, 2011. 266--271. Google Scholar
[5] Luo J, Li W. An algorithm to compute maximal contractions for Horn clauses. Sci China Inf Sci, 2011, 54: 244-257 CrossRef Google Scholar
[6] Luo J. A general framework for computing maximal contractions. Front Comput Sci, 2013, 7: 83-94 CrossRef Google Scholar
[7] Jiang D, Li W, Luo J. A decomposition based algorithm for maximal contractions. Front Comput Sci, 2013, 7: 801-811 CrossRef Google Scholar
[8] Papadimitriou C H, Wolfe D. The complexity of facets resolved. J Comput Syst Sci, 1988, 37: 2-13 CrossRef Google Scholar
[9] Bacchus F, Katsirelos G. Finding a collection of MUSes incrementally. In: Integration of AI and OR Techniques in Constraint Programming. Berlin: Springer, 2016. 35--44. Google Scholar
[10] Ryvchin V, Strichman O. Faster extraction of high-level minimal unsatisfiable cores. In: Proceedings of International Conference on Theory and Applications of Satisfiability Testing, Ann Arbor, 2011. 174--187. Google Scholar
[11] Xiao G H, Ma Y. Inconsistency measurement based on variables in minimal unsatisfiable subsets. In: Proceedings of the 20th European Conference on Artificial Intelligence, Montpellier, 2012. Google Scholar
[12] Hou A. A theory of measurement in diagnosis from first principles. Artificial Intelligence, 1994, 65: 281-328 CrossRef Google Scholar
[13] Bailey J, Stuckey P J. Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In: Proceedings of International Workshop on Practical Aspects of Declarative Languages, 2005. 174--186. Google Scholar
[14] Liffiton M H, Sakallah K A. Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints. J Autom Reasoning, 2008, 40: 1-33 CrossRef Google Scholar
[15] Stern R, Kalech M, Feldman A, et al. Exploring the duality in conflict-directed model-based diagnosis. In: Proceedings of the 26th AAAI Conference on Artificial Intelligence, Toronto, 2012. Google Scholar
[16] Liffiton M H, Previti A, Malik A. Fast, flexible MUS enumeration. Constraints, 2016, 21: 223-250 CrossRef Google Scholar
[17] Previti A, Marques-Silva J. Partial MUS enumeration. In: Proceedings of the 27th AAAI Conference on Artificial Intelligence, 2013. Google Scholar
[18] Kahng A B, Lienig J, Markov I L, et al. VLSI Physical Design: From Graph Partitioning to Timing Closure. Berlin: Springer, 2011. Google Scholar
[19] Schloegel K, Karypis G, Kumar V. Graph partitioning for high-performance scientific simulations. In: Sourcebook of Parallel Computing. San Francisco: Morgan Kaufmann Publishers, 2003. 491--541. Google Scholar
[20] Newman M. Networks: An Introduction. Oxford: Oxford University Press, 2010. Google Scholar
[21] Blondel V D, Guillaume J L, Lambiotte R. Fast unfolding of communities in large networks. J Stat Mech, 2008, 2008(10): P10008 CrossRef ADS arXiv Google Scholar
[22] Newman M E J, Girvan M. Finding and evaluating community structure in networks. Phys Rev E, 2004, 69: 026113 CrossRef PubMed ADS Google Scholar
[23] Newman M E J. From the Cover: Modularity and community structure in networks. Proc Natl Acad Sci USA, 2006, 103: 8577-8582 CrossRef PubMed ADS Google Scholar
Figure 1
(Color online) Modularity of inconsistency graph partitioning.
Figure 2
(Color online) Comparison of MARCO, GPMUS+MARCO, and GPMUS+GPMUS. (a) $N_{\text{TO}}$; (b) $T^-_{\text{Ave}}$;protect łinebreak (c) $T_{\text{Ave}}$.
Compute the set $\mathcal{M}_i$ of all MUSes of $\Gamma_i~\cup~\mathcal{C}(\Gamma_i,~\Gamma_S)$; |
Compute the set $\mathcal{M}_S$ of all MUSes of $\mathcal{L}(\Gamma_S)$; |
$M_0~:=~(\bigcup_{i=1}^{k}~\mathcal{M}_i)~\cup~\mathcal{M}_S$; |
|
$M_i~:=~\text{Merge}(M_{i-1},~A_i)$; |
|
$M_i~:=~M_{i-1}$; |
|
Classes | MARCO | GPMUS+MARCO | |||||
$N_{\text{TO}}$ | $T^-_{\text{Ave}}$ | $T_{\text{Ave}}$ | $N_{\text{TO}}$ | $T^-_{\text{Ave}}$ | $T_{\text{Ave}}$ | ||
mus100 | 12 | 3.71 | 21.48 | ||||
mus200 | 76 | 16.93 | 124.50 | ||||
mus400 | 182 | 71.01 | 279.39 | ||||
mus600 | 200 | – | 300 | ||||
mus800 | 200 | – | 300 | ||||
mus1000 | 200 | – | 300 |
Classes | GPMUS+MARCO | GPMUS+GPMUS | |||||
$N_{\text{TO}}$ | $T^-_{\text{Ave}}$ | $T_{\text{Ave}}$ | $N_{\text{TO}}$ | $T^-_{\text{Ave}}$ | $T_{\text{Ave}}$ | ||
mus100 | 6 | 1.85 | 10.79 | ||||
mus200 | 44 | 4.79 | 69.74 | ||||
mus400 | 113 | 20.92 | 178.60 | ||||
mus600 | 161 | 22.03 | 245.80 | ||||
mus800 | 186 | 39.76 | 281.78 | ||||
mus1000 | 194 | 16.02 | 291.48 |
$M'_{i}~:=~\emptyset$; |
$N_{i}:=~\{\Phi~\mid~\Phi~\in~M_{i-1}~\text{~and~}~\Phi~\cap~\{L^i_1,~\ldots,~L^i_{n_i}\}=\emptyset\}$; |
$S_{i}~:=~\{(\Phi_1^i,~\ldots,~\Phi_{n_i}^i)~\mid~\Phi^i_j~\in~M_{i-1},~L^i_j~\in~\Phi^i_j,~1~\leq~j~\leq~n_i\}$; |
$\Phi'~:=~\bigcup_{j~=1}^{n_i}~(\Phi^i_j~-~\{L^i_j\})$; |
|
$M'_{i}~:=~M'_{i}~\cup~\{\{A_i\}~\cup~\Phi'\}$; |
|
$M_i~:=~\MS(N_{i}~\cup~M'_{i})$; |
$\mathcal{S}~:=~\emptyset$; |
Filter out all clauses in $\Gamma$ that contain pure literals; |
Group vertices of $G$ such that each group is a smallest balanced set; |
Partition $G$ using the Louvain algorithm and obtain connected components $K_1,~\ldots,~K_s$; |
Compute the number $N$ of components that intersect with the corresponding group of each edge vertex; |
Select all groups that have the maximal number $N$ as $\mathcal{C}$; |
|
Let the unique group in $\mathcal{C}$ be $\Phi$; |
|
Compute the number of edges (degree) connecting vertices in each group of $\mathcal{C}$ to other components; |
Select a group $\Phi$ with the maximal degree; |
|
Delete all edges in $G$ connect to vertices in $\Phi$; |
$\mathcal{S}~:=~\mathcal{S}~\cup~\Phi$; |