Probabilistic Satisfiability: Logic-based Algorithms and Phase Transition
Marcelo Finger and Glauber de Bona
In this paper, we study algorithms for probabilistic satisfiability (PSAT), an NP-complete problem, and their empiric complexity distribution. We define a PSAT normal form, based on which we propose two logic-based algorithms: a reduction of normal form PSAT instances to SAT, and a linear-algebraic algorithm with a logic-based column generation strategy. We conclude that both algorithms present a phase transition behaviour and that the latter has a much better performance. We discuss the role of logic and the normal form in the detection of the phase transition.