logo

SCIENCE CHINA Information Sciences, Volume 62 , Issue 11 : 212104(2019) https://doi.org/10.1007/s11432-019-9881-0

Accelerating MUS enumeration by inconsistency graph partitioning

More info
  • ReceivedJan 11, 2019
  • AcceptedApr 19, 2019
  • PublishedOct 9, 2019

Abstract

The problem of finding minimal unsatisfiable subsets (MUSes) has been studied frequently because of itstheoretical importance and wide range of applications in domains such as electronic design automation,software, and integrated circuit verification. In this paper, a method for accelerating theenumeration of MUSes based on inconsistency graph partitioning is proposed. First, an inconsistency graphof a set of clauses is constructed by extracting the inconsistencyrelations between literals of different clauses. In this paper, we show that by partitioning the inconsistency graphinto small connected components through a vertex cut, the enumeration of MUSes in different componentsbecomes independent and it is possible to compute them separately. Moreover, the MUSes of the original clause setcan be constructed by merging the unit clauses in the MUSes of these connected components back into the clauses inthe vertex cut. Experiments show that by integrating the acceleration method into the MARCO MUSes enumerator,there is a 2–3 times improvement in the average runtime of solved instances for randomly generatedbenchmarks. By integrating the acceleration method into itself as an MUS enumerator, there isanother 3–4 times improvement when compared with the accelerated MARCO.


Acknowledgment

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).


References

[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}}$.

  •   

    Algorithm 1 $\text{GPMUS}(\Gamma_S,~\{\Gamma_1,~\ldots,~\Gamma_k\})$

    Require:$\Gamma$ is a clause set whose inconsistency graph is $G$; $\Gamma_S~=~\{A_1,~\ldots,~A_m\}$ is a subset of $\Gamma$ whose corresponding vertex set is a cut of $G$; $\{\Gamma_1,~\ldots,~\Gamma_k\}$ is the set of corresponding clause sets of connected components after a cut.

    Output:The set of all MUSes of $\Gamma$.

    for $i~=~1$ TO $k$

    Compute the set $\mathcal{M}_i$ of all MUSes of $\Gamma_i~\cup~\mathcal{C}(\Gamma_i,~\Gamma_S)$;

    end for

    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$;

    for $i~=~1$ TO $m$

    if $A_i$ is not a unit clause then

    $M_i~:=~\text{Merge}(M_{i-1},~A_i)$;

    else

    $M_i~:=~M_{i-1}$;

    end if

    end for

    return $M_m$.

  • Table 1   Comparison of MARCO with GPMUS+MARCO
    ClassesMARCOGPMUS+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 6 1.85 10.79
    mus200 76 16.93 124.50 44 4.79 69.74
    mus400 182 71.01 279.39 113 20.92 178.60
    mus600 200 300 161 22.03 245.80
    mus800 200 300 186 39.76 281.78
    mus1000 200 300 194 16.02 291.48
  • Table 2   Comparison of GPMUS+MARCO with GPMUS+GPMUS
    ClassesGPMUS+MARCOGPMUS+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 4 0.48 6.47
    mus200 44 4.79 69.74 17 1.58 26.95
    mus400 113 20.92 178.60 35 2.21 54.32
    mus600 161 22.03 245.80 54 4.98 84.63
    mus800 186 39.76 281.78 63 1.55 95.56
    mus1000 194 16.02 291.48 69 2.04 104.83
  •   

    Algorithm 2 $\text{Merge}(M_{i-1},~A_i)$

    Require:$M_{i-1}$ is the set of all MUSes of $\Sigma_{i-1}$; $A_i~=~L^i_1~\lor~\cdots~\lor~L^i_{n_i}$ is a clause.

    Output:The set of all MUSes of $\Sigma_{i}$.

    $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\}$;

    for all $(\Phi_1^i,~\ldots,~\Phi_{n_i}^i)~\in~S_i$

    $\Phi'~:=~\bigcup_{j~=1}^{n_i}~(\Phi^i_j~-~\{L^i_j\})$;

    if literals in $\Phi'$ are all from different clauses then

    $M'_{i}~:=~M'_{i}~\cup~\{\{A_i\}~\cup~\Phi'\}$;

    end if

    end for

    $M_i~:=~\MS(N_{i}~\cup~M'_{i})$;

    return $M_i$.

  •   

    Algorithm 3 $\text{Partition}(G)$

    Require:$G$ is the inconsistency graph of $\Gamma$;

    Output:A vertex cut of $G$.

    $\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$;

    while there exist $K_i$ and $K_j$ that are connected in $G$ do

    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}$;

    if $|\mathcal{C}|~=~1$ then

    Let the unique group in $\mathcal{C}$ be $\Phi$;

    else

    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;

    end if

    Delete all edges in $G$ connect to vertices in $\Phi$;

    $\mathcal{S}~:=~\mathcal{S}~\cup~\Phi$;

    end while

    return $\mathcal{S}$.

Copyright 2020 Science China Press Co., Ltd. 《中国科学》杂志社有限责任公司 版权所有

京ICP备17057255号       京公网安备11010102003388号