Probabilistic satisfiability (PSAT) is an NP-complete problem that requires the joint application of deductive and probabilistic reasoning. It consists of an assignment of probabilities to a set of propositional formulas, and its solution consists of a decision on whether this assignment is consistent. The original formulation of PSAT is attributed to George Boole (1854). The problem has since been independently rediscovered several times, until it was presented to the Computer Science and Artificial Intelligence community by Nilsson (1986) and was shown to be an NP-complete problem, even for cases where the corresponding classical satisfiability is known to be in PTIME. It was later claimed to be "a very hard problem" by Nilsson himself (1993).
Recent advances in the theory of PSAT have shown that it displays a "Phase Transition Behavior", which means that there are PSAT problems of considerable size which can be efficiently solved. Two algortithms were proposed that display exactly that kind of behavior: a reduction of PSAT to SAT, and a mix of linear programming and SAT using Column Generation Techniques. This project presents implementations for these two techniques.