›› 2013,Vol. 28 ›› Issue (2): 247-254.doi: 10.1007/s11390-013-1326-4

• Special Section on Selected Paper from NPC 2011 • 上一篇    下一篇

基于本地搜索的完全SAT搜索算法

Wen-Sheng Guo1 (郭文生), Member, CCF, ACM, Guo-Wu Yang (杨国武)1, Member, CCF, ACM William N. N. Hung2, Senior Member, IEEE, and Xiaoyu Song3, Senior Member, IEEE   

  • 收稿日期:2012-04-24 修回日期:2012-11-01 出版日期:2013-03-05 发布日期:2013-03-05

Complete Boolean Satisfiability Solving Algorithms Based on Local Search

Wen-Sheng Guo1 (郭文生), Member, CCF, ACM, Guo-Wu Yang (杨国武)1, Member, CCF, ACM William N. N. Hung2, Senior Member, IEEE, and Xiaoyu Song3, Senior Member, IEEE   

  1. 1 School of Computer Science and Engineering, University of Electronic Science and Technology of ChinaChengdu 611731, China;
    2 Synopsys Inc., Mountain View, California 94043, U.S.A.;
    3 Department of Electrical and Computer Engineering, Portland State University, Portland 97207, U.S.A.
  • Received:2012-04-24 Revised:2012-11-01 Online:2013-03-05 Published:2013-03-05
  • Supported by:

    This work was partially supported by the National Natural Science Foundation of China under Grant Nos. 60973016, 61272175, and the National Basic Research 973 Program of China under Grant No. 2010CB328004.

PDF (PC)

2125

布尔满足(SAT)是计算机科学、人工智能和运筹学研究中的著名问题。本文主要解决具有Model RB结构的满足性问题。Model RB与图着色等问题具有相似的结构。本文基于Model RB结构的特性提出了一种转换方式和三个高效的完全SAT求解算法。本文将问题子句转换成图的形式, 并用互斥集和关联集来表示变量之间的关系。通过使用图中的节点权值和团来确定搜索顺序的方式降低搜索深度。结果显示本文的算法在多数Model RB测试基准中比最好的SAT求解器具有更好的性能。特别是对那些大的测试基准, 本文的求解器具有更好的运行效率。

Abstract: Boolean satisfiability (SAT) is a well-known problem in computer science, artificial intelligence, and operations research. This paper focuses on the satisfiability problem ofModel RB structure that is similar to graph coloring problems and others. We propose a translation method and three effective complete SAT solving algorithms based on the characterization of Model RB structure. We translate clauses into a graph with exclusive sets and relative sets. In order to reduce search depth, we determine search order using vertex weights and clique in the graph. The results show that our algorithms are much more effective than the best SAT solvers in numerous Model RB benchmarks, especially in those large benchmark instances.

[1] Cook S A. The complexity of theorem-proving procedures. InProc. the 3rd Symp. Theory of Comput., May 1971, pp.151-158.

[2] Larrabee T. Test pattern generation using Boolean satisfiability.IEEE Trans. CAD, 1992, 11(1): 4-15.

[3] Biere A, Cimatti A, Clarke E M, Fujita M, Zhu Y. Symbolicmodel checking using SAT procedures instead of BDDs. InProc. the 36th Conf. Design Automation, June 1999, pp.317-320.

[4] Bjesse P, Leonard T, Mokkedem A. Finding bugs in an Alphamicroprocessor using satisfiability solvers. In Lecture Notes inComputer Science 2102, Berry G, Comon H, Finkel A (eds.),Springer-Verlag, 2001, pp.454-464.

[5] Hung W N N, Narasimhan N. Reference model based RTLverification: An integrated approach. In Proc. the 9thHLDVT, November 2004, pp.9-13.

[6] Hung W N N, Song X, Yang G, Yang J, Perkowski M. Optimalsynthesis of multiple output Boolean functions using aset of quantum gates by symbolic reachability analysis. IEEETrans. CAD, 2006, 25(9): 1652-1663.

[7] Hung W N N, Gao C, Song X, Hammerstrom D. Defect tolerantCMOL cell assignment via satisfiability. IEEE SensorsJournal, 2008, 8(6): 823-830.

[8] Wood R G, Rutenbar R A. FPGA routing and routability estimationvia Boolean satisfiability. In Proc. the 5th Int. Symp.Field-Programmable Gate Arrays, Feb. 1997, pp.119-125.

[9] Song X, Hung W N N, Mishchenko A, Chrzanowska-Jeske M,Kennings A, Coppola A. Board-level multiterminal net assignmentfor the partial cross-bar architecture. IEEE Trans.VLSI Systems, 2003, 11(3): 511-514.

[10] Hung W N N, Song X, Kam T, Cheng L, Yang G. Routabilitychecking for three-dimensional architectures. IEEE Trans.VLSI Systems, 2004, 12(12): 1371-1374.

[11] Hung W N N, Song X, Aboulhamid E M et al. Segmentedchannel routability via satisfiability. Trans. Design Automa-tion of Electronic Systems, 2004, 9(4): 517-528.

[12] He F, Hung W N N, Song X, Gu M, Sun J. A satisfiabilityformulation for FPGA routing with pin rearrangements. In-ternational Journal of Electronics, 2007, 94(9): 857-868.

[13] Wang J, Chen M, Wan X, Wei J. Ant-colony-optimizationbasedscheduling algorithm for uplink CDMA nonreal-timedata. IEEE Trans. Vehicular Tech., 2009, 58(1): 231-241.

[14] Wang J, Chen M,Wang J. Adaptive channel and power allocationof downlink multi-user MC-CDMA systems. Computersand Electrical Engineering, 2009, 35(5): 622-633.

[15] Wang J, Chen H, Chen M et al. Cross-layer packet schedulingfor downlink multiuser OFDM systems. Science in ChinaSeries F: Inform. Sci., 2009, 52(12): 2369-2377.

[16] Davis M, Putnam H. A computing procedure for quantificationtheory. J. ACM, 1960, 7(3): 201-215.

[17] Davis M, Logemann G, Loveland D. A machine program fortheorem proving. Comms. ACM, 1962, 5(7): 394-397.

[18] Gu J. Local search for satisfiability (SAT) problem. Trans.Systems, Man, and Cybernetics, 1993, 23(4): 1108-1129.

[19] Selman B, Kautz H A, Cohen B. Noise strategies for improvinglocal search. In Proc. the 12th National Conference onArtificial Intelligence, July 31-August 4, 1994, pp.337-343.

[20] Zhao C, Zhou H, Zheng Z, Xu K. A message-passing approachto random constraint satisfaction problems with growing domains.Journal of Statistical Mechanics: Theory and Experi-ment, 2011, P02019.

[21] Zhao C, Zhang P, Zheng Z, Xu K. Analytical and beliefpropagation studies of random constraint satisfaction problemswith growing domains. Physical Review E, 2012,85(1/2): 016106.

[22] Selman B, Levesque H, Mitchell D. A new method for solvinghard satisfiability problems. In Proc. the 10th NationalConference on Artificial Intelligence, July 1992, pp.440-446.

[23] Zhang L, Madigan C, Moskewicz M et al. Efficient conflictdriven learning in a Boolean satisfiability solver. In Proc. Int.Conf. Computer-Aided Design, Nov. 2001, pp.279-285.

[24] Goldberg E, Novikov Y. BerkMin: A fast and robust SATsolver.In Proc. Design Automation and Test in Europe,March 2002, pp.142-149.

[25] Eén N, Sörensson N. Translating pseudo-Boolean constraintsinto SAT. Journal on Satisfiability, Boolean Modeling andComputation, 2006, 2(1/4): 1-26.

[26] Pipatsrisawat K, Darwiche A. RSat 1.03: SAT solver description.Technical Report D-152, Automated Reasoning Group,Computer Science Department, UCLA, 2006.

[27] Xu K, Li W. Exact phase transitions in random constraintsatisfaction problems. Journal of Artificial Intelligence Re-search, 2000, 12: 93-103.

[28] Franco J, Paull M. Probabilistic analysis of the Davis Putnamprocedure for solving the satisfiability problem. Discrete Ap-plied Mathematics, 1983, 5(1): 77-87.

[29] Xu L, Hutter F, Hoos H H et al. SATzilla: Portfolio-basedalgorithm selection for SAT. Journal of Artificial IntelligenceResearch, 2008, 32(1): 565-606.

[30] Xu K, Li W. Many hard examples in exact phase transitions.Theoretical Computer Science, 2006, 355(3): 291-302.

[31] Xu K, Boussemart F, Hemery F, Lecoutre C. Random constraintsatisfaction: Easy generation of hard (satisfiable) instances.Artificial Intelligence, 2007, 171(8/9): 514-534.

[32] Jiang W, Liu T, Ren T, Xu K. Two hardness results on feedbackvertex sets. In Lecture Notes in Computer Science 6681,Atallah M, Li X, Zhu B (eds.), Springer, 2011, pp.233-243.

[33] Liu T, Lin X, Wang C, Su K, Xu K. Large hinge width onsparse random hypergraphs. In Proc. the 22nd Int. JointConf. Artificial Intelligence, July 2011, pp.611-616.

[34] Wang C, Liu T, Cui P, Xu K. A note on treewidth in randomgraphs. In Lecture Notes in Computer Science 6831, WangW, Zhu X, Du D (eds.), Springer-Verlag, 2011, pp.491-499.

[35] Zhang L. SAT-solving: From Davis-Putnam to Zchaff and beyond,2003. http://research.microsoft.com/enus/people/lintaoz/sat-course1.pdf.

[36] Nieuwenhuis R, Oliveras A, Tinelli C. Solving SAT and SATmodulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM, 2006,53(6): 937-977.

[37] Pullan W, Hoos H H. Dynamic local search for the maximumclique problem. Journal of Artificial Intelligence Research,2006, 25: 159-185.

[38] Cai S, Su K, Sattar A. Local search with edge weighting andconfiguration checking heuristics for minimum vertex cover.Artificial Intelligence, 2011, 175: 1672-1696.

[39] Cai S, Su K, Chen Q. EWLS: A new local search for minimumvertex cover. In Proc. the 24th AAAI Conference onArtificial Intelligence, July 2010, pp.45-50.

[40] Richter C G S, Helmert M. A stochastic local search approachto vertex cover. In Proc. the 30th Annual German Confer-ence on Artificial Intelligence, Sept. 2007, pp.412-426.
No related articles found!
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
[1] 姚荣; 康泰; 陈廷槐;. Algorithms for the Determination of Cutsets in a Hypergraph[J]. , 1990, 5(1): 41 -46 .
[2] 郭恒昌;. On the Characterization and Fault Identification of Sequentially t-Diagnosable System Under PMC Model[J]. , 1991, 6(1): 83 -90 .
[3] 徐殿祥; 郑国梁;. Towards a Declarative Semantics of Inheritance with Exceptions[J]. , 1996, 11(1): 61 -71 .
[4] 迟学斌;. Parallel Implementation of Linear Algebra Problems on Dawning-1000[J]. , 1998, 13(2): 141 -146 .
[5] 管伟光; 解林; 马颂德;. Deformable Registration of Digital Images[J]. , 1998, 13(3): 246 -260 .
[6] 傅育熙;. Reaction Graph[J]. , 1998, 13(6): 510 -530 .
[7] 倪彬; 冯玉琳;. Dynamic Checking Frameworkfor Java Beaus Semantic Constraints[J]. , 1999, 14(4): 408 -413 .
[8] . CAD 装配系统中多分辨率建模方法及应用[J]. , 2006, 21(2): 272 -278 .
[9] . 改进修改后代码中的故障检测——来自电信业的研究[J]. , 2007, 22(3): 397 -409 .
[10] . AHT Bézier曲线 及 NUAHT B样条曲线[J]. , 2007, 22(4): 597 -607 .
版权所有 © 《计算机科学技术学报》编辑部
本系统由北京玛格泰克科技发展有限公司设计开发 技术支持：support@magtech.com.cn
总访问量：