Explanations of Unsatisfiability Beyond Minimal Subsets
摘要
The analysis of unsatisfiable propositional formulas is crucial across a wide range of application domains. While minimal unsatisfiable subsets (MUSes) are standard explanations in this setting, gaining a clear understanding of the underlying reasons for unsatisfiability is often difficult when relying solely on them. As an alternative form of explanation, this paper investigates the practical application of power indices to measure the importance of clauses and variables in the inconsistency of a formula. Power indices were originally proposed in game theory to quantify the relative importance of voters in weighted voting games, and their use has been proposed in a variety of areas, including explainability and as measures of inconsistency for knowledge bases. To enable practical computation, this paper introduces a SAT-based approach to approximate the Shapley-Shubik power index. Our approach leverages a probabilistic algorithm with theoretical guarantees and incorporates optimization techniques to significantly improve performance. Experimental results demonstrate the suitability of the proposed algorithm.