pith. sign in

arxiv: 2202.07980 · v5 · submitted 2022-02-16 · 💻 cs.LO · cs.AI· cs.DB

Querying Inconsistent Prioritized Data with ORBITS: Algorithms, Implementation, and Experiments

Meghyn Bienvenu , Camille Bourgaux This is my paper

Pith reviewed 2026-05-24 12:07 UTC · model grok-4.3

classification 💻 cs.LO cs.AIcs.DB
keywords inconsistency-tolerant query answeringprioritized knowledge basesoptimal repairsPareto optimalitySAT encodingsrepair-based semanticsAR semanticsIAR semantics
0
0 comments X

The pith

SAT encodings for general priority relations enable query answering under Pareto and completion optimal repair semantics.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops the first SAT-based procedures that compute answers to queries over inconsistent knowledge bases equipped with arbitrary priority relations among conflicting facts. It encodes the notions of Pareto-optimal and completion-optimal repairs so that standard SAT solvers can identify repairs and evaluate answers under the AR, IAR and brave semantics. Experiments then measure how the choice of repair notion and the choice of encoding affect both the answers returned and the runtime cost.

Core claim

The authors introduce SAT encodings that correctly capture Pareto-optimal and completion-optimal repairs for arbitrary priority relations, then combine these new encodings with previously known ones to obtain decision procedures for inconsistency-tolerant query answering; the procedures exploit different reasoning modes of SAT solvers and are shown to be practical through systematic implementation and benchmarking.

What carries the argument

SAT encodings of Pareto-optimal and completion-optimal repairs that directly encode the dominance relation induced by a general priority relation on facts.

If this is right

  • Answers under AR, IAR and brave semantics can be computed for general priorities without restricting the priority relation to a total order or other special form.
  • The same encodings support both decision and enumeration modes of SAT solvers, yielding multiple practical algorithms for each semantics.
  • Comparative experiments become possible that isolate the effect of repair optimality notion from the effect of the underlying logical theory.
  • Existing SAT technology can be reused directly rather than requiring new dedicated solvers for prioritized repair semantics.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The approach may scale to larger data sets if modern SAT preprocessing or incremental solving techniques are applied to the generated formulas.
  • The encodings could be adapted to other repair-based semantics or to weighted priorities by extending the dominance clauses.
  • Real-world applications that already maintain priority information among data sources could adopt these procedures without first converting priorities into a total order.

Load-bearing premise

The proposed SAT formulas correctly represent the optimal-repair semantics for any given priority relation.

What would settle it

A concrete priority relation, set of facts, and query for which an off-the-shelf SAT solver using the new encoding returns an answer that differs from the answer obtained by exhaustive enumeration of all repairs.

Figures

Figures reproduced from arXiv: 2202.07980 by Camille Bourgaux, Meghyn Bienvenu.

Figure 1
Figure 1. Figure 1: Subformulas of ϕC-max(F), which is used to ensure it is possible to extend the selected subset of F to a completion-optimal repair. Non-binary conflicts We briefly discuss how to modify the preceding formulas to handle non-binary conflicts. The most essential difference is that instead of choosing a single contradicting fact, we may need to choose a conjunction of facts, and use additional variables to ref… view at source ↗
Figure 2
Figure 2. Figure 2: Single- and multi-answer encodings for X-AR (top) and X-brave (middle) semantics, single-answer encodings for X-IAR (bottom). [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Best running times (in milliseconds) for each semantics [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Time (in milliseconds, log. scale) to filter query answers under X-AR semantics (X [PITH_FULL_IMAGE:figures/full_fig_p009_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Food Inspection dataset: database schema, constraints and queries. In the queries, [PITH_FULL_IMAGE:figures/full_fig_p028_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Physicians dataset: database schema, constraints and queries. In the queries, [PITH_FULL_IMAGE:figures/full_fig_p029_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Best running times for each semantics and priority relation on Food Inspection dataset in milliseconds. [PITH_FULL_IMAGE:figures/full_fig_p090_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Best running times for each semantics and priority relation on Physicians dataset in milliseconds. [PITH_FULL_IMAGE:figures/full_fig_p092_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Best running times for each semantics and priority relation on [PITH_FULL_IMAGE:figures/full_fig_p094_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Query answers filtering time (in milliseconds) w.r.t. percentage of facts in conflicts for [PITH_FULL_IMAGE:figures/full_fig_p102_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Query answers filtering time (in milliseconds) w.r.t. data size for [PITH_FULL_IMAGE:figures/full_fig_p103_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Query answers filtering time (in milliseconds) w.r.t. percentage of facts in conflicts for [PITH_FULL_IMAGE:figures/full_fig_p104_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: Query answers filtering time (in milliseconds) w.r.t. data size for [PITH_FULL_IMAGE:figures/full_fig_p105_13.png] view at source ↗
Figure 14
Figure 14. Figure 14: Query answers filtering time (in milliseconds) w.r.t. percentage of facts in conflicts for [PITH_FULL_IMAGE:figures/full_fig_p106_14.png] view at source ↗
Figure 15
Figure 15. Figure 15: Query answers filtering time (in milliseconds) w.r.t. data size for [PITH_FULL_IMAGE:figures/full_fig_p107_15.png] view at source ↗
read the original abstract

We investigate practical algorithms for inconsistency-tolerant query answering over prioritized knowledge bases, which consist of a logical theory, a set of facts, and a priority relation between conflicting facts. We consider three well-known semantics (AR, IAR and brave) based upon two notions of optimal repairs (Pareto and completion). Deciding whether a query answer holds under these semantics is (co)NP-complete in data complexity for a large class of logical theories, and SAT-based procedures have been devised for repair-based semantics when there is no priority relation, or the relation has a special structure. The present paper introduces the first SAT encodings for Pareto- and completion-optimal repairs w.r.t. general priority relations and proposes several ways of employing existing and new encodings to compute answers under (optimal) repair-based semantics, by exploiting different reasoning modes of SAT solvers. The comprehensive experimental evaluation of our implementation compares both (i) the impact of adopting semantics based on different kinds of repairs, and (ii) the relative performances of alternative procedures for the same semantics.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper introduces the first SAT encodings for Pareto- and completion-optimal repairs with respect to general (arbitrary) priority relations over inconsistent prioritized knowledge bases. It proposes multiple ways to combine these new encodings with existing ones to compute answers under the AR, IAR, and brave repair-based semantics by exploiting different SAT-solver reasoning modes, presents an implementation (ORBITS), and reports a comprehensive experimental comparison of both the impact of the different semantics and the relative performance of the alternative procedures.

Significance. If the encodings are faithful, the work supplies the first practical, general-purpose SAT-based method for prioritized repair semantics beyond the total-order or empty-priority cases treated in prior literature. The experimental evaluation of semantics trade-offs and solver-mode variants would then constitute a useful empirical contribution for inconsistency-tolerant query answering.

major comments (1)
  1. [Abstract] Abstract: the central claim that the new SAT encodings correctly capture Pareto and completion optimality for general (non-total, non-strict) priority relations is presented without a formal correctness argument or machine-checked verification. Because the (co)NP-completeness result only establishes hardness and does not guarantee that the particular reduction preserves optimality, this unverified step is load-bearing for every subsequent claim about optimal-repair semantics and for the experimental results.
minor comments (2)
  1. The description of how the new encodings are combined with existing ones to realize the three semantics could be clarified with a small table or pseudocode listing the solver calls for each combination.
  2. A few sentences on the concrete priority-relation representation used in the implementation would help readers reproduce the experiments.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the thorough review and for highlighting the importance of formally establishing the correctness of the new SAT encodings. We address the major comment below and will revise the manuscript to strengthen this aspect.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the central claim that the new SAT encodings correctly capture Pareto and completion optimality for general (non-total, non-strict) priority relations is presented without a formal correctness argument or machine-checked verification. Because the (co)NP-completeness result only establishes hardness and does not guarantee that the particular reduction preserves optimality, this unverified step is load-bearing for every subsequent claim about optimal-repair semantics and for the experimental results.

    Authors: We agree that the (co)NP-completeness result only shows hardness and does not by itself verify that our specific encodings preserve optimality. A formal correctness argument is indeed required to support all claims about the encodings and the experimental results that rely on them. In the revised manuscript we will add a dedicated section (or appendix) containing the full formal proofs that the SAT encodings correctly capture Pareto-optimal and completion-optimal repairs for arbitrary priority relations. We will also make explicit how the encodings relate to the decision problem. revision: yes

Circularity Check

0 steps flagged

No circularity: new SAT encodings presented as independent technical contribution

full rationale

The paper's central contribution is the introduction of novel SAT encodings for Pareto- and completion-optimal repairs under general priority relations. These encodings are defined directly in the text as new artifacts, not derived from or equivalent to prior fitted parameters, self-definitions, or load-bearing self-citations. Established (co)NP-completeness results and existing SAT procedures are cited as background but do not reduce the new encodings to tautologies or renamings. Experimental evaluation provides an external benchmark. No steps match the enumerated circularity patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on standard complexity results for the decision problems and the assumption that SAT solvers can handle the encodings in practice; no free parameters, new entities, or ad-hoc axioms beyond domain assumptions are introduced.

axioms (1)
  • domain assumption Deciding whether a query answer holds under the semantics is (co)NP-complete in data complexity for a large class of logical theories.
    Stated directly in the abstract as background for the problem.

pith-pipeline@v0.9.0 · 5714 in / 999 out tokens · 20333 ms · 2026-05-24T12:07:38.020940+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

12 extracted references · 12 canonical work pages

  1. [1]

    (⇒) Assume that there exists a satisfying assignment ν of ΨX-AR(PotAns) such that ν(x⃗ a) = true, and let Sν = {α | ν(xα) = true}

    where F′ 1 = facts(⋀ ⃗ a∈PotAns ϕ′ ¬q(⃗ a)) and F′ 2 = F′ 1 ∪ facts(ϕX-max(F′ 1)). (⇒) Assume that there exists a satisfying assignment ν of ΨX-AR(PotAns) such that ν(x⃗ a) = true, and let Sν = {α | ν(xα) = true}. Since ν satisfiesϕX-max(F′

    work page

  2. [2]

    Since ν satisfiesϕ′ ¬q(⃗ a) and ν(x⃗ a) = true, then ν must satisfy ϕ¬q(⃗ a)

    ∧ ϕcons(F′ 2), by Lemma 5, 6, or 7, Sν can be extended to a X-optimal repair R of K≻. Since ν satisfiesϕ′ ¬q(⃗ a) and ν(x⃗ a) = true, then ν must satisfy ϕ¬q(⃗ a). It follows by Lemma 3 that (R, T ) ̸|= q(⃗ a). Hence K≻ ̸|=X AR q(⃗ a). (⇐) Assume that K≻ ̸|=X AR q(⃗ a): There exists R ∈ XRep(K≻) such that (R, T ) ̸|= q(⃗ a). • As in the proof of Propositio...

    work page

  3. [4]

    • Let us extend ν by setting ν(x⃗ a) = true and ν(x⃗ a′) = false for every ⃗ a′ ∈ PotAns such that ⃗ a̸= ⃗ a′

    and satisfiesϕ¬q(⃗ a). • Let us extend ν by setting ν(x⃗ a) = true and ν(x⃗ a′) = false for every ⃗ a′ ∈ PotAns such that ⃗ a̸= ⃗ a′. • Since ν satisfiesϕ¬q(⃗ a), it also satisfiesϕ′ ¬q(⃗ a). • Let ⃗ a′ ∈ PotAns, ⃗ a′ ̸= ⃗ a. Assume for a contradiction that ν does not satisfy ϕ′ ¬q(⃗ a′): There is a cause C of q(⃗ a′) such that ν does not satisfy ϕ′ ¬C(x⃗ a′...

    work page

  4. [5]

    (⇒) Assume that K≻ |=X brave q(⃗ a): There exists R ∈ XRep(K≻) such that (R, T ) |= q(⃗ a)

    where F′ 1 = facts(⋀ ⃗ a∈PotAns ϕ′ q(⃗ a)) and F′ 2 = F′ 1 ∪ facts(ϕX-max(F′ 1)). (⇒) Assume that K≻ |=X brave q(⃗ a): There exists R ∈ XRep(K≻) such that (R, T ) |= q(⃗ a)

    work page

  5. [6]

    As in the proof of Proposition 4, we can find a valuation ν of the variables of ϕX-max(F′

    work page

  6. [8]

    Let us extend ν by setting ν(x⃗ a) = true, and for every ⃗ a′ ∈ PotAns such that ⃗ a̸= ⃗ a′, ν(x⃗ a′) = false and ν(xC) = false for every C ∈ Causes(q(⃗ a′), K) \ Causes(q(⃗ a), K) (i.e., the value of ν(xC) has not been fixed in step (1))

    work page

  7. [9]

    Since ν satisfiesϕq(⃗ a) and ν(x⃗ a) = true, it also satisfiesϕ′ q(⃗ a)

    work page

  8. [10]

    It follows that ν satisfiesΨX-brave(PotAns)

    For every ⃗ a′ ∈ PotAns such that ⃗ a′ ̸= ⃗ a, ν satisfies ϕ′ q(⃗ a′) because (i) ν(x⃗ a′) = false and ¬x⃗ a′ is a disjunct of the first clause, and (ii) every other clause of ϕ′ q(⃗ a′) either contains some ¬xC with C ∈ Causes(q(⃗ a′), K) \ Causes(q(⃗ a), K) and ν(xC) = false, or is a clause shared with ϕq(⃗ a) and thus is satisfied byν. It follows that ν s...

    work page

  9. [11]

    Since ν satisfiesϕ′ q(⃗ a) and ν(x⃗ a) = true, then ν must satisfy ϕq(⃗ a)

    ∧ ϕcons(F′ 2), by Lemma 5, 6, or 7, Sν can be extended to a X-optimal repair R of K≻. Since ν satisfiesϕ′ q(⃗ a) and ν(x⃗ a) = true, then ν must satisfy ϕq(⃗ a). It follows by Lemma 4 that (R, T ) |= q(⃗ a). Hence K≻ |=X brave q(⃗ a). Proposition 7. K≻ |=X IAR q(⃗ a) if and only if ΦX-IAR(q(⃗ a)) is unsatisfiable. Proof. Recall that ΦX-IAR(q(⃗ a)) = ⋀ C∈Cau...

    work page

  10. [12]

    Since ν satisfiesϕ′ ¬{α} and ν(yα) = true, then ν must satisfy ϕ¬{α}

    ∧ ϕcons(F′ 2), by Lemma 5, 6, or 7,Sν can be extended to a X-optimal repairR of K≻. Since ν satisfiesϕ′ ¬{α} and ν(yα) = true, then ν must satisfy ϕ¬{α}. It follows by Lemma 1 that α /∈ R. Hence K≻ ̸|=X IAR α. (⇐) Assume that K≻ ̸|=X AR α: There exists R ∈ XRep(K≻) such that α /∈ R. • As in the proof of Proposition 10, we can find a valuation ν of the varia...

    work page

  11. [13]

    that satisfies ϕX-max(F′

    work page

  12. [14]

    • Let us extend ν by setting ν(yα) = true and ν(yα′) = false for every α′ ∈ Rel such that α ̸= α′

    and satisfiesϕ¬{α}. • Let us extend ν by setting ν(yα) = true and ν(yα′) = false for every α′ ∈ Rel such that α ̸= α′. • Since ν satisfiesϕ¬{α}, it also satisfiesϕ′ ¬{α}(yα). • Let α′ ∈ Rel, α′ ̸= α. Assume for a contradiction that ν does not satisfy ϕ′ ¬{α′}(yα′). In neg1 case, there is a contradiction because ϕ′ ¬{α′}(yα′) is a single clause that contains ...

    work page 2016