Scaling up Nonmonotonic c-Inference via Partial MaxSAT Problems

Ranking functions, also called ordinal conditional functions (OCF), provide a semantics for conditionals by assigning a degree of implausibility to the underlying possible worlds. The entailment relation c-inference takes all c-representations, which are special ranking functions, into account, and exhibits excellent properties put forward for nonmonotonic reasoning. However, for realizing c-inference, showing the unsolvability of a complex constraint satisfaction problem (CSP) is required, involving in particular satisfaction conditions affecting all possible worlds. All previous implementations of c-inference are severely limited by this requirement, making inferences from conditional belief bases involving more than about 25 signature elements, and thus \(2^{25}\) possible worlds, practically infeasible. In this paper, we present an approach for reducing the size of the CSP underlying c-inference significantly by using partial maximum satisfiability problems (PMaxSAT) and the power of current PMaxSAT solvers. In particular, we introduce the dual notion of minimum satisfiability problems for simplifying the minimum expressions in the CSP. We prove the soundness of our CSP optimization and develop an implementation for it. An evaluation demonstrates that it outperforms all previous implementations and that it, while still having to cope with the exponentially increasing number of possible worlds, scales up c-inference to a new dimension, allowing for c-inference from belief bases with up to 100 signature elements and thus involving \(2^{100}\) possible worlds.