Abschlussarbeit

The study of belief change addresses the question of how a rational agent should adjust its beliefs, when facing new, potentially contradictory, information. Following a belief change operation, there are usually two kinds of checks that are of interest: model and inference checks. The former are concerned with determining whether the new belief state holds for particular interpretations, whereas the latter investigate whether it entails a particular propositional formula. To avoid arbitrariness and ensure reproducibility, several belief change operators have been proposed in the literature. While these operators have been studied extensively on theoretical grounds, there are only few academic works on practical implementations. One reason is likely the high computational complexity of many operators with regards to inference and model checks, which are usually located on the first or second level of the polynomial hierarchy. We address this shortcoming by implementing and evaluating a compilation-based belief change application that makes use of Boolean Satisfiability Solving (SAT), Answer Set Programming (ASP), and Integer Linear Programming (ILP). The application supports inference and model checks for four distinct distance-based revision and contraction operators. Given a belief change instance, it firstly determines the minimum distance via partial Maximum Satisfiability Solving (partial MaxSAT), ASP, or ILP optimization encodings and subsequently compiles the new belief state that results from the change operation into a SAT, ASP, or ILP encoding. The resulting encoding can then be lever- aged for inference and model checks on the new belief state, turning these checks into feasibility problems. In an extensive evaluation we compare the usage of the different encodings in terms of runtime. The results show that for the determination of the minimum distance, our partial MaxSAT-based optimization encoding schemes perform best for each of the four supported change operators. With regards to inference and model checks we obtain that both the SAT- and the ASP-based encodings outperform their ILP counterparts. Moreover, the ASP-based encodings outperform the SAT-based ones in inference checks, whereas with regards to model checks the SAT-based encodings per- form best. A comparison with a naive baseline implementation further concludes that our compilation-based approach is clearly superior to the naive approach, irrespec- tive of the used encoding schemes. Our results demonstrate that compilation-based approaches to belief change constitute a viable and promising way of implementing inference and model checks and therefore deserve more research attention within the academic field of belief change.