Document Open Access Logo

Improving Local Search for Structured SAT Formulas via Unit Propagation Based Construct and Cut Initialization (Short Paper)

Authors Shaowei Cai , Chuan Luo , Xindi Zhang , Jian Zhang

PDF
Thumbnail PDF

File

LIPIcs.CP.2021.5.pdf
  • Filesize: 0.68 MB
  • 10 pages

Document Identifiers

Author Details

Shaowei Cai
  • State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China
  • School of Computer Science and Technology, University of Chinese Academy of Sciences, Beijing, China
Chuan Luo
  • School of Software, Beihang University, Beijing, China
Xindi Zhang
  • State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China
  • School of Computer Science and Technology, University of Chinese Academy of Sciences, Beijing, China
Jian Zhang
  • State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China
  • School of Computer Science and Technology, University of Chinese Academy of Sciences, Beijing, China

Funding

This work was supported by Beijing Academy of Artificial Intelligence (BAAI), and Youth Innovation Promotion Association, Chinese Academy of Sciences (No. 2017150), as well as the Key Research Program of Frontier Sciences, Chinese Academy of Sciences (Grant No. QYZDJ-SSW-JSC036).

Cite AsGet BibTex

Shaowei Cai, Chuan Luo, Xindi Zhang, and Jian Zhang. Improving Local Search for Structured SAT Formulas via Unit Propagation Based Construct and Cut Initialization (Short Paper). In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 5:1-5:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CP.2021.5

Abstract

This work is dedicated to improving local search solvers for the Boolean satisfiability (SAT) problem on structured instances. We propose a construct-and-cut (CnC) algorithm based on unit propagation, which is used to produce initial assignments for local search. We integrate our CnC initialization procedure within several state-of-the-art local search SAT solvers, and obtain the improved solvers. Experiments are carried out with a benchmark encoded from a spectrum repacking project as well as benchmarks encoded from two important mathematical problems namely Boolean Pythagorean Triple and Schur Number Five. The experiments show that the CnC initialization improves the local search solvers, leading to better performance than state-of-the-art SAT solvers based on Conflict Driven Clause Learning (CDCL) solvers.

Subject Classification

ACM Subject Classification
  • Theory of computation → Randomized local search
Keywords
  • Satisfiability
  • Local Search
  • Unit Propagation
  • Mathematical Problems

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Gilles Audemard, Jean-Marie Lagniez, Bertrand Mazure, and Lakhdar Sais. Boosting local search thanks to CDCL. In Proceedings of LPAR 2010, pages 474-488, 2010. Google Scholar
  2. Adrian Balint and Andreas Fröhlich. Improving stochastic local search for SAT with a new probability distribution. In Proceedings of SAT 2010, pages 10-15, 2010. Google Scholar
  3. Adrian Balint, Michael Henn, and Oliver Gableske. A novel approach to combine a SLS- and a DPLL-solver for the satisfiability problem. In Proceedings of SAT 2009, pages 284-297, 2009. Google Scholar
  4. Adrian Balint and Uwe Schöning. Choosing probability distributions for stochastic local search and the role of make versus break. In Proceedings of SAT 2012, pages 16-29, 2012. Google Scholar
  5. Armin Biere. Splatz, Lingeling, Plingeling, Treengeling, YalSAT entering the SAT competition 2016. In Proceedings of SAT Competition 2016: Solver and Benchmark Descriptions, pages 44-45, 2016. Google Scholar
  6. Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximilian Heisinger. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT competition 2020. In Proceedings of SAT Competition 2020: Solver and Benchmark Descriptions, pages 50-53, 2020. Google Scholar
  7. Shaowei Cai, Chuan Luo, Jinkun Lin, and Kaile Su. New local search methods for partial MaxSAT. Artificial Intelligence, 240:1-18, 2016. Google Scholar
  8. Shaowei Cai, Chuan Luo, and Kaile Su. CCAnr: A configuration checking based local search solver for non-random satisfiability. In Proceedings of SAT 2015, pages 1-8, 2015. Google Scholar
  9. Shaowei Cai, Chuan Luo, and Haochen Zhang. From decimation to local search and back: A new approach to MaxSAT. In Proceedings of IJCAI 2017, pages 571-577, 2017. Google Scholar
  10. Edmund M. Clarke, Armin Biere, Richard Raimi, and Yunshan Zhu. Bounded model checking using satisfiability solving. Formal Methods in System Design, 19(1):7-34, 2001. Google Scholar
  11. Byron Cook, Daniel Kroening, and Natasha Sharygina. Cogent: Accurate theorem proving for program verification. In Proceedings of CAV 2005, pages 296-300, 2005. Google Scholar
  12. Adnan Darwiche and Knot Pipatsrisawat. Complete algorithms. In Handbook of Satisfiability, pages 99-130. IOS Press, 2009. Google Scholar
  13. Martin Davis, George Logemann, and Donald W. Loveland. A machine program for theorem-proving. Communications of the ACM, 5(7):394-397, 1962. Google Scholar
  14. Andreas Fröhlich, Armin Biere, Christoph M. Wintersteiger, and Youssef Hamadi. Stochastic local search for satisfiability modulo theories. In Proceedings of AAAI 2015, pages 1136-1143, 2015. Google Scholar
  15. Oliver Gableske and Marijn Heule. EagleUP: Solving random 3-SAT using SLS with unit propagation. In Proceedings of SAT 2011, pages 367-368, 2011. Google Scholar
  16. Marijn J. H. Heule. Schur number five. In Proceedings AAAI 2018, pages 6598-6606, 2018. Google Scholar
  17. Marijn J. H. Heule, Oliver Kullmann, and Victor W. Marek. Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer. In Proceedings of SAT 2016, pages 228-245, 2016. Google Scholar
  18. Edward A. Hirsch and Arist Kojevnikov. UnitWalk: A new SAT solver that uses local search guided by unit clause elimination. Annals of Mathematics and Artificial Intelligence, 43(1):91-111, 2005. Google Scholar
  19. Holger H. Hoos and Thomas Stützle. Stochastic Local Search: Foundations & Applications. Elsevier / Morgan Kaufmann, 2004. Google Scholar
  20. Chu Min Li and Yu Li. Satisfying versus falsifying in local search for satisfiability. In Proceedings of SAT 2012, pages 477-478, 2012. Google Scholar
  21. Chu Min Li and Yu Li. Description of Sattime 2013. In Proceedings of SAT Competition 2013 : Solver and Benchmark Descriptions, pages 77-78, 2013. Google Scholar
  22. Xiao Yu Li, Matthias F. M. Stallmann, and Franc Brglez. A local search SAT solver using an effective switching strategy and an efficient unit propagation. In Proceedings of SAT 2003, pages 53-68, 2003. Google Scholar
  23. Jia Hui Liang, Vijay Ganesh, Pascal Poupart, and Krzysztof Czarnecki. Learning rate based branching heuristic for SAT solvers. In Proceedings of SAT 2016, pages 123-140, 2016. Google Scholar
  24. Michael Luby, Alistair Sinclair, and David Zuckerman. Optimal speedup of las vegas algorithms. Information Processing Letters, 47(4):173-180, 1993. Google Scholar
  25. Chuan Luo, Shaowei Cai, Kaile Su, and Wenxuan Huang. CCEHC: An efficient local search algorithm for weighted partial maximum satisfiability. Artificial Intelligence, 243:26-44, 2017. Google Scholar
  26. Chuan Luo, Shaowei Cai, Kaile Su, and Wei Wu. Clause states based configuration checking in local search for satisfiability. IEEE Transactions on Cybernetics, 45(5):1014-1027, 2015. Google Scholar
  27. Chuan Luo, Shaowei Cai, Wei Wu, Zhong Jie, and Kaile Su. CCLS: An efficient local search algorithm for weighted maximum satisfiability. IEEE Transactions on Computers, 64(7):1830-1843, 2015. Google Scholar
  28. Chuan Luo, Shaowei Cai, Wei Wu, and Kaile Su. Double configuration checking in stochastic local search for satisfiability. In Proceedings of AAAI 2014, pages 2703-2709, 2014. Google Scholar
  29. Chuan Luo, Holger H. Hoos, and Shaowei Cai. PbO-CCSAT: Boosting local search for satisfiability using programming by optimisation. In Proceedings of PPSN 2020, pages 373-389, 2020. Google Scholar
  30. Mao Luo, Chu-Min Li, Fan Xiao, Felip Manyà, and Zhipeng Lü. An effective learnt clause minimization approach for CDCL SAT solvers. In Proceedings of IJCAI 2017, pages 703-711, 2017. Google Scholar
  31. Norbert Manthey. Coprocessor 2.0 - A flexible CNF simplifier - (tool presentation). In Proceedings of SAT 2012, pages 436-441, 2012. Google Scholar
  32. Neil Newman, Alexandre Fréchette, and Kevin Leyton-Brown. Deep optimization for spectrum repacking. Communications of the ACM, 61(1):97-104, 2018. Google Scholar
  33. João P. Marques Silva and Karem A. Sakallah. GRASP - A new search algorithm for satisfiability. In Proceedings of ICCAD 1996, pages 220-227, 1996. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact