Realization of c-Inference as a SAT Problem - Christoph Beierle; Martin von Berg; Arthur Sanin (Proceedings of the International Florida Artificial Intelligence Research Society Conference)
Semantically based on Spohn’s ranking functions, c-representations are special ranking models obtained by assigning individual integer impacts to the conditionals in a knowledge base R and by defining the rank of each possible world as the sum of the impacts of falsified conditionals. c-Inference is the inference relation taking all c-representations of a given knowledge base R into account. In this paper, we show that c-inference can be realized as a boolean satisfiability problem (SAT), which in turn allows c-inference to be implemented by a SAT solver. We provide a stepwise transformation of the characterization of c-inference as as constraint satisfaction problem (CSP), into a solvable-equivalent SAT problem. We present a SAT-based implementation of c-inference using the SMT solver Z3, demonstrating the feasibility of the approach. Up to now, there has been only one previous implementation of c-inference; this previous implementation utilizes a Prolog-based CSP solver. First evaluation results demonstrate that our SAT-based implementation outperforms the previous CSP-based implementation, providing a promising basis for further developing this approach.