Probabilistic Satisfiability


BibTeX reference

A review is made of models and algorithms for probabilistic satisfiability and its extensions. The basic probabilistic satisfiability problem, in decision form, is: given m logical sentences and their probabilities of being true to determine if these probabilities are consistent. In optimization form, given an additional logical sentence, it is to find best lower and upper bounds on the probability of this last sentence to be true. Extensions involve probability intervals, conditional probabilities (or probabilities of conditional events), probabilities of negations, conjunctions or disjunctions of conditional events, and probabilities of iterated conditional. Analytical solution methods include Boole's algebraic approach, and enumeration of vertices and extreme rays of the dual polytope of the probabilistic satisfiability problem. They lead to automated theorem proving in probability theory. Numerical solution methods rely upon the column generation technique of linear programming and nonlinear 0-1 programming to solve the choice of entering column auxiliary problem. Heuristic algorithms of simulated annealing or Tabu search type are also useful for this last task. Decomposition proves to be helpful for large instances, i.e., with several hundred variables. Restoring consistency with minimal changes, a form of nonmonotonic reasoning can be done by linear or mixed-integer programming. Alternate but close solution concepts, models, and algorithms are discussed: finding the maximum entropy solution, justifying bounds by anytime deduction, incidence calculus, Bayesian logic which combines probabilistic satisfiability with Bayesian networks, probabilistic assumption-based truth maintenance systems and probabilistic satisfiability with belief functions. Finally, applications are briefly examined and potential of the probabilistic satisfiability approach evaluated.

, 69 pages

Research Axes

Research applications