Combining VSIDS and CHB Using Restarts in SAT

Authors Mohamed Sami Cherif , Djamal Habet, Cyril Terrioux



PDF
Thumbnail PDF

File

LIPIcs.CP.2021.20.pdf
  • Filesize: 1.12 MB
  • 19 pages

Document Identifiers

Author Details

Mohamed Sami Cherif
  • Aix-Marseille Univ, Université de Toulon, CNRS, LIS, Marseille, France
Djamal Habet
  • Aix-Marseille Univ, Université de Toulon, CNRS, LIS, Marseille, France
Cyril Terrioux
  • Aix-Marseille Univ, Université de Toulon, CNRS, LIS, Marseille, France

Cite AsGet BibTex

Mohamed Sami Cherif, Djamal Habet, and Cyril Terrioux. Combining VSIDS and CHB Using Restarts in SAT. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CP.2021.20

Abstract

Conflict Driven Clause Learning (CDCL) solvers are known to be efficient on structured instances and manage to solve ones with a large number of variables and clauses. An important component in such solvers is the branching heuristic which picks the next variable to branch on. In this paper, we evaluate different strategies which combine two state-of-the-art heuristics, namely the Variable State Independent Decaying Sum (VSIDS) and the Conflict History-Based (CHB) branching heuristic. These strategies take advantage of the restart mechanism, which helps to deal with the heavy-tailed phenomena in SAT, to switch between these heuristics thus ensuring a better and more diverse exploration of the search space. Our experimental evaluation shows that combining VSIDS and CHB using restarts achieves competitive results and even significantly outperforms both heuristics for some chosen strategies.

Subject Classification

ACM Subject Classification
  • Computing methodologies → Artificial intelligence
Keywords
  • Satisfiability
  • Branching Heuristic
  • Restarts

Metrics

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

References

  1. Rajeev Agrawal. Sample mean based index policies by O(log n) regret for the multi-armed bandit problem. Advances in Applied Probability, 27(4):1054-1078, 1995. URL: https://doi.org/10.2307/1427934.
  2. Gilles Audemard and Laurent Simon. Predicting Learnt Clauses Quality in Modern SAT Solvers. In Craig Boutilier, editor, Proceedings of the 21st International Joint Conference on Artifical Intelligence, IJCAI'09, page 399–404, San Francisco, CA, USA, 2009. Morgan Kaufmann Publishers Inc. URL: https://www.ijcai.org/Proceedings/09/Papers/074.pdf.
  3. Gilles Audemard and Laurent Simon. Refining Restarts Strategies for SAT and UNSAT. In Michela Milano, editor, Principles and Practice of Constraint Programming - 18th International Conference, CP 2012, Québec City, QC, Canada, October 8-12, 2012. Proceedings, volume 7514 of Lecture Notes in Computer Science, pages 118-126. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-33558-7_11.
  4. Jean-Yves Audibert and Sébastien Bubeck. Minimax Policies for Adversarial and Stochastic Bandits. In COLT 2009 - The 22nd Conference on Learning Theory, Montreal, Quebec, Canada, June 18-21, 2009, 2009. URL: http://www.cs.mcgill.ca/%7Ecolt2009/papers/022.pdf.
  5. Peter Auer, Nicolò Cesa-Bianchi, and Paul Fischer. Finite-time Analysis of the Multiarmed Bandit Problem. Mach. Learn., 47(2-3):235-256, 2002. URL: https://doi.org/10.1023/A:1013689704352.
  6. Peter Auer, Nicolo Cesa-Bianchi, Yoav Freund, and Robert E Schapire. The nonstochastic multiarmed bandit problem. SIAM journal on computing, 32(1):48-77, 2002. URL: https://doi.org/10.1137/S0097539701398375.
  7. Tomáš Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors. Proceedings of SAT Competition 2020: Solver and Benchmark Descriptions, volume B-2020-1 of Department of Computer Science Series of Publications B. Department of Computer Science, University of Helsinki, 2020. URL: https://helda.helsinki.fi/bitstream/handle/10138/318450/sc2020_proceedings.pdf.
  8. Armin Biere. Adaptive Restart Strategies for Conflict Driven SAT Solvers. In Hans Kleine Büning and Xishun Zhao, editors, Theory and Applications of Satisfiability Testing - SAT 2008, 11th International Conference, SAT 2008, Guangzhou, China, May 12-15, 2008. Proceedings, volume 4996 of Lecture Notes in Computer Science, pages 28-33. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-79719-7_4.
  9. Armin Biere. CaDiCaL, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT Competition 2017. In Tomáš Balyo, Marijn Heule, and Matti Järvisalo, editors, Proc. of SAT Competition 2017 - Solver and Benchmark Descriptions, volume B-2017-1 of Department of Computer Science Series of Publications B, pages 14-15. University of Helsinki, 2017. Google Scholar
  10. Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximillian Heisinger. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors, Proc. of SAT Competition 2020 - Solver and Benchmark Descriptions, volume B-2020-1 of Department of Computer Science Report Series B, pages 51-53. University of Helsinki, 2020. Google Scholar
  11. Armin Biere, Mathias Fleury, and Maximillian Heisinger. CADICAL, KISSAT, PARACOOBA Entering the SAT Competition 2021. In Proceedings of SAT Competition 2021: Solver and Benchmark Descriptions, volume B-2021-1 of Department of Computer Science Series of Publications B, pages 10-13. University of Helsinki, 2021 . Google Scholar
  12. Armin Biere and Andreas Fröhlich. Evaluating CDCL Variable Scoring Schemes. In Marijn Heule and Sean A. Weaver, editors, Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings, volume 9340 of Lecture Notes in Computer Science, pages 405-422. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-24318-4_29.
  13. Mohamed Sami Cherif, Djamal Habet, and Cyril Terrioux. On the Refinement of Conflict History Search Through Multi-Armed Bandit. In 32nd IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2020, Baltimore, MD, USA, November 9-11, 2020, pages 264-271. IEEE, 2020. URL: https://doi.org/10.1109/ICTAI50040.2020.00050.
  14. Mohamed Sami Cherif, Djamal Habet, and Cyril Terrioux. Kissat_MAB: Combining VSIDS and CHB through Multi-Armed Bandit. In Proceedings of SAT Competition 2021: Solver and Benchmark Descriptions, volume B-2021-1 of Department of Computer Science Series of Publications B, pages 15-16. University of Helsinki, 2021. Google Scholar
  15. Wei Chu, Lihong Li, Lev Reyzin, and Robert E. Schapire. Contextual Bandits with Linear Payoff Functions. In Geoffrey J. Gordon, David B. Dunson, and Miroslav Dudík, editors, Proceedings of the Fourteenth International Conference on Artificial Intelligence and Statistics, AISTATS 2011, Fort Lauderdale, USA, April 11-13, 2011, volume 15 of JMLR Proceedings, pages 208-214. JMLR.org, 2011. URL: http://proceedings.mlr.press/v15/chu11a/chu11a.pdf.
  16. Stephen A. Cook. The Complexity of Theorem-Proving Procedures. In Proceedings of the Third Annual ACM Symposium on Theory of Computing, STOC '71, page 151–158, New York, NY, USA, 1971. Association for Computing Machinery. URL: https://doi.org/10.1145/800157.805047.
  17. Todd Deshane, Wenjin Hu, Patty Jablonski, Hai Lin, Christopher Lynch, and Ralph Eric McGregor. Encoding First Order Proofs in SAT. In Frank Pfenning, editor, Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings, volume 4603 of Lecture Notes in Computer Science, pages 476-491. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73595-3_35.
  18. Niklas Eén and Niklas Sörensson. An Extensible SAT-solver. In Enrico Giunchiglia and Armando Tacchella, editors, Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers, volume 2919 of Lecture Notes in Computer Science, pages 502-518. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-24605-3_37.
  19. Carla P Gomes, Bart Selman, Nuno Crato, and Henry Kautz. Heavy-tailed phenomena in satisfiability and constraint satisfaction problems. Journal of automated reasoning, 24(1-2):67-100, 2000. URL: https://doi.org/10.1023/A:1006314320276.
  20. Shai Haim and Marijn Heule. Towards Ultra Rapid Restarts. CoRR, abs/1402.4413, 2014. URL: http://arxiv.org/abs/1402.4413.
  21. William D. Harvey and Matthew L. Ginsberg. Limited Discrepancy Search. In Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence, IJCAI 95, Montréal Québec, Canada, August 20-25 1995, 2 Volumes, pages 607-615. Morgan Kaufmann, 1995. URL: http://ijcai.org/Proceedings/95-1/Papers/080.pdf.
  22. Marijn Heule, Matti Järvisalo, and Martin Suda, editors. Proceedings of SAT Race 2019: Solver and Benchmark Descriptions, volume B-2019-1 of Department of Computer Science Series of Publications B. Department of Computer Science, University of Helsinki, 2019. URL: https://helda.helsinki.fi/bitstream/handle/10138/306988/sr2019_proceedings.pdf.
  23. Marijn Heule, Matti Juhani Järvisalo, Martin Suda, et al., editors. Proceedings of SAT Competition 2018: Solver and Benchmark Descriptions, volume B-2018-1 of Department of Computer Science Series of Publications B. Department of Computer Science, University of Helsinki, 2018. URL: https://helda.helsinki.fi/bitstream/handle/10138/237063/sc2018_proceedings.pdf.
  24. Ted Hong, Yanjing Li, Sung-Boem Park, Diana Mui, David Lin, Ziyad Abdel Kaleq, Nagib Hakim, Helia Naeimi, Donald S. Gardner, and Subhasish Mitra. QED: Quick Error Detection tests for effective post-silicon validation. In Ron Press and Erik H. Volkerink, editors, 2011 IEEE International Test Conference, ITC 2010, Austin, TX, USA, November 2-4, 2010, pages 154-163. IEEE Computer Society, 2010. URL: https://doi.org/10.1109/TEST.2010.5699215.
  25. Vitaly Kurin, Saad Godil, Shimon Whiteson, and Bryan Catanzaro. Improving SAT Solver Heuristics with Graph Networks and Reinforcement Learning. CoRR, abs/1909.11830, 2019. URL: http://arxiv.org/abs/1909.11830.
  26. Tze Leung Lai and Herbert Robbins. Asymptotically efficient adaptive allocation rules. Advances in applied mathematics, 6(1):4-22, 1985. URL: https://doi.org/10.1016/0196-8858(85)90002-8.
  27. Nadjib Lazaar, Youssef Hamadi, Said Jabbour, and Michèle Sebag. Cooperation control in Parallel SAT Solving: a Multi-armed Bandit Approach. Research Report RR-8070, INRIA, 2012. Google Scholar
  28. Jia Hui Liang, Chanseok, Vijay Ganesh, Krzysztof Czarnecki, and Pascal Poupart. MapleCOMSPS, MapleCOMSPS_LRB, MapleCOMSPS_CHB. In Proceedings of SAT Competition 2017: Solver and Benchmark Descriptions, page 20–21, 2017. Google Scholar
  29. Jia Hui Liang, Vijay Ganesh, Pascal Poupart, and Krzysztof Czarnecki. Exponential Recency Weighted Average Branching Heuristic for SAT Solvers. In Dale Schuurmans and Michael P. Wellman, editors, Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, February 12-17, 2016, Phoenix, Arizona, USA, pages 3434-3440. AAAI Press, 2016. URL: http://www.aaai.org/ocs/index.php/AAAI/AAAI16/paper/view/12451.
  30. Jia Hui Liang, Vijay Ganesh, Pascal Poupart, and Krzysztof Czarnecki. Learning Rate Based Branching Heuristic for SAT Solvers. In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, volume 9710 of Lecture Notes in Computer Science, pages 123-140. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_9.
  31. Jia Hui Liang, Chanseok Oh, Vijay Ganesh, Krzysztof Czarnecki, and Pascal Poupart. MapleCOMSPS, MapleCOMSPS_LRB, MapleCOMSPS_CHB. In Proceedings of SAT Competition 2016: Solver and Benchmark Descriptions, page 52–53, 2016. Google Scholar
  32. Michael Luby, Alistair Sinclair, and David Zuckerman. Optimal speedup of Las Vegas algorithms. Information Processing Letters, pages 128-133, 1993. URL: https://doi.org/10.1109/ISTCS.1993.253477.
  33. Inês Lynce and João Marques-Silva. SAT in Bioinformatics: Making the Case with Haplotype Inference. In Armin Biere and Carla P. Gomes, editors, Theory and Applications of Satisfiability Testing - SAT 2006, 9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings, volume 4121 of Lecture Notes in Computer Science, pages 136-141. Springer, 2006. URL: https://doi.org/10.1007/11814948_16.
  34. J.P. Marques-Silva and K.A. Sakallah. GRASP: a search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48(5):506-521, 1999. URL: https://doi.org/10.1109/12.769433.
  35. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an Efficient SAT Solver. In Proceedings of the 38th Design Automation Conference, DAC 2001, Las Vegas, NV, USA, June 18-22, 2001, pages 530-535. ACM, 2001. URL: https://doi.org/10.1145/378239.379017.
  36. Anastasia Paparrizou and Hugues Wattez. Perturbing Branching Heuristics in Constraint Solving. In Helmut Simonis, editor, Principles and Practice of Constraint Programming - 26th International Conference, CP 2020, Louvain-la-Neuve, Belgium, September 7-11, 2020, Proceedings, volume 12333 of Lecture Notes in Computer Science, pages 496-513. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-58475-7_29.
  37. Lawrence Ryan. Efficient algorithms for clause-learning SAT solvers. Master’s thesis, Simon Fraser University, 2004. Google Scholar
  38. Richard S. Sutton and Andrew G. Barto. Reinforcement learning - an introduction. Adaptive computation and machine learning. MIT Press, Cambridge, MA, USA, 1998. URL: https://www.worldcat.org/oclc/37293240.
  39. William R. Thompson. On the likelihood that one unknown probability exceeds another in view of the evidence of two samples. Biometrika, 25(3-4):285-294, December 1933. URL: https://doi.org/10.1093/biomet/25.3-4.285.
  40. Toby Walsh. Search in a Small World. In Proceedings of the 16th International Joint Conference on Artificial Intelligence - Volume 2, IJCAI'99, page 1172–1177, San Francisco, CA, USA, 1999. Morgan Kaufmann Publishers Inc. URL: https://www.ijcai.org/Proceedings/99-2/Papers/071.pdf.
  41. Hugues Wattez, Frédéric Koriche, Christophe Lecoutre, Anastasia Paparrizou, and Sébastien Tabary. Learning Variable Ordering Heuristics with Multi-Armed Bandits and Restarts. In Giuseppe De Giacomo, Alejandro Catalá, Bistra Dilkina, Michela Milano, Senén Barro, Alberto Bugarín, and Jérôme Lang, editors, ECAI 2020 - 24th European Conference on Artificial Intelligence, 29 August-8 September 2020, Santiago de Compostela, Spain, volume 325 of Frontiers in Artificial Intelligence and Applications, pages 371-378. IOS Press, 2020. URL: https://doi.org/10.3233/FAIA200115.
  42. Wei Xia and Roland H. C. Yap. Learning Robust Search Strategies Using a Bandit-Based Approach. In Sheila A. McIlraith and Kilian Q. Weinberger, editors, Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), the 30th innovative Applications of Artificial Intelligence (IAAI-18), and the 8th AAAI Symposium on Educational Advances in Artificial Intelligence (EAAI-18), New Orleans, Louisiana, USA, February 2-7, 2018, pages 6657-6665. AAAI Press, 2018. URL: https://www.aaai.org/ocs/index.php/AAAI/AAAI18/paper/view/17192.
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