A randomized diversification strategy for solving satisfiability problem with long clauses | Science China Information Sciences Skip to main content
Springer Nature Link
Log in

A randomized diversification strategy for solving satisfiability problem with long clauses

  • Research Paper
  • Published:
Science China Information Sciences Aims and scope Submit manuscript

Abstract

Satisfiability problem (SAT) is a central problem in artificial intelligence due to its computational complexity and usefulness in industrial applications. Stochastic local search (SLS) algorithms are powerful to solve hard instances of satisfiability problems, among which CScoreSAT is proposed for solving SAT instances with long clauses by using greedy mode and diversification mode. In this paper, we present a randomized variable selection strategy to improve efficiency of the diversification mode, and thus propose a new SLS algorithm. We perform a number of experiments to evaluate the new algorithm comparing with the recently proposed algorithms, and show that our algorithm is comparative with others for solving random instances near the phase transition threshold.

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

References

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

    Article  MathSciNet  MATH  Google Scholar 

  2. Davis M, Logemann G, Loveland D. A machine program for theorem proving. Commun ACM, 1962, 5: 394–397

    Article  MathSciNet  MATH  Google Scholar 

  3. Marques-Silva J P, Sakallah K A. GRASP: a search algorithm for propositional satisfiability. IEEE Trans Comput, 1999, 48: 506–521

    Article  MathSciNet  Google Scholar 

  4. Zhang L, Madigan C F, Moskewicz M H, et al. Efficient conflict driven learning in a Booleansatisfiability solver. In: Proceedings of the 2001 IEEE/ACM International Conference on Computer-Aided Design. Piscataway: IEEE Press, 2001. 279–285

    Google Scholar 

  5. Selman B, Kautz H A, Cohen B. Local search strategies for satisfiability testing. Discrete Math Theor, 1996, 26: 521–532

    MATH  Google Scholar 

  6. Selma B, Kautz H A, Cohen B. Noise strategies for improving local search. In: Proceedings of the 12th National Conference on Artificial Intelligence (AAAI-94). San Francisco: AAAI Press, 1994. 337–343

    Google Scholar 

  7. Achlioptas D, Naor A, Peres Y. Rigorous location of phase transitions in hard optimization problems. Nature, 2005, 435: 759–764

    Article  Google Scholar 

  8. Cheeseman P, Kanefsky B, Taylor W M. Where the really hard problems are. In: Proceedings of the International Joint Conference on Artificial Intelligence. San Francisco: Morgan Kaufmann Publishers, 1991. 331–340

    Google Scholar 

  9. Xu K, Li W. Exact phase transitions in random constraint satisfaction problems. J Artif Intell Res, 2000, 12: 93–103

    MathSciNet  MATH  Google Scholar 

  10. Xu K, Boussemart F, Hemery F, et al. Random constraint satisfaction: easy generation of hard (satisfiable) instances. Artif Intell, 2007, 171: 514–534

    Article  MathSciNet  MATH  Google Scholar 

  11. Mitchell D G, Selman B, Levesque H J. Hard and easy distributions of SAT problems. In: Proceedings of the 10th National Conference on Artificial Intelligence (AAAI-92). San Jose: AAAI Press, 1992. 459–465

    Google Scholar 

  12. Selman B, Levesque H, Mitchell D. A new method for solving hard satisfiability problems. In: Proceedings of the 10th National Conference on Artificial Intelligence (AAAI-92). San Jose: AAAI Press, 1992. 440–446

    Google Scholar 

  13. Hutter F, Tompkins D A D, Hoos H H. Scaling and probabilistic smoothing: efficient dynamic local search for SAT. In: Proceedings of the 8th International Conference on the Principles and Practice of Constraint Programming. Berlin: Springer, 2002. 233–248

    Google Scholar 

  14. Thornton J, Pham D N, Bain S, et al. Additive versus multiplicative clause weighting for SAT. In: Proceedings of the 19th National Conference on Artificial Intelligence (AAAI-04). San Jose: AAAI Press, 2004. 191–196

    Google Scholar 

  15. Balint A, Schöning U. Choosing probability distributions for stochastic local search and the role of make versus break. In: Proceedings of the International Conference on Theory and Applications of Satisfiability Testing. Berlin: Springer, 2012. 16–29

    Google Scholar 

  16. Li CM, Li Y. Satisfying versus falsifying in local search for satisfiability. In: Proceedings of the International Conference on Theory and Applications of Satisfiability Testing. Berlin: Springer, 2012. 477–478

    Google Scholar 

  17. Wei W, Li C M, Zhang H. A switching criterion for intensification and diversification in local search for SAT. J Satisfiab Bool Model Comput, 2008, 4: 219–237

    MATH  Google Scholar 

  18. Duong T T, Pham D N, Sattar A, et al. Weight-enhanced diversification in stochastic local search for satisfiability. In: Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, 2013

    Google Scholar 

  19. Cai S, Su K. Local search for Boolean Satisfiability with configuration checking and subscore. Artif Intell, 2013, 204: 75–98

    Article  MATH  Google Scholar 

  20. Gableske O, Heule M. EagleUP: solving random 3-SAT using SLS with unit propagation. In: Proceedings of the International Conference on Theory and Applications of Satisfiability Testing. Berlin: Springer, 2011. 367–368

    Google Scholar 

  21. Cai S, Su K. Comprehensive Score: towards efficient local search for SAT with long clauses. In: Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, 2013

    Google Scholar 

  22. Cai S, Luo C, Su K. Scoring functions based on second level score for k-SAT with long clauses. J Artif Intell Res, 2014, 51: 413–441

    MathSciNet  MATH  Google Scholar 

  23. Balint A, Biere A, Fröhlich A, et al. Improving implementation of SLS solvers for SAT and new heuristics for k-SAT with long clauses. In: Proceedings of the International Conference on Theory and Applications of Satisfiability Testing. Berlin: Springer, 2014. 302–316

    Google Scholar 

  24. Liu S, Papakonstantinou P A. Local search for hard SAT formulas: The strength of the polynomial law. In: Proceedings of the 26th AAAI Conference on Artificial Intelligence, Phoenix, 2016

    Google Scholar 

  25. Liu J, Xu K. A novel weighting scheme for random k-SAT. Sci China Inf Sci, 2016, 59: 092101

    Article  MathSciNet  Google Scholar 

  26. Cai S, Su K. Configuration checking with aspiration in local search for SAT. In: Proceedings of the 26th AAAI Conference on Artificial Intelligence. Phoenix: AAAI Press, 2016

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  28. Luo C, Cai S, Wu W, et al. Double configuration checking in stochastic local search for satisfiability. In: Proceedings of the 28th AAAI Conference on Artificial Intelligence. Quebec City: AAAI Press, 2014. 2703–2709

    Google Scholar 

  29. Wang Y Y, Ouyang D T, Zhang L M, et al. A novel local search for unicost set covering problem using hyperedge configuration checking and weight diversity. Sci China Inf Sci, 2017, 60: 062103

    Article  Google Scholar 

  30. Luo C, Cai S, Su K, et al. Clause states based configuration checking in local search for satisfiability. IEEE Trans Cybernetics, 2015, 45: 1014–1027

    Article  Google Scholar 

Download references

Acknowledgments

This work was supported by National Natural Science Foundation of China (Grant Nos. 61370156, 61402070, 61503074), Program for New Century Excellent Talents in University (Grant No. NCET-13-0724), and Natural Science Foundation of Liaoning Province (Grant No. 2015020023).

Author information

Authors and Affiliations

  1. College of Computer Science, Northeast Normal University, Changchun, 130024, China

    Jian Gao, Ruizhi Li & Minghao Yin

  2. College of Information Science and Technology, Dalian Maritime University, Dalian, 116026, China

    Jian Gao

  3. Key Laboratory of Symbolic Computation and Knowledge Engineering of Ministry of Education, Jilin University, Changchun, 130012, China

    Jian Gao

Authors
  1. Jian Gao
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ruizhi Li
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Minghao Yin
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Minghao Yin.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Gao, J., Li, R. & Yin, M. A randomized diversification strategy for solving satisfiability problem with long clauses. Sci. China Inf. Sci. 60, 092109 (2017). https://doi.org/10.1007/s11432-016-0258-4

Download citation

  • Received:

  • Accepted:

  • Published:

  • DOI: https://doi.org/10.1007/s11432-016-0258-4

Keywords

Search

Navigation