A Hybrid Method for Probabilistic Satisfiability

Abstract

Determining satisfiability of sets of formula formulated in a Nilsson style probabilistic logic (PSAT) by reduction to a system of linear (in)equations has been extensively studied, esp. in the propositional setting. The basic technique for coping with the potentially exponentially large (in terms of the formulae) linear system is column generation, which has been successful (in various forms) in solving problems of around 1000 formulae. Common to existing techniques is that the column generation model explicitly encodes all classical, i.e., non-probabilistic, knowledge. In this paper we introduce a straightforward but new hybrid method for PSAT that makes use of a classical solver in the column generation process. The benefits of this technique are twofold: first, we can, in practice, accommodate inputs with significantly larger classical parts, and thus which are overall larger, and second, we can accommodate inputs with supra-propositional classical parts, such as propositionally complete description logics. We validate our approach with an extensive series of experiments which show that our technique is competitive with traditional non-hybrid approaches in spite of scaling the expressivity of the classical part to the description logic $\mathcal{SROIQ}$.