logo

Journals Books
Advanced Search
Sign in Register

中文

SCIENCE CHINA Information Sciences
Download PDF
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

Jie LUO *, Shaofan LIU
More info
  • ReceivedJan 11, 2019
  • AcceptedApr 19, 2019
  • PublishedOct 9, 2019
Previous Table of Contents Next
Share
Rating

Abstract


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

  • Click to view Download high-quality image

    Figure 1

    (Color online) Modularity of inconsistency graph partitioning.

  • Click to view Download high-quality image

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