Boosting Distance-Based Revision Using SAT Encodings

Belief revision has been studied for more than 30 years, and the theoretical properties of the belief revision operators are now well-known. Contrastingly, there are almost no practical applications of these operators. One of the reasons is the computational complexity of the corresponding inference problem, which is typically NP-hard and coNP-hard. Especially, existing implementations of belief revision operators are capable to solve toy instances, but are still unable to cope with real-size problem instances. However, the improvements achieved by SAT solvers for the past few years have been very impressive and they allow to tackle the solving of instances of inference problems located beyond N P. In this paper we describe and evaluate SAT encodings for a large family of distance-based belief revision operators. The results obtained pave the way for the practical use of belief revision operators in large-scale applications.