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.

该研究探讨了一种能容忍不一致性的查询回答算法，依据逻辑理论、事实集和冲突事实间的优先关系构建知识库，并提出了一种新的基于 SAT 求解器的编码模式，能够应用在不同推理模式下实现查询回答。