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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Explanations of Unsatisfiability Beyond Minimal Subsets

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

摘要

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.