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.

翻译：我们研究了在优先知识库上进行容错查询回答的实用算法，该知识库由逻辑理论、事实集合以及冲突事实之间的优先关系组成。我们基于两种最优修复概念（帕累托修复和完全修复）考虑了三种众所周知的语义（AR、IAR和勇敢语义）。对于一大类逻辑理论，在这些语义下判定查询答案是否成立在数据复杂度上是(co)NP完全的，并且针对无优先关系或关系具有特殊结构的情况，已设计出基于SAT的修复语义程序。本文首次针对一般优先关系引入了帕累托最优修复和完全最优修复的SAT编码，并提出了利用SAT求解器的不同推理模式来运用现有及新编码以计算基于（最优）修复语义的答案的若干方法。我们实现的综合实验评估比较了：(i) 采用基于不同类型修复的语义所带来的影响，以及 (ii) 相同语义下替代程序的相对性能。