Document Open Access Logo

Parallel Clause Sharing Strategy Based on Graph Structure of SAT Problem

Authors Yoichiro Iida , Tomohiro Sonobe , Mary Inaba

PDF
Thumbnail PDF

File

LIPIcs.SAT.2024.17.pdf
  • Filesize: 1.64 MB
  • 18 pages

Document Identifiers

Author Details

Yoichiro Iida
  • Graduate School of Information Science and Technology, The University of Tokyo, Japan
Tomohiro Sonobe
  • National Institute of Informatics, Tokyo, Japan
Mary Inaba
  • Graduate School of Information Science and Technology, The University of Tokyo, Japan

Acknowledgements

We would like to express our sincere gratitude to the reviewers for their valuable comments and constructive feedback, which have greatly improved the quality of this paper. Additionally, we are grateful to the members of the Imai Laboratory for their insightful discussions and support throughout this research.

Cite AsGet BibTex

Yoichiro Iida, Tomohiro Sonobe, and Mary Inaba. Parallel Clause Sharing Strategy Based on Graph Structure of SAT Problem. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 17:1-17:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.SAT.2024.17

Abstract

Parallelization of SAT solvers is an important technique for improving solver performance. The selection of the learnt clauses to share among parallel workers is crucial for its efficiency. Literal block distance (LBD) is often used to evaluate the quality of clauses to select. We propose a new method, Parallel Clause sharing based on graph Structure (PaCS), to select good clauses for sharing. First, we conducted three preliminary experiments to assess the performance of LBD in parallel clause sharing: a performance comparison between the LBD and clause size, an analysis of the utilization of shared clauses, and a comparison of the LBD values of shared clauses at originating and receiving workers. These experiments indicate that the LBD may not be optimal for learnt clause sharing. We attribute the results to the LBD’s inherent dependency on decision trees. Each parallel worker has a unique decision tree; thus, a sharing clause that is good for its originating worker may not be good for others. Therefore, we propose PaCS, a search-independent method that uses the graph structure derived from the input CNF of SAT problems. PaCS evaluates clauses using their edges' weight in the variable incidence graph. Using the input CNF’s graph is effective for parallel clause sharing because it is the common input for all parallel workers. Furthermore, using edge weight can select clauses whose variables' Boolean values are more likely to be determined. Performance evaluation experiments demonstrate that our strategy outperforms LBD by 4% in the number of solved instances and by 12% in PAR-2. This study opens avenues for further improvements in parallel-solving strategies using the structure of SAT problems and reinterpretations of the quality of learnt clauses.

Subject Classification

ACM Subject Classification
  • Computing methodologies → Heuristic function construction
  • Mathematics of computing → Solvers
Keywords
  • SAT Solver
  • Structure of SAT
  • Parallel application
  • Clause Learning

Metrics

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

References

  1. Carlos Ansótegui, Jesús Giráldez-Cru, and Jordi Levy. The community structure of sat formulas. In Theory and Applications of Satisfiability Testing - SAT 2012, pages 410-423, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. Google Scholar
  2. Gilles Audemard, Benoît Hoessen, Saïd Jabbour, Jean-Marie Lagniez, and Cédric Piette. Revisiting clause exchange in parallel sat solving. In Alessandro Cimatti and Roberto Sebastiani, editors, Theory and Applications of Satisfiability Testing - SAT 2012, pages 200-213, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. Google Scholar
  3. Gilles Audemard, Jean-Marie Lagniez, Bertrand Mazure, and Lakhdar Saïs. On freezing and reactivating learnt clauses. In Karem A. Sakallah and Laurent Simon, editors, Theory and Applications of Satisfiability Testing - SAT 2011, pages 188-200, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. Google Scholar
  4. Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern SAT solvers. In Proceedings of the 21st international jont conference on Artifical intelligence, IJCAI'09, pages 399-404, San Francisco, CA, USA, July 2009. Morgan Kaufmann Publishers Inc. Google Scholar
  5. Gilles Audemard and Laurent Simon. Lazy clause exchange policy for parallel sat solvers. In Carsten Sinz and Uwe Egly, editors, Theory and Applications of Satisfiability Testing - SAT 2014, pages 197-205, Cham, 2014. Springer International Publishing. Google Scholar
  6. Tomas Balyo, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors. Proceedings of SAT Competition 2023: Solver, Benchmark and Proof Checker Descriptions. Department of Computer Science Series of Publications B. Department of Computer Science, University of Helsinki, Finland, 2023. Google Scholar
  7. Tomáš Balyo, Peter Sanders, and Carsten Sinz. Hordesat: A massively parallel portfolio sat solver. In Marijn Heule and Sean Weaver, editors, Theory and Applications of Satisfiability Testing - SAT 2015, pages 156-172, Cham, 2015. Springer International Publishing. Google Scholar
  8. Roberto J. Bayardo and Robert C. Schrag. Using csp look-back techniques to solve real-world sat instances. In Proceedings of the Fourteenth National Conference on Artificial Intelligence and Ninth Conference on Innovative Applications of Artificial Intelligence, AAAI'97/IAAI'97, pages 203-208. AAAI Press, 1997. Google Scholar
  9. Armin Biere and Andreas Frohlich. Evaluating cdcl restart schemes. In Proceedings of Pragmatics of SAT 2015 and 2018, volume 59 of EPiC Series in Computing, pages 1-17. EasyChair, 2019. URL: https://doi.org/10.29007/89dw.
  10. Wolfgang Blochinger, Carsten Sinz, and Wolfgang Küchlin. Parallel propositional satisfiability checking with distributed dynamic learning. Parallel Computing, 29(7):969-994, 2003. URL: https://doi.org/10.1016/S0167-8191(03)00068-1.
  11. Curtis Bright, Ilias Kotsireas, Albert Heinle, and Vijay Ganesh. Complex golay pairs up to length 28: A search via computer algebra and programmatic sat. Journal of Symbolic Computation, 102:153-172, 2021. URL: https://doi.org/10.1016/j.jsc.2019.10.013.
  12. Wenjing Chang, Guanfeng Wu, and Yang Xu. Adding a lbd-based rewarding mechanism in branching heuristic for sat solvers. In 2017 12th International Conference on Intelligent Systems and Knowledge Engineering (ISKE), pages 1-6, 2017. URL: https://doi.org/10.1109/ISKE.2017.8258780.
  13. Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Commun. ACM, 5(7):394-397, July 1962. URL: https://doi.org/10.1145/368273.368557.
  14. Andrea Ferrara, Guoqiang Pan, and Moshe Y. Vardi. Treewidth in verification: Local vs. global. In Logic for Programming, Artificial Intelligence, and Reasoning, pages 489-503, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. Google Scholar
  15. Carla P Gomes, Bart Selman, and Henry Kautz. Boosting combinatorial search through randomization. In 15th national conference on artificial intelligence and 10th conference on Innovative applications of artificial intelligence, pages 431-437. AAAI, 1998. Google Scholar
  16. Youssef Hamadi, Said Jabbour, and Jabbour Sais. Control-Based Clause Sharing in Parallel SAT Solving, pages 245-267. Springer Berlin Heidelberg, Berlin, Heidelberg, 2012. URL: https://doi.org/10.1007/978-3-642-21434-9_10.
  17. Youssef Hamadi, Said Jabbour, and Lakhdar Sais. Manysat: a parallel sat solver. Journal on Satisfiability, Boolean Modeling and Computation, 6(4):245-262, 2010. URL: https://doi.org/10.3233/SAT190070.
  18. Marijn J H Heule, Oliver Kullmann, and Victor W Marek. Solving and verifying the boolean pythagorean triples problem via Cube-and-Conquer. In Theory and Applications of Satisfiability Testing - SAT 2016, pages 228-245, Cham, 2016. Springer. URL: https://doi.org/10.1007/978-3-319-40970-2_15.
  19. Bernardo A. Huberman, Rajan M. Lukose, and Tad Hogg. An economics approach to hard computational problems. Science, 275(5296):51-54, 1997. URL: https://doi.org/10.1126/science.275.5296.51.
  20. Yoichiro Iida, Tomohiro Sonobe, and Mary Inaba. Structural impact of learnt clauses in sat solvers: An empirical analysis. In Pragmatics of SAT, 2023. Google Scholar
  21. Yoichiro Iida, Tomohiro Sonobe, and Inaba Mary. Wance: Learnt clause evaluation method for sat solver using graph structure. In The 18th Learning and Intelligent Optimization Conference (LION 2024), 2024. submitting and under review. Google Scholar
  22. Saïd Jabbour, Jerry Lonlac, Lakhdar Saïs, and Yakoub Salhi. Revisiting the learned clauses database reduction strategies. International journal of artificial intelligence tools: architectures, languages, algorithms, 27(08):1850033, 2018. URL: https://doi.org/10.1142/S0218213018500331.
  23. Sima Jamali and David Mitchell. Centrality-based improvements to cdcl heuristics. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, Theory and Applications of Satisfiability Testing - SAT 2018, pages 122-131, Cham, 2018. Springer International Publishing. Google Scholar
  24. George Katsirelos and Laurent Simon. Eigenvector centrality in industrial sat instances. In Michela Milano, editor, Principles and Practice of Constraint Programming, pages 348-356, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. Google Scholar
  25. Nadjib Lazaar, Youssef Hamadi, Said Jabbour, and Michèle Sebag. Cooperation control in parallel sat solving: a multi-armed bandit approach. Technical report, Institut National de Recherche en Informatique et en Automatique, 2012. Google Scholar
  26. Ludovic Le Frioux, Souheib Baarir, Julien Sopena, and Fabrice Kordon. Painless: A framework for parallel sat solving. In Serge Gaspers and Toby Walsh, editors, Theory and Applications of Satisfiability Testing - SAT 2017, pages 233-250, Cham, 2017. Springer International Publishing. Google Scholar
  27. Jia Hui Liang, Hari Govind V.K., Pascal Poupart, Krzysztof Czarnecki, and Vijay Ganesh. An empirical study of branching heuristics through the lens of global learning rate. In Serge Gaspers and Toby Walsh, editors, Theory and Applications of Satisfiability Testing - SAT 2017, pages 119-135, Cham, 2017. Springer International Publishing. Google Scholar
  28. 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.
  29. M.W. Moskewicz, C.F. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: engineering an efficient sat solver. In Proceedings of the 38th Design Automation Conference (IEEE Cat. No.01CH37232), pages 530-535, 2001. URL: https://doi.org/10.1145/378239.379017.
  30. Zack Newsham, Vijay Ganesh, Sebastian Fischmeister, Gilles Audemard, and Laurent Simon. Impact of community structure on sat solver performance. In Theory and Applications of Satisfiability Testing - SAT 2014, pages 252-268, Cham, 2014. Springer International Publishing. Google Scholar
  31. Zack Newsham, William Lindsay, Vijay Ganesh, Jia Hui Liang, Sebastian Fischmeister, and Krzysztof Czarnecki. Satgraf: Visualizing the evolution of sat formula structure in solvers. In Marijn Heule and Sean Weaver, editors, Theory and Applications of Satisfiability Testing - SAT 2015, pages 62-70, Cham, 2015. Springer International Publishing. Google Scholar
  32. Nicolas Prevot, Mate Soos, and Kuldeep S. Meel. Leveraging gpus for effective clause sharing in parallel sat solving. In Chu-Min Li and Felip Manyà, editors, Theory and Applications of Satisfiability Testing - SAT 2021, pages 471-487, Cham, 2021. Springer International Publishing. Google Scholar
  33. Dominik Schreiber and Peter Sanders. Scalable sat solving in the cloud. In Chu-Min Li and Felip Manyà, editors, Theory and Applications of Satisfiability Testing - SAT 2021, pages 518-534, Cham, 2021. Springer International Publishing. Google Scholar
  34. Bart Selman, Henry Kautz, and Bram Cohen. Local search strategies for satisfiability testing. Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge, 26:521-532, September 1996. Google Scholar
  35. Vincent Vallade, Ludovic Le Frioux, Souheib Baarir, Julien Sopena, Vijay Ganesh, and Fabrice Kordon. Community and lbd-based clause sharing policy for parallel sat solving. In Theory and Applications of Satisfiability Testing - SAT 2020, pages 11-27, Cham, 2020. Springer International Publishing. Google Scholar
  36. Richard Williams, Carla Gomes, and Bart Selman. On the connections between backdoors, restarts, and heavy-tailedness in combinatorial search. In Theory and Applications of Satisfiability Testing 2003, 2003. Google Scholar
  37. Edward Zulkoski, Ruben Martins, Christoph M. Wintersteiger, Jia Hui Liang, Krzysztof Czarnecki, and Vijay Ganesh. The effect of structural measures and merges on sat solver performance. In Principles and Practice of Constraint Programming, pages 436-452, Cham, 2018. Springer International Publishing. 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