[1] Nam G J,Aloul F,Sakallah K,et al.A comparative study of two Boolean formulations of FPGA detailed routing constraints[A].Proceedings of the 2001 International Symposium on Physical Design[C].Sonoma County,CA,USA:ACM,2001.222-227. [2] Liffiton M H,Mneimneh M N,Lynce I,et al.A branch and bound algorithm for extracting smallest minimal unsatisfiable formulas[J].Constraints,2009,14(4):415-442. [3] 张建民,沈胜宇,李思昆.最小布尔不可满足子式的求解算法[J].电子学报,2009,9(5):993-999. Zhang Jianmin,Shen Shengyu,Li Sikun.Algorithm for deriving minimum unsatisfiable subformulae[J].Acta Electronica Sinca,2009,9(5):993-999.(in Chinese) [4] Oh Y,Mneimneh M N,Andraus Z S,et al.AMUSE:a minimally-unsatisfiable subformula extractor[A].Proceedings of the 41st Design Automation Conference[C].San Diego,CA,USA:ACM,2004.518-523. [5] Li Xiaowei,Li Guanghui,Shao Ming.Formal verification techniques based on Boolean satisfiability problem[J].Journal of Computer Science and Technology,2005,20(1):38-47. [6] Liffiton MH,Sakallah KA.Algorithms for computing minimal unsatisfiable subsets of constraints[J].Journal of Automated Reasoning,2008,40:1-30. [7] 陈振宇,徐宝文,周从华.一种基于消解的变量极小不可满足子公式的提取方法[J].计算机研究与发展,2008,45(s1):43-47. Chen Zhenyu,Xu Baowen,Zhou Conghua.A resolution-based approach for extracting variable minimal unsatisfiable subformulas[J].Journal of Computer Research and Development,2008,45(s1):43-47.(in Chinese) [8] 赵相福,欧阳丹彤.使用SAT求解器产生所有极小冲突部件集[J].电子学报,2009,37(4):804-810. Zhao Xiangfu,Ouyang Dantong.Deriving all minimal conflict sets using satisfiability algorithms[J].Acta Electronica Sinica,2009,37(4):804-810.(in Chinese) [9] Nadel A.Boosting minimal unsatisfiable core extraction[A].Proceedings of the 10th International Conference on Formal Methods in Computer Aided Design[C].Lugano,Switzerland:IEEE,2010.221-229. [10] Marques-Silva J,Lynce I.Onimproving MUS extraction algorithms[A].Proceedings of the 14th International Conference on Theory and Applications of Satisfiability Testing[C].Ann Arbor,MI,USA:Springer,2011.159-173. [11] Belov A,Lynce I,Marques-Silva J.Towards efficient MUS extraction[J].Journal AI Communications,2012,25(2):97-116. [12] Nadel A,Ryvchin V,Strichman O.Efficient MUS extraction with resolution[A].Proceedings of the 13th International Conference Formal Methods in Computer Aided Design[C].Portland,OR,USA:IEEE,2013.197-200. [13] Marques-Silva J,Previti A.On computing preferred MUSes and MCSes[A].Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing[C].Vienna,Austria:Springer,2014.58-74. [14] Bacchus F,Katsirelos G.Using minimal correction sets to more efficiently compute minimal unsatisfiable sets[A].Proceedings of the 27th International Conference on Computer Aided Verification[C].San Francisco,CA,USA:Springer,2015.70-86. [15] Bacchus F,Katsirelos G.Finding a collection of MUSes incrementally[A].Proceedings of the 13th International Conference on AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems[C].Banff,AB,Canada:Springer,2016.35-44. [16] Zhao W,Liffiton M H.Parallelizing partial MUS enumeration[A].Proceedings of IEEE 28th International Conference on Tools with Artificial Intelligence[C].San Jose,CA,USA:IEEE,2016.464-471. [17] Gregoire E,Izza Y.Boosting MCSes enumeration[A].Proceedings of the 27th International Joint Conference on Artificial Intelligence[C].Stockholm,Sweden:ACM,2018.1309-1315. [18] Narodytska N,Bjorner N,Marinescu M C,et al.Core-guided minimal correction set and core enumeration[A].Proceedings of the 27th International Joint Conference on Artificial Intelligence[C].Stockholm,Sweden:ACM,2018.1353-1361. [19] Liu Shaofan,Luo Jie.FMUS2:An efficient algorithm to compute minimal unsatisfiable subsets[A].Proceedings of 2018 International Conference on Artificial Intelligence and Symbolic Computation[C].Suzhou,China:Springer,2018.104-118. [20] Luo Jie,Liu Shaofan.Accelerating MUS enumeration by inconsistency graph partitioning[J].Science China Information Sciences,2019,62:212104. [21] Mencia C,Kullmann O,Ignatiev A,Marques-Silva J.On computing the union of MUSes[A].Proceedings of 22nd International Conference on Theory and Applications of Satisfiability Testing[C].Lisbon,Portugal:Springer,2019.211-221. [22] Jaroslav B,Kuldeep MS.Approximate counting of minimal unsatisfiable subsets[A].Proceedings of the 32nd International Conference on Computer Aided Verification[C].Los Angeles,CA,USA:Springer,2020.1-23. [23] Jaroslav B,Cerna I.Rotation based MSS/MCS enumeration[A].Proceedings of the 23rd International Conference on Logic for Programming,Artificial Intelligence and Reasoning[C].Alicante,Spain:EasyChair,2020.120-137. [24] Jaroslav B,Cerna I.MUST:minimal unsatisfiable subsets enumeration tool[A].Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems[C].Dublin,Ireland:Springer,2020.135-152. [25] Gallier J H.Logic for Computer Science:Foundations of Automatic Theorem Proving[M].New York:Harper & Row Publishers Inc,2003. |