Complete Boolean Satisfiability Solving Algorithms Based on Local Search | Journal of Computer Science and Technology Skip to main content
Springer Nature Link
Log in

Complete Boolean Satisfiability Solving Algorithms Based on Local Search

  • Regular Paper
  • Published:
Journal of Computer Science and Technology Aims and scope Submit manuscript

Abstract

Boolean satisfiability (SAT) is a well-known problem in computer science, artificial intelligence, and operations research. This paper focuses on the satisfiability problem of Model 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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

  1. Cook S A. The complexity of theorem-proving procedures. In Proc. 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.

    Google Scholar 

  3. Biere A, Cimatti A, Clarke E M, Fujita M, Zhu Y. Symbolic model checking using SAT procedures instead of BDDs. In Proc. the 36th Conf. Design Automation, June 1999, pp.317-320.

  4. Bjesse P, Leonard T, Mokkedem A. Finding bugs in an Alpha microprocessor using satisfiability solvers. In Lecture Notes in Computer 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 RTL verification: An integrated approach. In Proc. the 9th HLDVT, November 2004, pp.9-13.

  6. Hung W N N, Song X, Yang G, Yang J, Perkowski M. Optimal synthesis of multiple output Boolean functions using a set of quantum gates by symbolic reachability analysis. IEEE Trans. CAD, 2006, 25(9): 1652–1663.

    Google Scholar 

  7. Hung W N N, Gao C, Song X, Hammerstrom D. Defect tolerant CMOL cell assignment via satisfiability. IEEE Sensors Journal, 2008, 8(6): 823–830.

    Article  Google Scholar 

  8. Wood R G, Rutenbar R A. FPGA routing and routability estimation via 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 assignment for the partial cross-bar architecture. IEEE Trans. VLSI Systems, 2003, 11(3): 511–514.

    Article  Google Scholar 

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

    Article  Google Scholar 

  11. Hung W N N, Song X, Aboulhamid E M et al. Segmented channel routability via satisfiability. Trans. Design Automation of Electronic Systems, 2004, 9(4): 517–528.

    Article  Google Scholar 

  12. He F, Hung W N N, Song X, Gu M, Sun J. A satisfiability formulation for FPGA routing with pin rearrangements. International Journal of Electronics, 2007, 94(9): 857–868.

    Article  Google Scholar 

  13. Wang J, Chen M, Wan X, Wei J. Ant-colony-optimizationbased scheduling algorithm for uplink CDMA nonreal-time data. IEEE Trans. Vehicular Tech., 2009, 58(1): 231–241.

    Article  Google Scholar 

  14. Wang J, Chen M,Wang J. Adaptive channel and power allocation of downlink multi-user MC-CDMA systems. Computers and Electrical Engineering, 2009, 35(5): 622–633.

    Article  MATH  Google Scholar 

  15. Wang J, Chen H, Chen M et al. Cross-layer packet scheduling for downlink multiuser OFDM systems. Science in China Series F: Inform. Sci., 2009, 52(12): 2369–2377.

    Article  MATH  Google Scholar 

  16. Davis M, Putnam H. A computing procedure for quantification theory. J. ACM, 1960, 7(3): 201–215.

    Article  MathSciNet  MATH  Google Scholar 

  17. Davis M, Logemann G, Loveland D. A machine program for theorem proving. Comms. ACM, 1962, 5(7): 394–397.

    Article  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

  19. Selman B, Kautz H A, Cohen B. Noise strategies for improving local search. In Proc. the 12th National Conference on Artificial Intelligence, July 31-August 4, 1994, pp.337-343.

  20. Zhao C, Zhou H, Zheng Z, Xu K. A message-passing approach to random constraint satisfaction problems with growing domains. Journal of Statistical Mechanics: Theory and Experiment, 2011, P02019.

  21. Zhao C, Zhang P, Zheng Z, Xu K. Analytical and belief-propagation studies of random constraint satisfaction problems with growing domains. Physical Review E, 2012, 85(1/2): 016106.

    Article  Google Scholar 

  22. Selman B, Levesque H, Mitchell D. A new method for solving hard satisfiability problems. In Proc. the 10th National Conference on Artificial Intelligence, July 1992, pp.440-446.

  23. Zhang L, Madigan C, Moskewicz M et al. Efficient conflict driven 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 constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation, 2006, 2(1/4): 1–26.

    MATH  Google Scholar 

  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 constraint satisfaction problems. Journal of Artificial Intelligence Research, 2000, 12: 93–103.

    MathSciNet  MATH  Google Scholar 

  28. Franco J, Paull M. Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem. Discrete Applied Mathematics, 1983, 5(1): 77–87.

    Article  MathSciNet  MATH  Google Scholar 

  29. Xu L, Hutter F, Hoos H H et al. SATzilla: Portfolio-based algorithm selection for SAT. Journal of Artificial Intelligence Research, 2008, 32(1): 565–606.

    MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  32. Jiang W, Liu T, Ren T, Xu K. Two hardness results on feedback vertex 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 on sparse random hypergraphs. In Proc. the 22nd Int. Joint Conf. Artificial Intelligence, July 2011, pp.611-616.

  34. Wang C, Liu T, Cui P, Xu K. A note on treewidth in random graphs. In Lecture Notes in Computer Science 6831, Wang W, 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 SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM, 2006, 53(6): 937–977.

    Article  MathSciNet  Google Scholar 

  37. Pullan W, Hoos H H. Dynamic local search for the maximum clique problem. Journal of Artificial Intelligence Research, 2006, 25: 159–185.

    MATH  Google Scholar 

  38. Cai S, Su K, Sattar A. Local search with edge weighting and configuration checking heuristics for minimum vertex cover. Artificial Intelligence, 2011, 175: 1672–1696.

    Article  MathSciNet  MATH  Google Scholar 

  39. Cai S, Su K, Chen Q. EWLS: A new local search for minimum vertex cover. In Proc. the 24th AAAI Conference on Artificial Intelligence, July 2010, pp.45-50.

  40. Richter C G S, Helmert M. A stochastic local search approach to vertex cover. In Proc. the 30th Annual German Conference on Artificial Intelligence, Sept. 2007, pp.412-426.

Download references

Author information

Authors and Affiliations

  1. School of Computer Science and Engineering, University of Electronic Science and Technology of China, Chengdu, 611731, China

    Wen-Sheng Guo (Member, CCF, ACM) & Guo-Wu Yang (Member, CCF, ACM)

  2. Synopsys Inc., Mountain View, California, 94043, U.S.A.

    William N. N. Hung (Senior Member, IEEE)

  3. Department of Electrical and Computer Engineering, Portland State University, Portland, 97207, U.S.A.

    Xiaoyu Song (Senior Member, IEEE)

Authors
  1. Wen-Sheng Guo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Guo-Wu Yang
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. William N. N. Hung
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Xiaoyu Song
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Wen-Sheng Guo.

Additional information

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.

Electronic Supplementary Material

Below is the link to the electronic supplementary material.

(DOC 27.0 KB)

Rights and permissions

Reprints and permissions

About this article

Cite this article

Guo, WS., Yang, GW., Hung, W.N.N. et al. Complete Boolean Satisfiability Solving Algorithms Based on Local Search. J. Comput. Sci. Technol. 28, 247–254 (2013). https://doi.org/10.1007/s11390-013-1326-4

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11390-013-1326-4

Keywords

Search

Navigation