Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Comparison of SAT-based and ASP-based Algorithms for Inconsistency Measurement

Isabelle Kuhlmann, Anna Gessler, Vivien Laszlo, Matthias Thimm

TL;DR

This work advances inconsistency measurement in propositional knowledge bases by providing both SAT-based and ASP-based algorithms for six measures tied to the first level of the polynomial hierarchy. It systematically derives encodings for contension, forgetting-based, hitting-set, and three distance-based measures, and compares their performance across five diverse datasets, using CaDiCaL and Clingo. Across extensive experiments, both approaches outperform naive baselines, with ASP-based methods generally achieving superior runtime performance and scalability. The study also examines search strategies, MaxSAT variants, and core-guided optimization, offering practical guidance on preprocessing and method selection for real-world inconsistency assessment. The results underscore the value of ASP in this domain while highlighting remaining scalability challenges for very large knowledge bases and encouraging future exploration of alternative solving paradigms and preprocessing techniques.

Abstract

We present algorithms based on satisfiability problem (SAT) solving, as well as answer set programming (ASP), for solving the problem of determining inconsistency degrees in propositional knowledge bases. We consider six different inconsistency measures whose respective decision problems lie on the first level of the polynomial hierarchy. Namely, these are the contension inconsistency measure, the forgetting-based inconsistency measure, the hitting set inconsistency measure, the max-distance inconsistency measure, the sum-distance inconsistency measure, and the hit-distance inconsistency measure. In an extensive experimental analysis, we compare the SAT-based and ASP-based approaches with each other, as well as with a set of naive baseline algorithms. Our results demonstrate that overall, both the SAT-based and the ASP-based approaches clearly outperform the naive baseline methods in terms of runtime. The results further show that the proposed ASP-based approaches perform superior to the SAT-based ones with regard to all six inconsistency measures considered in this work. Moreover, we conduct additional experiments to explain the aforementioned results in greater detail.

Comparison of SAT-based and ASP-based Algorithms for Inconsistency Measurement

TL;DR

This work advances inconsistency measurement in propositional knowledge bases by providing both SAT-based and ASP-based algorithms for six measures tied to the first level of the polynomial hierarchy. It systematically derives encodings for contension, forgetting-based, hitting-set, and three distance-based measures, and compares their performance across five diverse datasets, using CaDiCaL and Clingo. Across extensive experiments, both approaches outperform naive baselines, with ASP-based methods generally achieving superior runtime performance and scalability. The study also examines search strategies, MaxSAT variants, and core-guided optimization, offering practical guidance on preprocessing and method selection for real-world inconsistency assessment. The results underscore the value of ASP in this domain while highlighting remaining scalability challenges for very large knowledge bases and encouraging future exploration of alternative solving paradigms and preprocessing techniques.

Abstract

We present algorithms based on satisfiability problem (SAT) solving, as well as answer set programming (ASP), for solving the problem of determining inconsistency degrees in propositional knowledge bases. We consider six different inconsistency measures whose respective decision problems lie on the first level of the polynomial hierarchy. Namely, these are the contension inconsistency measure, the forgetting-based inconsistency measure, the hitting set inconsistency measure, the max-distance inconsistency measure, the sum-distance inconsistency measure, and the hit-distance inconsistency measure. In an extensive experimental analysis, we compare the SAT-based and ASP-based approaches with each other, as well as with a set of naive baseline algorithms. Our results demonstrate that overall, both the SAT-based and the ASP-based approaches clearly outperform the naive baseline methods in terms of runtime. The results further show that the proposed ASP-based approaches perform superior to the SAT-based ones with regard to all six inconsistency measures considered in this work. Moreover, we conduct additional experiments to explain the aforementioned results in greater detail.
Paper Structure (60 sections, 41 theorems, 149 equations, 34 figures, 8 tables)

This paper contains 60 sections, 41 theorems, 149 equations, 34 figures, 8 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. The Contension Inconsistency Measure
  4. The Forgetting-Based Inconsistency Measure
  5. The Hitting Set Inconsistency Measure
  6. Distance-Based Inconsistency Measures
  7. SAT-Based Algorithms for Selected Inconsistency Measures
  8. Satisfiability Solving
  9. Scheme for SAT-Based Algorithms for Inconsistency Measures
  10. The Contension Inconsistency Measure
  11. The Forgetting-Based Inconsistency Measure
  12. The Hitting Set Inconsistency Measure
  13. The Max-Distance Inconsistency Measure
  14. The Sum-Distance Inconsistency Measure
  15. The Hit-Distance Inconsistency Measure
  16. ...and 45 more sections

Key Result

Theorem 1

For a given value $u$, the encoding $S_{\mathrm{c}}(\mathcal{K},u)$ is satisfiable if and only if $\mathcal{I}{_{\mathrm{c}}}(\mathcal{K}) \leq u$.

Figures (34)

  • Figure 1: Overview of the average runtime composition of the ASP-based and SAT-based approaches for $\mathcal{I}{_{\mathrm{c}}}$ wrt. the SRS data set.
  • Figure 2: Overview of the average runtime composition of the ASP-based and SAT-based approaches for $\mathcal{I}_{\mathrm{f}}$ wrt. the SRS data set.
  • Figure 3: Runtime comparison of the ASP-based, SAT-based, and naive approaches on the SRS data set. Timeout: $10$ minutes.
  • Figure 4: Runtime comparison of the ASP-based, SAT-based, and naive approaches on the ML data set. Timeout: $10$ minutes.
  • Figure 5: Runtime comparison of the ASP-based, SAT-based, and naive approaches on the ARG data set. Timeout: $10$ minutes.
  • ...and 29 more figures

Theorems & Definitions (106)

  • Definition 1
  • Definition 2
  • Example 1
  • Example 2
  • Definition 3: Grant & Hunter ( ? )
  • Example 3
  • Definition 4
  • Example 4
  • Definition 5
  • Example 5
  • ...and 96 more