Document Open Access Logo

CaDiCaL 3.0 (Tool Paper)

Authors Florian Pollitt , Mathias Fleury , Katalin Fazekas , Nils Froleyks , André Schidler , Dominik Schreiber , Armin Biere

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.40.pdf
  • Filesize: 1.02 MB
  • 14 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Incremental SAT
  • CaDiCaL
  • SAT Solver

Metrics

Abstract

The propositional satisfiability (SAT) solver Kissat supports a relatively narrow feature set in favor of bare-metal performance and targeted improvements to core solving techniques, which helped it dominate the International SAT Competition since 2024. However, many applications rely on advanced SAT solver features such as incremental interaction schemes, finding direct consequences of assumed literals, or expressive proof logging that allows for real-time checking. This system description reports on how we successfully adapted Kissat’s award-winning techniques to the full-featured incremental SAT solver CaDiCaL, including clausal congruence closure, clausal equivalence sweeping, and bounded variable addition. The main challenge was to support efficient linear proof production with hints. We further extended CaDiCaL’s API to extract implied literals under assumptions and applied advanced deterministic scheduling of inprocessing based on the ticks metric for approximating cache line accesses. Experiments confirm the benefits of these efforts.

Cite As Get BibTex

Florian Pollitt, Mathias Fleury, Katalin Fazekas, Nils Froleyks, André Schidler, Dominik Schreiber, and Armin Biere. CaDiCaL 3.0 (Tool Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 40:1-40:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.SAT.2026.40

Author Details

Florian Pollitt
  • University of Freiburg, Germany
Mathias Fleury
  • University of Freiburg, Germany
Katalin Fazekas
  • TU Wien, Austria
Nils Froleyks
  • Johannes Kepler University Linz, Austria
André Schidler
  • University of Freiburg, Germany
Dominik Schreiber
  • Karlsruhe Institute of Technology, Germany
Armin Biere
  • University of Freiburg, Germany

Funding

Supported by Austrian Science Fund (FWF) projects T-1306, W1255-N23, and S11408-N23, the state of Baden-Württemberg through bwHPC, German Research Foundation (DFG) through grant INST 35/1597-1 FUGG, and by a gift from Intel Corporation.

Supplementary Materials

References

  1. 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, San Francisco, CA, USA, 2009. Morgan Kaufmann Publishers Inc. URL: http://ijcai.org/Proceedings/09/Papers/074.pdf.
  2. 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.
  3. Seulkee Baek, Mario Carneiro, and Marijn J. H. Heule. A flexible proof format for SAT solver-elaborator communication. 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 I, volume 12651 of Lecture Notes in Computer Science, pages 59-75. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72016-2_4.
  4. Seulkee Baek, Mario Carneiro, and Marijn J. H. Heule. A flexible proof format for SAT solver-elaborator communication. Log. Methods Comput. Sci., 18(2), 2022. URL: https://doi.org/10.46298/LMCS-18(2:3)2022.
  5. Tomás Balyo, Armin Biere, Markus Iser, and Carsten Sinz. SAT Race 2015. Artif. Intell., 241:45-65, 2016. URL: https://doi.org/10.1016/J.ARTINT.2016.08.007.
  6. Tomás Balyo, Andreas Fröhlich, Marijn Heule, and Armin Biere. Everything you always wanted to know about blocked sets (but were afraid to ask). In Carsten Sinz and Uwe Egly, editors, Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8561 of LNCS, pages 317-332. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_24.
  7. Tomas Balyo, Marijn J. H. 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
  8. Armin Biere. Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. Technical Report 10/1, Johannes Kepler University Linz, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria, 2010. URL: https://doi.org/10.350/fmvtr.2010-1.
  9. Armin Biere. Lingeling essentials, a tutorial on design and implementation aspects of the SAT solver Lingeling. In Daniel Le Berre, editor, POS-14. Fifth Pragmatics of SAT workshop, volume 27 of EPiC Series in Computing, page 88. EasyChair, 2014. URL: https://doi.org/10.29007/jhd7.
  10. Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. Cadical 2.0. In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I, volume 14681 of LNCS, pages 133-152. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-65627-9_7.
  11. Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. CaDiCaL, Gimsatul, IsaSAT and Kissat entering the SAT Competition 2024. In Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors, Proc. of SAT Competition 2024 - Solver, Benchmark and Proof Checker Descriptions, volume B-2024-1 of Department of Computer Science Report Series B, pages 8-10. University of Helsinki, 2024. Google Scholar
  12. Armin Biere, Katalin Fazekas, Mathias Fleury, and Nils Froleyks. Clausal congruence closure. In Supratik Chakraborty and Jie-Hong Roland Jiang, editors, 27th International Conference on Theory and Applications of Satisfiability Testing, SAT 2024, August 21-24, 2024, Pune, India, volume 305 of LIPIcs, pages 6:1-6:25. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.SAT.2024.6.
  13. Armin Biere, Katalin Fazekas, Mathias Fleury, and Nils Froleyks. Clausal equivalence sweeping. In Nina Narodytska and Philipp Rümmer, editors, Proceedings 24th International Conference on Formal Methods in Computer-Aided Design (FMCAD'24), pages 236-241. TU Wien Academic Press, 2024. URL: https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_29.
  14. 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 J. H. 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
  15. Armin Biere, Nils Froleyks, and Mathias Preiner. Hardware model checking competition 2025. In Ahmed Irfan and Daniela Kaufmann, editors, Proceedings of the 25th Conference on Formal Methods in Computer-Aided Design, FMCAD 2025, Menlo Park, CA, USA, October 6-10, 2025. TU Wien Academic Press, 2025. URL: https://doi.org/10.34727/2025/ISBN.978-3-85448-084-6_6.
  16. Armin Biere, Nils Froleyks, and Wenxi Wang. CadiBack: Extracting backbones with CaDiCaL. In Meena Mahajan and Friedrich Slivovsky, editors, 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy, volume 271 of LIPIcs, pages 3:1-3:12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.SAT.2023.3.
  17. Armin Biere, Matti Järvisalo, and Bejamin Kiesl. Preprocessing in SAT solving. In Armin Biere, Marijn J. H. 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, 2nd edition edition, 2021. URL: https://doi.org/10.3233/FAIA200992.
  18. Armin Biere and Florian Pollitt. LRAT trimmer, Last access, February 2026. Source code. URL: https://github.com/arminbiere/lrat-trim.
  19. Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Certified dominance and symmetry breaking for combinatorial optimisation. Journal of Artificial Intelligence Research, 77:1539-1589, August 2023. Preliminary version in AAAI '22. URL: https://doi.org/10.1613/JAIR.1.14296.
  20. Luís Cruz-Filipe, Marijn J. H. Heule, Jr. Hunt, Warren A., Matt Kaufmann, and Peter Schneider-Kamp. Efficient certified RAT verification. In Leonardo de Moura, editor, Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, volume 10395 of LNCS, pages 220-236. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63046-5_14.
  21. Luís Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt, Matt Kaufmann, and Peter Schneider-Kamp. Efficient certified RAT verification. In Leonardo de Moura, editor, Automated Deduction - CADE 26, pages 220-236, Cham, 2017. Springer International Publishing. Google Scholar
  22. Hang Ding, Mao Luo, Chu-Min Li, Shunwei Li, Runyao Chen, Caiquan Xiong, and Xinyun Wu. A self-optimizing framework for sat solvers via population evolution and large language model collaboration. In Cayden Codel, Katalin Fazekas, Marijn Heule, and Markus Iser, editors, Proceedings of SAT Competition 2025: Solver and Benchmark Descriptions, Proceedings of SAT Competitions, pages 15-17. TU Wien Academic Press, 2025. URL: https://doi.org/10.34726/10379.
  23. 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 LNCS, pages 502-518. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-24605-3_37.
  24. Katalin Fazekas. On SAT-based Solution Methods for Computational Problems. PhD thesis, Informatik, Johannes Kepler University Linz, 2020. Google Scholar
  25. Katalin Fazekas, Armin Biere, and Christoph Scholl. Incremental inprocessing in SAT solving. 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 LNCS, pages 136-154. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-24258-9_9.
  26. Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, and Armin Biere. IPASIR-UP: user propagators for CDCL. In Meena Mahajan and Friedrich Slivovsky, editors, 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy, volume 271 of LIPIcs, pages 8:1-8:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.SAT.2023.8.
  27. Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, and Armin Biere. Satisfiability modulo user propagators. J. Artif. Intell. Res., 81:989-1017, 2024. URL: https://doi.org/10.1613/JAIR.1.16163.
  28. Katalin Fazekas, Florian Pollitt, Mathias Fleury, and Armin Biere. Certifying incremental SAT solving. In Nikolaj S. Bjørner, Marijn Heule, and Andrei Voronkov, editors, LPAR 2024: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, Port Louis, Mauritius, May 26-31, 2024, volume 100 of EPiC Series in Computing, pages 321-340. EasyChair, 2024. URL: https://doi.org/10.29007/PDCC.
  29. Katalin Fazekas, Florian Pollitt, Mathias Fleury, and Armin Biere. Incremental proofs for bounded model checking. In Wolfgang Kunz, editor, 27th GMM/ITG/GI Workshop on Methods and Description Languages for Modelling and Verification of Circuits and Systems (MBMV'24), Kaiserslautern, Germany, volume 314 of ITG-Fachberichte, pages 133-143. VDE Verlag, 2024. Google Scholar
  30. Katalin Fazekas, Florian Pollitt, Mathias Fleury, and Armin Biere. Incremental inprocessing rules beyond resolution. In Jochen Hoenicke, Mikoláš Janota, Aina Niemetz, and Sophie Tourret, editors, Proceedings 16'th Pragmatics of SAT International Workshop (POS'25), co-located with the 28th International Conference on Theory and Applications of Satisfiability Testing (SAT'23), number 4008 in CEUR Workshop Proceedings, pages 190-200, 2025. URL: https://ceur-ws.org/Vol-4008.
  31. Mathias Fleury and Armin Biere. Mining definitions in Kissat with Kittens. Formal Methods Syst. Des., 60(3):381-404, 2022. URL: https://doi.org/10.1007/S10703-023-00421-2.
  32. Nils Froleyks, Emily Yu, and Armin Biere. BIG backbones. In Alexander Nadel and Kristin Yvonne Rozier, editors, Formal Methods in Computer-Aided Design, FMCAD 2023, Ames, IA, USA, October 24-27, 2023, pages 162-167. IEEE, 2023. URL: https://doi.org/10.34727/2023/ISBN.978-3-85448-060-0_24.
  33. Andrew Haberlandt and Harrison Green. SBVA-CaDiCaL and SBVA-Kissat: Structured bounded variable addition. In Tomas Balyo, Nils Froleyks, Marijn J. H. Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors, Proc. of SAT Competition 2023 - Solver and Benchmark Descriptions, volume B-2023-1 of Department of Computer Science Report Series B, page 18. University of Helsinki, 2023. Google Scholar
  34. Marijn Heule. Checkr of DPR proof files, Last access, April 2024. Source code. URL: https://github.com/marijnheule/dpr-trim.
  35. Marijn J. H. Heule. Proofs of unsatisfiability. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 635-668. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA200998.
  36. Marijn J. H. Heule and Armin Biere. Blocked clause decomposition. In Kenneth L. McMillan, Aart Middeldorp, and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings, volume 8312 of LNCS, pages 423-438. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-45221-5_29.
  37. Marijn J. H. Heule and Armin Biere. Proofs for satisfiability problems. In All about Proofs, Proofs for All (APPA), volume 55 of Math. Logic and Foundations. College Pub., 2015. Google Scholar
  38. Marijn J.H. Heule, Warren A. Hunt, and Nathan Wetzler. Trimming while checking clausal proofs. In 2013 Formal Methods in Computer-Aided Design, pages 181-188, 2013. URL: https://doi.org/10.1109/FMCAD.2013.6679408.
  39. Alexey Ignatiev, António Morgado, and João Marques-Silva. PySAT: A Python toolkit for prototyping with SAT oracles. 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 LNCS, pages 428-437. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94144-8_26.
  40. Alexey Ignatiev, António Morgado, and João Marques-Silva. RC2: an efficient MaxSAT solver. J. Satisf. Boolean Model. Comput., 11(1):53-64, 2019. URL: https://doi.org/10.3233/SAT190116.
  41. Alexey Ignatiev, Zi Li Tan, and Christos Karamanos. Towards universally accessible SAT technology. In SAT, pages 4:1-4:11, 2024. URL: https://doi.org/10.4230/LIPIcs.SAT.2024.16.
  42. Donald E. Knuth. The Art of Computer Programming, Volume 4, Fascicle 4: Generating All Trees-History of Combinatorial Generation (Art of Computer Programming). Addison-Wesley Professional, 2006. Google Scholar
  43. Peter Lammich. The GRAT tool chain - efficient (UN)SAT certificate checking with formal correctness guarantees. In Serge Gaspers and Toby Walsh, editors, Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, volume 10491 of LNCS, pages 457-463. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66263-3_29.
  44. Daniel Le Berre, Olivier Roussel, and Laurent Simon. SAT competition 2009: Benchmark submission guidelines. https://web.archive.org/web/20190325181937/https://www.satcompetition.org/2009/format-benchmarks2009.html. Accessed: 2024-01-15.
  45. Norbert Manthey, Marijn J. H. Heule, and Armin Biere. Automated reencoding of boolean formulas. In Armin Biere, Amir Nahir, and Tanja Vos, editors, Hardware and Software: Verification and Testing, pages 102-117, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
  46. Dawn Michaelson, Dominik Schreiber, Marijn JH Heule, Benjamin Kiesl-Reiter, and Michael W Whalen. Producing proofs of unsatisfiability with distributed clause-sharing SAT solvers. Journal of Automated Reasoning, 69(2):12, 2025. URL: https://doi.org/10.1007/s10817-025-09725-w.
  47. Hidetomo Nabeshima, Tsubasa Fukiage, Yuto Obitsu, Xiao-Nan Lu, and Katsumi Inoue. Dps: a framework for deterministic parallel sat solvers. EasyChair Preprint 8553, EasyChair, 2022. Google Scholar
  48. Chanseok Oh. Between SAT and UNSAT: the fundamental difference in CDCL SAT. In Theory and Applications of Satisfiability Testing-SAT 2015-18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings, pages 307-323, 2015. URL: https://doi.org/10.1007/978-3-319-24318-4_23.
  49. Florian Pollitt, Mathias Fleury, and Armin Biere. Faster LRAT checking than solving with cadical. In Meena Mahajan and Friedrich Slivovsky, editors, 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy, volume 271 of LIPIcs, pages 21:1-21:12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.SAT.2023.21.
  50. Florian Pollitt, Mathias Fleury, Armin Biere, Karem Sakallah, Marijn Heule, Jiawei Chen, and Yonathan Fisseha. Revisiting clause vivification. In Jochen Hoenicke, Mikoláš Janota, Aina Niemetz, and Sophie Tourret, editors, Proceedings 16'th Pragmatics of SAT International Workshop (POS'25), co-located with the 28th International Conference on Theory and Applications of Satisfiability Testing (SAT'23), number 4008 in CEUR Workshop Proceedings, pages 153-167, 2025. URL: https://ceur-ws.org/Vol-4008.
  51. Florian Pollitt, Mathias Fleury, Katalin Fazekas, Nils Froleyks, André Schidler, Dominik Schreiber, and Armin Biere. Artifact cadical 3.0 paper, March 2026. URL: https://doi.org/10.5281/zenodo.18924223.
  52. Mathias Preiner, Nils Froleyks, and Armin Biere. HWMCC'25 benchmarks and results (version 1). https://doi.org/10.5281/zenodo.17428464, October 2025. URL: https://doi.org/10.5281/ZENODO.17428464.
  53. Dominik Schreiber. Trusted scalable SAT solving with on-the-fly LRAT checking. In Theory and Applications of Satisfiability Testing (SAT), pages 25:1-25:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.SAT.2024.25.
  54. Dominik Schreiber, Katalin Fazekas, Mathias Fleury, and Armin Biere. Real-time proof checking for distributed incremental SAT solving. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2026. To appear. URL: https://satres.kikit.kit.edu/papers/2026-tacas-distrincproof.pdf.
  55. 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 LNCS, pages 244-257. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02777-2_24.
  56. Yong Kiam Tan, Marijn J. H. Heule, and Magnus O. Myreen. cake_lpr: Verified propagation redundancy checking in CakeML. 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 LNCS, pages 223-241. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72013-1_12.
  57. Yong Kiam Tan, Jiong Yang, Mate Soos, Magnus O. Myreen, and Kuldeep S. Meel. Formally certified approximate model counting. In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I, volume 14681 of LNCS, pages 153-177. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-65627-9_8.
  58. Nathan Wetzler, Marijn J. H. Heule, and Jr. Hunt, Warren A. DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In Carsten Sinz and Uwe Egly, editors, Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8561 of LNCS, pages 422-429. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_31.
  59. Akihisa Yamada, Armin Biere, Cyrille Artho, Takashi Kitamura, and Eun-Hye Choi. Greedy combinatorial test case generation using unsatisfiable cores. In David Lo, Sven Apel, and Sarfraz Khurshid, editors, Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, ASE 2016, Singapore, September 3-7, 2016, pages 614-624. ACM, 2016. URL: https://doi.org/10.1145/2970276.2970335.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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