Document Open Access Logo

Solving Huge Instances with Intel(R) SAT Solver

Author Alexander Nadel

PDF
Thumbnail PDF

File

LIPIcs.SAT.2023.17.pdf
  • Filesize: 0.75 MB
  • 12 pages

Document Identifiers

Author Details

Alexander Nadel
  • Intel Corporation, Haifa, Israel
  • Faculty of Data and Decision Sciences, Technion, Haifa, Israel

Cite AsGet BibTex

Alexander Nadel. Solving Huge Instances with Intel(R) SAT Solver. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 17:1-17:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.SAT.2023.17

Abstract

We introduce a new release of our SAT solver Intelregistered SAT Solver. The new release, called IS23, is targeted to solve huge instances beyond the capacity of other solvers. IS23 can use 64-bit clause-indices and store clauses compressedly using bit-arrays, where each literal is normally allocated fewer than 32 bits. As a preliminary result, we show that only IS23 can handle a gigantic trivially satisfiable instance with over 8.5 billion clauses. Then, we demonstrate that IS23 enables a significant improvement in the capacity of our industrial tool for cell placement in physical design, since only IS23 can solve placement instances with up to 4.3 billion clauses. Finally, we show that IS23 is substantially more efficient than other solvers for finding many (10⁶) placements on instances with up to 170 million clauses. We use the latter application to demonstrate that variable succession, that is, the order in which the variables are provided to the solver, might have a significant impact on IS23’s performance, thereby providing a new dimension to SAT encoding considerations.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Solvers
Keywords
  • SAT
  • CDCL

Metrics

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

Supplementary Materials

References

  1. Gilles Audemard and Laurent Simon. On the glucose SAT solver. Int. J. Artif. Intell. Tools, 27(1):1840001:1-1840001:25, 2018. URL: https://doi.org/10.1142/S0218213018400018.
  2. Tomas Balyo, Marijn J.H. Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors. Proceedings of SAT Competition 2022: Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B. Department of Computer Science, University of Helsinki, Finland, 2022. Google Scholar
  3. Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The SMT-LIB Standard: Version 2.6. Technical report, Department of Computer Science, The University of Iowa, 2017. Available at URL: http://smt-lib.org/.
  4. 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
  5. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability, volume 336 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2021. Google Scholar
  6. Armin Biere, Matti Järvisalo, and Benjamin Kiesl. Preprocessing in sat solving. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 391-435. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA200992.
  7. Geoffrey Chu, Aaron Harwood, and Peter J. Stuckey. Cache conscious data structures for boolean satisfiability solvers. J. Satisf. Boolean Model. Comput., 6(1-3):99-120, 2009. URL: https://doi.org/10.3233/sat190064.
  8. Aviad Cohen, Alexander Nadel, and Vadim Ryvchin. Local search with a SAT oracle for combinatorial optimization. In Jan Friso Groote and Kim Guldstrand Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II, volume 12652 of Lecture Notes in Computer Science, pages 87-104. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72013-1_5.
  9. 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.
  10. Vijay Ganesh and David L. Dill. A decision procedure for bit-vectors and arrays. In Werner Damm and Holger Hermanns, editors, Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings, volume 4590 of Lecture Notes in Computer Science, pages 519-531. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73368-3_52.
  11. Orna Grumberg, Assaf Schuster, and Avi Yadgar. Memory efficient all-solutions SAT solver and its application for reachability analysis. In Alan J. Hu and Andrew K. Martin, editors, Formal Methods in Computer-Aided Design, 5th International Conference, FMCAD 2004, Austin, Texas, USA, November 15-17, 2004, Proceedings, volume 3312 of Lecture Notes in Computer Science, pages 275-289. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30494-4_20.
  12. Jinbo Huang and Adnan Darwiche. The language of search. J. Artif. Intell. Res., 29:191-219, 2007. URL: https://doi.org/10.1613/jair.2097.
  13. Richard Korf, Michael Moffitt, and Martha Pollack. Optimal rectangle packing. Annals OR, 179:261-295, September 2010. URL: https://doi.org/10.1007/s10479-008-0463-6.
  14. Chu-Min Li, Fan Xiao, Mao Luo, Felip Manyà, Zhipeng Lü, and Yu Li. Clause vivification by unit propagation in CDCL SAT solvers. Artif. Intell., 279, 2020. URL: https://doi.org/10.1016/j.artint.2019.103197.
  15. Norbert Manthey. The mergesat solver. In Chu-Min Li and Felip Manyà, editors, Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings, volume 12831 of Lecture Notes in Computer Science, pages 387-398. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_27.
  16. Kenneth L. McMillan. Applying SAT methods in unbounded symbolic model checking. In Ed Brinksma and Kim Guldstrand Larsen, editors, Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings, volume 2404 of Lecture Notes in Computer Science, pages 250-264. Springer, 2002. URL: https://doi.org/10.1007/3-540-45657-0_19.
  17. 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.
  18. Alexander Nadel. Introducing intel(r) SAT solver. In Kuldeep S. Meel and Ofer Strichman, editors, 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2-5, 2022, Haifa, Israel, volume 236 of LIPIcs, pages 8:1-8:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.8.
  19. Alexander Nadel. Intelregistered SAT Solver. https://github.com/alexander-nadel/intel_sat_solver, 2022-2023.
  20. Alexander Nadel. Solving huge instances with intelregistered sat solver: Supplementary material. https://technionmail-my.sharepoint.com/:f:/g/personal/alexandernad_technion_ac_il/EtihJbiS1XBJoi0DRTGbCnIBlfs1__hkPRiZ3uTpIR_x_g, 2023.
  21. Alexander Nadel and Vadim Ryvchin. Efficient SAT solving under assumptions. In Alessandro Cimatti and Roberto Sebastiani, editors, Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings, volume 7317 of Lecture Notes in Computer Science, pages 242-255. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31612-8_19.
  22. Collin Peterson. How to define and work with an array of bits in C?, November 2020. URL: https://stackoverflow.com/a/30590727.
  23. Naveed A. Sherwani. Algorithms for VLSI physical design automation. Kluwer, 3 edition, November 1998. Google Scholar
  24. Mate Soos. Allow memory to grow larger than 4gb per thread. https://github.com/msoos/cryptominisat/issues/389, May 2017.
  25. Mate Soos, Karsten Nohl, and Claude Castelluccia. Extending SAT solvers to cryptographic problems. In Oliver Kullmann, editor, Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings, volume 5584 of Lecture Notes in Computer Science, pages 244-257. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02777-2_24.
  26. Marc Thurley. sharpSAT - Counting models with advanced component caching and implicit BCP. 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 424-429. Springer, 2006. URL: https://doi.org/10.1007/11814948_38.
  27. Takahisa Toda. Implementing efficient all solutions SAT solvers. J. Exp. Algorithmics, 21:1, 2016. URL: https://doi.org/10.1145/2975585.
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