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与勇敢语义）。对于一大类逻辑理论，在这些语义下判断查询答案是否成立在数据复杂度上属于（共）NP完全问题。当不存在优先关系或该关系具有特殊结构时，针对基于修复的语义已有基于SAT的求解方法。本文首次引入了针对一般优先关系的帕累托最优与完备最优修复的SAT编码，并提出了多种运用现有及新型编码的方法，通过利用SAT求解器的不同推理模式来计算基于（最优）修复的语义下的答案。我们实现的全面实验评估比较了：（i）采用基于不同类型修复的语义的影响，以及（ii）针对相同语义的替代方法的相对性能。