Representing Nonmonotonic Inference Based on c-Representations as an SMT Problem.

As a semantics for conditional knowledge bases, ranking functions order possible worlds by mapping them to a degree of plausibility. c-Representations are special ranking functions that are 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 these impacts of falsified conditionals. c-Inference is the nonmonotonic inference relation taking all c-representations of a given knowledge base R into account. In this paper, we show how c-inference can be realized as a satisfiability modulo theories problem (SMT), which allows an implementation by an appropriate SMT solver. We develop a transformation of the constraint satisfaction problem characterizing c-inference into a solvable-equivalent SMT problem, prove its correctness, and illustrate it by a running example. Furthermore, we provide a corresponding implementation using the SMT solver Z3, demonstrating the feasibility of the approach as well as the superiority in comparison to former implementations.