Realization of c-Inference as a SAT Problem

摘要

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.