Classical Generalized Probabilistic Satisfiability
Abstract
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.
Cite
Text
Caleiro et al. "Classical Generalized Probabilistic Satisfiability." International Joint Conference on Artificial Intelligence, 2017. doi:10.24963/IJCAI.2017/126Markdown
[Caleiro et al. "Classical Generalized Probabilistic Satisfiability." International Joint Conference on Artificial Intelligence, 2017.](https://mlanthology.org/ijcai/2017/caleiro2017ijcai-classical/) doi:10.24963/IJCAI.2017/126BibTeX
@inproceedings{caleiro2017ijcai-classical,
title = {{Classical Generalized Probabilistic Satisfiability}},
author = {Caleiro, Carlos and Casal, Filipe and Mordido, Andreia},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2017},
pages = {908-914},
doi = {10.24963/IJCAI.2017/126},
url = {https://mlanthology.org/ijcai/2017/caleiro2017ijcai-classical/}
}