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

• Theoretical Computer Science • Previous Articles     Next Articles

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.

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!
Full text



[1] Yao Rong; Kang Tai; Chen Tinghuai;. Algorithms for the Determination of Cutsets in a Hypergraph[J]. , 1990, 5(1): 41 -46 .
[2] Guo Hengchang;. On the Characterization and Fault Identification of Sequentially t-Diagnosable System Under PMC Model[J]. , 1991, 6(1): 83 -90 .
[3] Xu Dianxiang; Zheng Guoliang;. Towards a Declarative Semantics of Inheritance with Exceptions[J]. , 1996, 11(1): 61 -71 .
[4] Chi Xuebin;. Parallel Implementation of Linear Algebra Problems on Dawning-1000[J]. , 1998, 13(2): 141 -146 .
[5] Guan Weiguang; Xie Lin; Ma Songde;. Deformable Registration of Digital Images[J]. , 1998, 13(3): 246 -260 .
[6] Fu Yuxi;. Reaction Graph[J]. , 1998, 13(6): 510 -530 .
[7] NI Bin; FENG Yulin;. Dynamic Checking Frameworkfor Java Beaus Semantic Constraints[J]. , 1999, 14(4): 408 -413 .
[8] Sungchan Kim, Kunwoo Lee, Taesik Hong, and Moonki Jung. Modeling in Multi-Resolution and Its Applications[J]. , 2006, 21(2): 272 -278 .
[9] Piotr Tomaszewski, Lars Lundberg, and Haa kan Grahn. Improving Fault Detection in Modified Code --- A Study from the Telecommunication Industry[J]. , 2007, 22(3): 397 -409 .
[10] Gang Xu and Guo-Zhao Wang. AHT Bézier Curves and NUAHT B-Spline Curves[J]. , 2007, 22(4): 597 -607 .

ISSN 1000-9000(Print)

CN 11-2296/TP

Editorial Board
Author Guidelines
Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
E-mail: jcst@ict.ac.cn
  Copyright ©2015 JCST, All Rights Reserved