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 quantifierfree 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