Document Open Access Logo

Introducing Intel(R) SAT Solver

Author Alexander Nadel

PDF
Thumbnail PDF

File

LIPIcs.SAT.2022.8.pdf
  • Filesize: 0.94 MB
  • 23 pages

Document Identifiers

Author Details

Alexander Nadel
  • Intel Corporation, Haifa, Israel

Cite AsGet BibTex

Alexander Nadel. Introducing Intel(R) SAT Solver. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 8:1-8:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.SAT.2022.8

Abstract

We introduce Intel(R) SAT Solver (IntelSAT) - a new open-source CDCL SAT solver, written from scratch. IntelSAT is optimized for applications which generate many mostly satisfiable incremental SAT queries. We apply the following Incremental Lazy Backtracking (ILB) principle: in-between incremental queries, backtrack only when necessary and to the highest possible decision level. ILB is enabled by a novel reimplication procedure, which can reimply an assigned literal at a lower level without backtracking. Reimplication also helped us to restore the following two properties, lost in the modern solvers with the introduction of chronological backtracking: no assigned literal can be implied at a lower level, conflict analysis always starts with a clause falsified at the lowest possible level. In addition, we apply some new heuristics. Integrating IntelSAT into the MaxSAT solver TT-Open-WBO-Inc resulted in a significant performance boost on incomplete unweighted MaxSAT Evaluation benchmarks and improved the state-of-the-art in anytime unweighted MaxSAT solving.

Subject Classification

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

Metrics

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

Supplementary Materials

References

  1. Carlos Ansótegui, Felip Manyà, Jesus Ojeda, Josep M. Salvia, and Eduard Torres. Incomplete maxsat approaches for combinatorial testing. CoRR, abs/2105.12552, 2021. URL: http://arxiv.org/abs/2105.12552.
  2. Gilles Audemard, Jean-Marie Lagniez, Bertrand Mazure, and Lakhdar Sais. RCL: Reduce learnt clauses. https://baldur.iti.kit.edu/sat-race-2010/descriptions/solver_10.pdf, 2010. Online; accessed 23 December 2021.
  3. Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern SAT solvers. In Craig Boutilier, editor, IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, California, USA, July 11-17, 2009, pages 399-404, 2009. URL: http://ijcai.org/Proceedings/09/Papers/074.pdf.
  4. 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.
  5. Fahiem Bacchus. MaxSat Lib. https://www.cs.toronto.edu/maxsat-lib/. Online; accessed 5 January 2022.
  6. Fahiem Bacchus, Jeremias Berg, Matti Järvisalo, and Ruben Martins, editors. MaxSAT Evaluation 2020: Solver and Benchmark Descriptions, Department of Computer Science Report Series B. University of Helsinki, 2020. Google Scholar
  7. Fahiem Bacchus, Jeremias Berg, Matti Järvisalo, and Ruben Martins, editors. MaxSAT Evaluation 2021: Solver and Benchmark Descriptions, Department of Computer Science Report Series B. University of Helsinki, 2021. Google Scholar
  8. Fahiem Bacchus, Matti Järvisalo, and Ruben Martins. Maximum satisfiabiliy. 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 929-991. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA201008.
  9. Paul Beame, Henry A. Kautz, and Ashish Sabharwal. Towards understanding and harnessing the potential of clause learning. CoRR, abs/1107.0044, 2011. URL: http://arxiv.org/abs/1107.0044.
  10. Daniel Le Berre and Anne Parrain. The sat4j library, release 2.2. JSAT, 7(2-3):59-6, 2010. URL: http://jsat.ewi.tudelft.nl/content/volume7/JSAT7_4_LeBerre.pdf, URL: https://doi.org/10.3233/sat190075.
  11. 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.
  12. 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
  13. Armin Biere and Mathias Fleury. Chasing target phases. In Pragmatics of SAT (PoS), 2020. Google Scholar
  14. 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.
  15. 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
  16. 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.
  17. Shaowei Cai and Zhendong Lei. Old techniques in new ways: Clause weighting, unit propagation and hybridization for maximum satisfiability. Artif. Intell., 287:103354, 2020. URL: https://doi.org/10.1016/j.artint.2020.103354.
  18. Shaowei Cai and Xindi Zhang. Deep cooperation of CDCL and local search for SAT. 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 64-81. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_6.
  19. 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.
  20. Nachum Dershowitz, Ziyad Hanna, and Alexander Nadel. Towards a better understanding of the functionality of a conflict-driven SAT solver. In João Marques-Silva and Karem A. Sakallah, editors, Theory and Applications of Satisfiability Testing - SAT 2007, 10th International Conference, Lisbon, Portugal, May 28-31, 2007, Proceedings, volume 4501 of Lecture Notes in Computer Science, pages 287-293. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-72788-0_27.
  21. Rohit Dureja, Arie Gurfinkel, Alexander Ivrii, and Yakir Vizel. IC3 with internal signals. In Formal Methods in Computer Aided Design, FMCAD 2021, New Haven, CT, USA, October 19-22, 2021, pages 63-71. IEEE, 2021. URL: https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_14.
  22. 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.
  23. Nick Feng and Fahiem Bacchus. Clause size reduction with all-uip learning. In Luca Pulina and Martina Seidl, editors, Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings, volume 12178 of Lecture Notes in Computer Science, pages 28-45. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_3.
  24. Andrea Formisano and Flavio Vella. On multiple learning schemata in conflict driven solvers. In Stefano Bistarelli and Andrea Formisano, editors, Proceedings of the 15th Italian Conference on Theoretical Computer Science, Perugia, Italy, September 17-19, 2014, volume 1231 of CEUR Workshop Proceedings, pages 133-146. CEUR-WS.org, 2014. URL: http://ceur-ws.org/Vol-1231/long10.pdf.
  25. Alberto Griggio and Marco Roveri. Comparing different variants of the ic3 algorithm for hardware model checking. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 35(6):1026-1039, 2016. URL: https://doi.org/10.1109/TCAD.2015.2481869.
  26. Youssef Hamadi, Saïd Jabbour, and Lakhdar Sais. Learning for dynamic subsumption. Int. J. Artif. Intell. Tools, 19(4):511-529, 2010. URL: https://doi.org/10.1142/S0218213010000303.
  27. HyoJung Han and Fabio Somenzi. On-the-fly clause improvement. 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 209-222. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02777-2_21.
  28. Randy Hickey and Fahiem Bacchus. Speeding up assumption-based SAT. In Mikolás Janota and Inês Lynce, editors, Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings, volume 11628 of Lecture Notes in Computer Science, pages 164-182. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-24258-9_11.
  29. Randy Hickey and Fahiem Bacchus. Trail saving on backtrack. In Luca Pulina and Martina Seidl, editors, Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings, volume 12178 of Lecture Notes in Computer Science, pages 46-61. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_4.
  30. Hao Hu, Mohamed Siala, Emmanuel Hebrard, and Marie-José Huguet. Learning optimal decision trees with maxsat and its integration in adaboost. In Christian Bessiere, editor, Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI 2020, pages 1170-1176. ijcai.org, 2020. URL: https://doi.org/10.24963/ijcai.2020/163.
  31. Stepan Kochemazov. Improving implementation of SAT competitions 2017-2019 winners. In Luca Pulina and Martina Seidl, editors, Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings, volume 12178 of Lecture Notes in Computer Science, pages 139-148. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_11.
  32. Stepan Kochemazov, Alexey Ignatiev, and João Marques-Silva. Assessing progress in SAT solvers through the lens of incremental SAT. 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 280-298. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_20.
  33. Zhendong Lei, Shaowei Cai, Fei Geng, Dongxu Wang, Yongrong Peng, Dongdong Wan, Yiping Deng, and Pinyan Lu. SATLike-c: Solver description. In Fahiem Bacchus, Jeremias Berg, Matti Järvisalo, and Ruben Martins, editors, MaxSAT Evaluation 2021, Department of Computer Science Report Series B, pages 19-20. University of Helsinki, 2021. Google Scholar
  34. Alexandre Lemos, Pedro T. Monteiro, and Inês Lynce. Minimal perturbation in university timetabling with maximum satisfiability. In Emmanuel Hebrard and Nysret Musliu, editors, Integration of Constraint Programming, Artificial Intelligence, and Operations Research - 17th International Conference, CPAIOR 2020, Vienna, Austria, September 21-24, 2020, Proceedings, volume 12296 of Lecture Notes in Computer Science, pages 317-333. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-58942-4_21.
  35. 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.
  36. Jia Hui Liang, Chanseok Oh, Vijay Ganesh, Krzysztof Czarnecki, and Pascal Poupart. MapleCOMSPS, MapleCOMSPS_LRB, MapleCOMSPS_CHB. In Matti Juhani Järvisalo, editor, Proceedings of SAT Competition 2016: Solver and Benchmark Descriptions, Department of Computer Science Series of Publications B, page 52, Finland, 2016. University of Helsinki. Google Scholar
  37. Sibylle Möhle and Armin Biere. Backing backtracking. In Mikolás Janota and Inês Lynce, editors, Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings, volume 11628 of Lecture Notes in Computer Science, pages 250-266. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-24258-9_18.
  38. 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.
  39. Alexander Nadel. Understanding and Improving a Modern SAT Solver. Dissertation, Tel Aviv University, 2009. URL: https://tau-primo.hosted.exlibrisgroup.com/permalink/f/bqa2g2/972TAU_ALMA21235249890004146.
  40. Alexander Nadel. Solving maxsat with bit-vector optimization. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, Theory and Applications of Satisfiability Testing - SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, volume 10929 of Lecture Notes in Computer Science, pages 54-72. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94144-8_4.
  41. Alexander Nadel. Anytime weighted maxsat with improved polarity selection and bit-vector optimization. In Clark W. Barrett and Jin Yang, editors, 2019 Formal Methods in Computer Aided Design, FMCAD 2019, San Jose, CA, USA, October 22-25, 2019, pages 193-202. IEEE, 2019. URL: https://doi.org/10.23919/FMCAD.2019.8894273.
  42. Alexander Nadel. Anytime algorithms for maxsat and beyond. In 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, September 21-24, 2020, page 1. IEEE, 2020. URL: https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_1.
  43. Alexander Nadel. On optimizing a generic function in SAT. In 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, September 21-24, 2020, pages 205-213. IEEE, 2020. URL: https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_28.
  44. Alexander Nadel. Polarity and variable selection heuristics for SAT-based anytime MaxSAT. J. Satisf. Boolean Model. Comput., 12:17-22, 2020. Google Scholar
  45. Alexander Nadel. TT-Open-WBO-Inc-20: an anytime maxsat solver entering MSE’20. In Fahiem Bacchus, Jeremias Berg, Matti Järvisalo, and Ruben Martins, editors, MaxSAT Evaluation 2020, Department of Computer Science Report Series B, pages 32-33. University of Helsinki, 2020. Google Scholar
  46. Alexander Nadel. TT-Open-WBO-Inc-21: an anytime maxsat solver entering MSE’21. In Fahiem Bacchus, Jeremias Berg, Matti Järvisalo, and Ruben Martins, editors, MaxSAT Evaluation 2021, Department of Computer Science Report Series B, pages 21-22. University of Helsinki, 2021. Google Scholar
  47. Alexander Nadel. TT-Open-WBO-Inc-21 with Intelregistered SAT Solver. https://drive.google.com/file/d/1taWT1Kp16xzXp9FWKHzQwjwo80v_0hoh/view?usp=sharing, 2022.
  48. Alexander Nadel. Intelregistered SAT Solver. https://github.com/alexander-nadel/intel_sat_solver, 2022.
  49. 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.
  50. Alexander Nadel and Vadim Ryvchin. Chronological backtracking. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, Theory and Applications of Satisfiability Testing - SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, volume 10929 of Lecture Notes in Computer Science, pages 111-121. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94144-8_7.
  51. Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. Solving SAT and SAT modulo theories: From an abstract davis-putnam-logemann-loveland procedure to dpll(T). J. ACM, 53(6):937-977, 2006. URL: https://doi.org/10.1145/1217856.1217859.
  52. Chanseok Oh. Between SAT and UNSAT: the fundamental difference in CDCL SAT. 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 307-323. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-24318-4_23.
  53. Vadim Ryvchin and Alexander Nadel. Flipped recording. In Pragmatics of SAT (PoS), 2019. Google Scholar
  54. Vadim Ryvchin and Ofer Strichman. Local restarts. 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 271-276. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-79719-7_25.
  55. João P. Marques Silva and Karem A. Sakallah. GRASP - a new search algorithm for satisfiability. In Rob A. Rutenbar and Ralph H. J. M. Otten, editors, Proceedings of the 1996 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 1996, San Jose, CA, USA, November 10-14, 1996, pages 220-227. IEEE Computer Society / ACM, 1996. URL: https://doi.org/10.1109/ICCAD.1996.569607.
  56. Niklas Sörensson and Armin Biere. Minimizing learned clauses. 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 237-243. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02777-2_23.
  57. Peter van der Tak, Antonio Ramos, and Marijn Heule. Reusing the assignment trail in CDCL solvers. J. Satisf. Boolean Model. Comput., 7(4):133-138, 2011. URL: https://doi.org/10.3233/sat190082.
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