Research map / Learning theory and algorithms / Combinatorial and search optimization
Computing the Why-Provenance for Datalog Queries via SAT Solvers
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Shows how off-the-shelf SAT solvers (Glucose) can compute why-provenance for Datalog queries relative to unambiguous proof trees, enumerating explanations incrementally via blocking clauses.
Problem
Why-provenance for Datalog queries is computationally expensive and can yield counterintuitive explanations from ambiguous proof trees, and existing approaches compute the whole explanation set at once.
Approach
Restricts attention to unambiguous proof trees, encodes the existence of a compressed DAG over the downward closure as a Boolean formula (with vertex-elimination acyclicity encoding), and enumerates why-provenance members one at a time with a SAT solver using blocking clauses.
Key results
- Building the downward closure and SAT formula takes on the order of seconds for most scenarios; for Andersen with 3.4M-6.8M facts it takes between half a minute and a minute.
- Once the formula is built, most delays between successive why-provenance explanations are below 1 millisecond, with medians in microseconds.
- The SAT-based approach consistently outperforms the rule-based approach of Elhalawati et al.; on Galen, the rule-based method times out (5 min) in most cases, with 41 of 100 runs timing out on the largest database.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use the SAT-based approach with unambiguous proof trees instead of the rule-based approach | Why-provenance computation · Galen | end-to-end runtime | Helped |
| Use the SAT-based approach with unambiguous proof trees instead of the rule-based approach | Why-provenance computation · Doctors-i | end-to-end runtime | Helped |
| Incrementally enumerate explanations using the SAT-based approach | Why-provenance computation · Experimental scenarios | delay per explanation | Helped |
| Use the SAT-based approach for incremental explanation enumeration | Why-provenance computation · Experimental scenarios | explanation computation speed | Helped |
Surprising findings
- Computing why-provenance restricted to unambiguous proof trees is faster in practice than the rule-based approach computing the full why-provenance, despite the extra unambiguity check.
Limitations
- Runtime is dominated by computing the downward closure, which is the main bottleneck.
- Approach is only evaluated for pure Datalog queries; extension to more expressive languages such as ontology-mediated queries is left open.
- Comparison with the rule-based baseline is restricted to Galen and Doctors scenarios because only those rewritings were available.
Experimental setup
Datasets: Doctors Galen Andersen CSDA TClosure bitcoin facebook httpd postgresql linux
Benchmarks: TClosure Galen Andersen CSDA Doctors-i
Metrics: runtime (s) delay between explanations (ms) timeouts
Baselines: rule-based why-provenance (Elhalawati, Krötzsch, and Mennicke 2022)
Builds on: why-provenance (Buneman et al. 2001) downward closure (Elhalawati et al. 2022) vertex elimination acyclicity encoding (Rankooh and Rintanen 2022) non-recursive and minimal-depth proof trees (Bourgaux et al. 2022)
Closest papers by meaning
- Explaining Inconsistency-Tolerant Query Answering over Description Logic Knowledge Bases (AAAI 2016 · similarity 0.86)
- Preferred Explanations for Ontology-Mediated Queries under Existential Rules (AAAI 2021 · similarity 0.85)
- Explanations for Inconsistency-Tolerant Query Answering under Existential Rules (AAAI 2020 · similarity 0.85)
- Querying Attributed DL-Lite Ontologies Using Provenance Semirings (AAAI 2019 · similarity 0.85)
- Epistemic Disjunctive Datalog for Querying Knowledge Bases (AAAI 2023 · similarity 0.85)
- Optimised Storage for Datalog Reasoning (AAAI 2024 · similarity 0.83)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.