2026-07-21T11:25:48Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:26339 2026-07-16T10:50:12Z ddc:004 open_access

Shapley-Shubik Attribution from Minimal Subsets (Short Paper) Martínez-Naredo, Pablo Mencía, Raúl Marques-Silva, Joao Mencía, Carlos Unsatisfiability Shapley-Shubik index MUSes and MCSes 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Pablo Martínez-Naredo and Raúl Mencía and Joao Marques-Silva and Carlos Mencía 2026 Is Part Of LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2026.33 urn:nbn:de:0030-drops-263398 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.33 eng https://creativecommons.org/licenses/by/4.0/legalcode