Document Open Access Logo

Shapley-Shubik Attribution from Minimal Subsets (Short Paper)

Authors Pablo Martínez-Naredo , Raúl Mencía , Joao Marques-Silva , Carlos Mencía

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.33.pdf
  • Filesize: 1.16 MB
  • 13 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
Keywords
  • Unsatisfiability
  • Shapley-Shubik index
  • MUSes and MCSes

Metrics

Abstract

We address the problem of attributing responsibility to individual clauses for the unsatisfiability of a propositional formula. Recent work adopted the Shapley-Shubik power index, proposing a probabilistic approximation algorithm. However, although polynomial, the required number of SAT solver calls becomes impractical when the input formula is not easy to solve. In such cases, it is often possible to enumerate a partial set of minimal unsatisfiable subsets (MUSes) and minimal correction subsets (MCSes). In this paper, we demonstrate that these subsets can be leveraged to efficiently bound and approximate the Shapley-Shubik index. We introduce a framework that exploits the structural information provided by the available sets to derive useful attribution explanations.

Cite As Get BibTex

Pablo Martínez-Naredo, Raúl Mencía, Joao Marques-Silva, and Carlos Mencía. Shapley-Shubik Attribution from Minimal Subsets (Short Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 33:1-33:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.SAT.2026.33

Author Details

Pablo Martínez-Naredo
  • University of Oviedo, Gijón, Spain
Raúl Mencía
  • University of Oviedo, Gijón, Spain
Joao Marques-Silva
  • ICREA & University of Lleida, Spain
Carlos Mencía
  • University of Oviedo, Gijón, Spain

Funding

This work is supported by the Spanish Government (grants PID2023-152814OB-I00 and PID2022-141746OB-I00) and by the Principality of Asturias (grant SEK-25-GRU-GIC-24-018).

Supplementary Materials

References

  1. Fahiem Bacchus and George Katsirelos. Using minimal correction sets to more efficiently compute minimal unsatisfiable sets. In Computer Aided Verification - 27th International Conference, CAV 2015, Proceedings, Part II, pages 70-86, 2015. URL: https://doi.org/10.1007/978-3-319-21668-3_5.
  2. James Bailey and Peter J. Stuckey. Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In Practical Aspects of Declarative Languages, 7th International Symposium, PADL 2005, Proceedings, pages 174-186, 2005. URL: https://doi.org/10.1007/978-3-540-30557-6_14.
  3. R. R. Bakker, F. Dikker, F. Tempelman, and P. M. Wognum. Diagnosing and solving over-determined constraint satisfaction problems. In Proceedings of the 13th International Joint Conference on Artificial Intelligence, pages 276-281. Morgan Kaufmann, 1993. URL: http://ijcai.org/Proceedings/93-1/Papers/039.pdf.
  4. John F Banzhaf III. Weighted voting doesn't work: A mathematical analysis. Rutgers L. Rev., 19:317, 1965. Google Scholar
  5. Anton Belov, Inês Lynce, and João Marques-Silva. Towards efficient MUS extraction. AI Commun., 25(2):97-116, 2012. URL: https://doi.org/10.3233/AIC-2012-0523.
  6. Jaroslav Bendík and Ivana Cerná. Replication-guided enumeration of minimal unsatisfiable subsets. In Principles and Practice of Constraint Programming - 26th International Conference, CP 2020, Proceedings, volume 12333 of Lecture Notes in Computer Science, pages 37-54. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-58475-7_3.
  7. Jaroslav Bendík and Kuldeep S. Meel. Counting minimal unsatisfiable subsets. In Computer Aided Verification - 33rd International Conference, CAV 2021, Proceedings, Part II, volume 12760 of Lecture Notes in Computer Science, pages 313-336. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-81688-9_15.
  8. Jaroslav Bendík and Kuldeep S. Meel. Hashing-based approximate counting of minimal unsatisfiable subsets. Formal Methods Syst. Des., 63(1):5-39, 2024. URL: https://doi.org/10.1007/S10703-023-00419-W.
  9. Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. Symbolic model checking without bdds. In Tools and Algorithms for Construction and Analysis of Systems, 5th International Conference, TACAS '99, Lecture Notes in Computer Science, pages 193-207. Springer, 1999. URL: https://doi.org/10.1007/3-540-49059-0_14.
  10. 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. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA336.
  11. Elazar Birnbaum and Eliezer L. Lozinskii. Consistent subsets of inconsistent systems: structure and behaviour. J. Exp. Theor. Artif. Intell., 15(1):25-46, 2003. URL: https://doi.org/10.1080/0952813021000026795.
  12. Ignace Bleukx, Hélène Verhaeghe, Bart Bogaerts, and Tias Guns. Exploiting symmetries in MUS computation. In AAAI-25, Sponsored by the Association for the Advancement of Artificial Intelligence, pages 11122-11130. AAAI Press, 2025. URL: https://doi.org/10.1609/AAAI.V39I11.33209.
  13. Javier Castro, Daniel Gómez, and Juan Tejada. Polynomial calculation of the Shapley value based on sampling. Comput. Oper. Res., 36(5):1726-1730, 2009. URL: https://doi.org/10.1016/J.COR.2008.04.004.
  14. Georgios Chalkiadakis, Edith Elkind, and Michael J. Wooldridge. Computational Aspects of Cooperative Game Theory. Synthesis Lectures on Artificial Intelligence and Machine Learning. Morgan & Claypool Publishers, 2012. URL: https://doi.org/10.2200/S00355ED1V01Y201107AIM016.
  15. 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.
  16. John Deegan and Edward W Packel. A new index of power for simple n-person games. International Journal of Game Theory, 7:113-123, 1978. Google Scholar
  17. Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003, pages 502-518, 2003. URL: https://doi.org/10.1007/978-3-540-24605-3_37.
  18. Dan S Felsenthal and Moshé Machover. The measurement of voting power. Edward Elgar Publishing, 1998. Google Scholar
  19. Johannes Klaus Fichte and Markus Hecher. The model counting competitions 2021-2023. CoRR, abs/2504.13842, 2025. URL: https://doi.org/10.48550/arXiv.2504.13842.
  20. Éric Grégoire, Yacine Izza, and Jean-Marie Lagniez. Boosting MCSes enumeration. In Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, pages 1309-1315, 2018. URL: https://doi.org/10.24963/ijcai.2018/182.
  21. Éric Grégoire, Jean-Marie Lagniez, and Bertrand Mazure. An experimentally efficient method for (MSS, CoMSS) partitioning. In Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, pages 2666-2673, 2014. URL: https://doi.org/10.1609/AAAI.V28I1.9118.
  22. Fred Hemery, Christophe Lecoutre, Lakhdar Sais, and Frédéric Boussemart. Extracting MUCs from constraint networks. In ECAI 2006, 17th European Conference on Artificial Intelligence, Proceedings, volume 141 of Frontiers in Artificial Intelligence and Applications, pages 113-117. IOS Press, 2006. URL: https://ebooks.iospress.nl/volumearticle/2661.
  23. Anthony Hunter and Sébastien Konieczny. Shapley inconsistency values. In Proceedings, Tenth International Conference on Principles of Knowledge Representation and Reasoning, pages 249-259. AAAI Press, 2006. URL: http://www.aaai.org/Library/KR/2006/kr06-027.php.
  24. Anthony Hunter and Sébastien Konieczny. On the measure of conflicts: Shapley inconsistency values. Artif. Intell., 174(14):1007-1026, 2010. URL: https://doi.org/10.1016/J.ARTINT.2010.06.001.
  25. Alexey Ignatiev, António Morgado, and João Marques-Silva. Pysat: A python toolkit for prototyping with SAT oracles. In Theory and Applications of Satisfiability Testing - SAT 2018 - 21st International Conference, Proceedings, volume 10929 of Lecture Notes in Computer Science, pages 428-437. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94144-8_26.
  26. Alexey Ignatiev, Alessandro Previti, Mark H. Liffiton, and João Marques-Silva. Smallest MUS extraction with minimal hitting set dualization. In Principles and Practice of Constraint Programming - 21st International Conference, CP 2015, Proceedings, pages 173-182, 2015. URL: https://doi.org/10.1007/978-3-319-23219-5_13.
  27. Alexey Ignatiev, Zi Li Tan, and Christos Karamanos. Towards universally accessible SAT technology. In 27th International Conference on Theory and Applications of Satisfiability Testing, SAT 2024, volume 305 of LIPIcs, pages 16:1-16:11. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.SAT.2024.16.
  28. Ulrich Junker. QUICKXPLAIN: preferred explanations and relaxations for over-constrained problems. In Proceedings of the Nineteenth National Conference on Artificial Intelligence, pages 167-172. AAAI Press / The MIT Press, 2004. URL: http://www.aaai.org/Library/AAAI/2004/aaai04-027.php.
  29. Hans Kleine Büning. Classes of propositional UMU formulas and their extensions to minimal unsatisfiable formulas. Theor. Comput. Sci., 998:114538, 2024. URL: https://doi.org/10.1016/J.TCS.2024.114538.
  30. Sébastien Konieczny and Stéphanie Roussel. A reasoning platform based on the MI shapley inconsistency value. In Symbolic and Quantitative Approaches to Reasoning with Uncertainty - 12th European Conference, ECSQARU 2013, Lecture Notes in Computer Science, pages 315-327. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39091-3_27.
  31. Isabelle Kuhlmann, Andreas Niskanen, and Matti Järvisalo. Computing MUS-based inconsistency measures. In Logics in Artificial Intelligence - 18th European Conference, JELIA 2023, Proceedings, volume 14281 of Lecture Notes in Computer Science, pages 745-755. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-43619-2_50.
  32. Mark H. Liffiton and Ammar Malik. Enumerating infeasibility: Finding multiple muses quickly. In Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, 10th International Conference, CPAIOR 2013. Proceedings, volume 7874 of Lecture Notes in Computer Science, pages 160-175. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-38171-3_11.
  33. Mark H. Liffiton, Alessandro Previti, Ammar Malik, and João Marques-Silva. Fast, flexible MUS enumeration. Constraints An Int. J., 21(2):223-250, 2016. URL: https://doi.org/10.1007/s10601-015-9183-0.
  34. Mark H. Liffiton and Karem A. Sakallah. Searching for autarkies to trim unsatisfiable clause sets. In Theory and Applications of Satisfiability Testing - SAT 2008, 11th International Conference. Proceedings, pages 182-195, 2008. URL: https://doi.org/10.1007/978-3-540-79719-7_18.
  35. Mark H. Liffiton and Karem A. Sakallah. Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reasoning, 40(1):1-33, 2008. URL: https://doi.org/10.1007/s10817-007-9084-z.
  36. Scott M. Lundberg and Su-In Lee. A unified approach to interpreting model predictions. In Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, pages 4765-4774, 2017. URL: https://proceedings.neurips.cc/paper/2017/hash/8a20a8621978632d76c43dfd28b67767-Abstract.html.
  37. Joao Marques-Silva, Federico Heras, Mikolás Janota, Alessandro Previti, and Anton Belov. On computing minimal correction subsets. In IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, pages 615-622, 2013. URL: https://www.ijcai.org/Proceedings/13/Papers/098.pdf.
  38. João Marques-Silva, Mikolás Janota, and Anton Belov. Minimal sets over monotone predicates in boolean formulae. In Computer Aided Verification - 25th International Conference, CAV 2013. Proceedings, volume 8044 of Lecture Notes in Computer Science, pages 592-607. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39799-8_39.
  39. João Marques-Silva, Mikolás Janota, and Carlos Mencía. Minimal sets on propositional formulae. Problems and reductions. Artif. Intell., 252:22-50, 2017. URL: https://doi.org/10.1016/J.ARTINT.2017.07.005.
  40. João Marques-Silva and Carlos Mencía. Reasoning about inconsistent formulas. In Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI 2020, pages 4899-4906, 2020. URL: https://doi.org/10.24963/IJCAI.2020/682.
  41. João Marques-Silva, Carlos Mencía, and Raúl Mencía. The sets of power. CoRR, abs/2410.07867, 2024. URL: https://doi.org/10.48550/arXiv.2410.07867.
  42. Pablo Martínez-Naredo, Raúl Mencía, João Marques-Silva, and Carlos Mencía. Explanations of unsatisfiability beyond minimal subsets. In Logics in Artificial Intelligence - 19th European Conference, JELIA 2025, Proceedings, Part II, volume 16094 of Lecture Notes in Computer Science, pages 141-158. Springer, 2025. URL: https://doi.org/10.1007/978-3-032-04590-4_10.
  43. Carlos Mencía, Alexey Ignatiev, Alessandro Previti, and João Marques-Silva. MCS extraction with sublinear oracle queries. In Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Proceedings, pages 342-360, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_21.
  44. Carlos Mencía, Oliver Kullmann, Alexey Ignatiev, and João Marques-Silva. On computing the union of MUSes. In Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Proceedings, volume 11628 of Lecture Notes in Computer Science, pages 211-221. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-24258-9_15.
  45. Carlos Mencía, Alessandro Previti, and João Marques-Silva. Literal-based MCS extraction. In Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, pages 1973-1979. AAAI Press, 2015. URL: http://ijcai.org/Abstract/15/280.
  46. Raúl Mencía, Carlos Mencía, and João Marques-Silva. Efficient reasoning about infeasible one machine sequencing. In Proceedings of the Thirty-Third International Conference on Automated Planning and Scheduling, ICAPS 2023, pages 268-276. AAAI Press, 2023. URL: https://doi.org/10.1609/ICAPS.V33I1.27204.
  47. Alexander Nadel. Boosting minimal unsatisfiable core extraction. In Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, pages 221-229, 2010. URL: http://ieeexplore.ieee.org/document/5770953/.
  48. Nina Narodytska, Nikolaj Bjørner, Maria-Cristina Marinescu, and Mooly Sagiv. Core-guided minimal correction set and core enumeration. In Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, pages 1353-1361, 2018. URL: https://doi.org/10.24963/ijcai.2018/188.
  49. Alexander Nöhrer, Armin Biere, and Alexander Egyed. Managing SAT inconsistencies with HUMUS. In Sixth International Workshop on Variability Modelling of Software-Intensive Systems. Proceedings, pages 83-91, 2012. URL: https://doi.org/10.1145/2110147.2110157.
  50. Alessandro Previti and João Marques-Silva. Partial MUS enumeration. In Proceedings of the Twenty-Seventh AAAI Conference on Artificial Intelligence, pages 818-825. AAAI Press, 2013. URL: https://doi.org/10.1609/AAAI.V27I1.8657.
  51. Alessandro Previti, Carlos Mencía, Matti Järvisalo, and João Marques-Silva. Premise set caching for enumerating minimal correction subsets. In Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), pages 6633-6640, 2018. URL: https://doi.org/10.1609/AAAI.V32I1.12213.
  52. Raymond Reiter. A theory of diagnosis from first principles. Artif. Intell., 32(1):57-95, 1987. URL: https://doi.org/10.1016/0004-3702(87)90062-2.
  53. Lloyd S Shapley and Martin Shubik. A method for evaluating the distribution of power in a committee system. American political science review, 48(3):787-792, 1954. Google Scholar
  54. Mate Soos, Stephan Gocht, and Kuldeep S. Meel. Tinted, detached, and lazy CNF-XOR solving and its applications to counting and sampling. In Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings, Part I, volume 12224 of Lecture Notes in Computer Science, pages 463-484. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-53288-8_22.
  55. Mate Soos and Kuldeep S. Meel. BIRD: engineering an efficient CNF-XOR SAT solver and its applications to approximate model counting. In The Thirty-Third AAAI Conference on Artificial Intelligence, AAAI 2019, pages 1592-1599. AAAI Press, 2019. URL: https://doi.org/10.1609/AAAI.V33I01.33011592.
  56. Mate Soos and Kuldeep S. Meel. Engineering an efficient probabilistic exact model counter. In Ruzica Piskac and Zvonimir Rakamaric, editors, Computer Aided Verification - 37th International Conference, CAV 2025, Proceedings, Part III, volume 15933 of Lecture Notes in Computer Science, pages 72-91. Springer, 2025. URL: https://doi.org/10.1007/978-3-031-98682-6_5.
  57. Leslie G. Valiant. The complexity of enumeration and reliability problems. SIAM J. Comput., 8(3):410-421, 1979. URL: https://doi.org/10.1137/0208032.
  58. Stylianos Loukas Vasileiou, Borong Xu, and William Yeoh. A logic-based framework for explainable agent scheduling problems. In ECAI 2023 - 26th European Conference on Artificial Intelligence, Frontiers in Artificial Intelligence and Applications, pages 2402-2410. IOS Press, 2023. URL: https://doi.org/10.3233/FAIA230542.
  59. Jinqiang Yu, Graham Farr, Alexey Ignatiev, and Peter J. Stuckey. Anytime approximate formal feature attribution. In 27th International Conference on Theory and Applications of Satisfiability Testing, SAT 2024, volume 305 of LIPIcs, pages 30:1-30:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.SAT.2024.30.
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