Document Open Access Logo

WhyUnsat: A Practical Explanation Tool (Tool Paper)

Authors Robert Nieuwenhuis , Albert Oliveras , Enric Rodríguez-Carbonell

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.39.pdf
  • Filesize: 0.64 MB
  • 10 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation
Keywords
  • SAT
  • SMT
  • Constraint Programming
  • Lazy Clause Generation

Metrics

Abstract

Hard industrial planning, timetabling or scheduling instances for SAT typically have many high-level constraints, each expressed by a possibly large number of clauses. When a given instance is reported unsatisfiable by the SAT solver, the user normally needs an explanation why: a (hopefully small) subset of the constraints causing it. Our industrial applications require fast explanations, preferably faster than the original SAT run. For this, we leverage the original solver’s work through its unsatisfiability proof.
Here we introduce WhyUnsat, and explain why it is fast and robust. In WhyUnsat one can always plug in the best current SAT solver and proof trimmer, without any modification, by simply indicating the path to their executables. WhyUnsat is also fast because it exploits, via MPI, the -progressively cheaper- shared-memory and distributed computing resources. Another requirement we had is that the tool should be anytime and user-friendly; indeed, it quickly shows a human-readable presentation of (an over-approximation of) the explanation, which is then progressively reduced until minimality (unless interrupted by the user).
Finally, and not less importantly, here we explain how and why the WhyUnsat approach is now also directly applicable, at no implementation cost, to IPASIR-UP-based constraint programming by Lazy Clause Generation (LCG) as well as to SAT Modulo Theories (SMT).

Cite As Get BibTex

Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez-Carbonell. WhyUnsat: A Practical Explanation Tool (Tool Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 39:1-39:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.SAT.2026.39

Author Details

Robert Nieuwenhuis
  • Technical University of Catalonia, Barcelona, Spain
Albert Oliveras
  • Technical University of Catalonia, Barcelona, Spain
Enric Rodríguez-Carbonell
  • Technical University of Catalonia, Barcelona, Spain

Funding

All authors are supported by grant PID2024-157044OB-C32, funded by MICIU /AEI /10.13039/501100011033 / FEDER, UE.

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. R. R. Bakker, F. Dikker, F. Tempelman, and P. M. Wognum. Diagnosing and solving over-determined constraint satisfaction problems. In Ruzena Bajcsy, editor, Procs 13th IJCAI, pages 276-281, 1993. URL: http://ijcai.org/Proceedings/93-1/Papers/039.pdf.
  3. Tomás Balyo, Armin Biere, Ashlin Iser, and Carsten Sinz. SAT race 2015. Artif. Intell., 241:45-65, 2016. URL: https://doi.org/10.1016/J.ARTINT.2016.08.007.
  4. Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. cvc5: A versatile and industrial-strength SMT solver. In Dana Fisman and Grigore Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, volume 13243 of Lecture Notes in Computer Science, pages 415-442. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99524-9_24.
  5. Anton Belov, Marijn JH Heule, and Joao Marques-Silva. Mus extraction using clausal proofs. In Theory and Applications of Satisfiability Testing-SAT 2014: 17th International Conference, Vienna, Austria, July 14-17, 2014. Proceedings, pages 48-57. Springer, 2014. Google Scholar
  6. Anton Belov, Norbert Manthey, and Joao Marques-Silva. Parallel mus extraction. In Matti Järvisalo and Allen Van Gelder, editors, Theory and Applications of Satisfiability Testing - SAT 2013, pages 133-149, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
  7. Anton Belov and João Marques-Silva. Muser2: An efficient MUS extractor. J. Satisf. Boolean Model. Comput., 8(3/4):123-128, 2012. URL: https://doi.org/10.3233/SAT190094.
  8. 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 Lecture Notes in Computer Science, pages 133-152. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-65627-9_7.
  9. 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
  10. John W. Chinneck and Erik W. Dravnieks. Locating minimal infeasible constraint sets in linear programs. INFORMS J. Comput., 3(2):157-168, 1991. URL: https://doi.org/10.1287/IJOC.3.2.157.
  11. Nachum Dershowitz, Ziyad Hanna, and Alexander Nadel. A scalable algorithm for minimal unsatisfiable core extraction. 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 36-41. Springer, 2006. URL: https://doi.org/10.1007/11814948_5.
  12. Niklas Eén and Niklas Sörensson. Temporal induction by incremental sat solving. Electronic Notes in Theoretical Computer Science, 89(4):543-560, 2003. BMC'2003, First International Workshop on Bounded Model Checking. URL: https://doi.org/10.1016/S1571-0661(05)82542-3.
  13. Katalin Fazekas, Uwe Egly, Marijn JH Heule, Stefan Szeider, and Armin Biere. Satisfiability modulo user propagators. Journal of Artificial Intelligence Research, 81:989-1017, 2024. URL: https://doi.org/10.1613/jair.1.16163.
  14. Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere. Strong extension-free proof systems. J. Autom. Reason., 64(3):533-554, 2020. URL: https://doi.org/10.1007/S10817-019-09516-0.
  15. Mark H. Liffiton and Karem A. Sakallah. Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reason., 40(1):1-33, 2008. URL: https://doi.org/10.1007/S10817-007-9084-Z.
  16. João Marques-Silva and Inês Lynce. On improving MUS extraction algorithms. In Karem A. Sakallah and Laurent Simon, editors, Theory and Applications of Satisfiability Testing - SAT 2011 - 14th International Conference, SAT 2011, Ann Arbor, MI, USA, June 19-22, 2011. Proceedings, volume 6695 of Lecture Notes in Computer Science, pages 159-173. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-21581-0_14.
  17. Alexander Nadel. Boosting minimal unsatisfiable core extraction. In Roderick Bloem and Natasha Sharygina, editors, Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, Lugano, Switzerland, October 20-23, pages 221-229. IEEE, 2010. URL: https://ieeexplore.ieee.org/document/5770953/.
  18. Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez-Carbonell. enric-rodriguez/WhyUnsat. Software, (visited on 2026-05-26). URL: https://github.com/enric-rodriguez/WhyUnsat
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.26035
  19. Olga Ohrimenko, Peter J. Stuckey, and Michael Codish. Propagation = lazy clause generation. In Christian Bessiere, editor, CP, volume 4741 of Lecture Notes in Computer Science, pages 544-558. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74970-7_39.
  20. Vadim Ryvchin and Ofer Strichman. Faster extraction of high-level minimal unsatisfiable cores. In Karem A. Sakallah and Laurent Simon, editors, Theory and Applications of Satisfiability Testing - SAT 2011 - 14th International Conference, SAT 2011, Ann Arbor, MI, USA, June 19-22, 2011. Proceedings, volume 6695 of Lecture Notes in Computer Science, pages 174-187. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-21581-0_15.
  21. Peter J. Stuckey. There are no CNF problems. In Matti Järvisalo and Allen Van Gelder, editors, Theory and Applications of Satisfiability Testing - SAT, volume 7962 of LNCS, pages 19-21. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39071-5_3.
  22. L. Zhang and S. Malik. Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications. In 2003 Conference on Design, Automation and Test in Europe Conference, DATE '03, pages 10880-10885. IEEE Computer Society, 2003. URL: https://doi.org/10.1109/DATE.2003.10014.
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