Classical Generalized Probabilistic Satisfiability

Classical Generalized Probabilistic Satisfiability

Carlos Caleiro, Filipe Casal, Andreia Mordido

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence
Main track. Pages 908-914. https://doi.org/10.24963/ijcai.2017/126

We analyze a classical generalized probabilistic satisfiability problem (GGenPSAT) which consists in deciding the satisfiability of Boolean combinations of linear inequalities involving probabilities of classical propositional formulas. GGenPSAT coincides precisely with the satisfiability problem of the probabilistic logic of Fagin et al. and was proved to be NP-complete. Here, we present a polynomial reduction of GGenPSAT to SMT over the quantifier-free theory of linear integer and real arithmetic. Capitalizing on this translation, we implement and test a solver for the GGenPSAT problem. As previously observed for many other NP-complete problems, we are able to detect a phase transition behavior for GGenPSAT.
Keywords:
Knowledge Representation, Reasoning, and Logic: Automated Reasoning and Theorem Proving
Uncertainty in AI: Exact Probabilistic Inference
Constraints and Satisfiability: Solvers and Tools
Constraints and Satisfiability: Satisfiability