Merging the local and global approaches to probabilistic satisfiability

The probabilistic satisfiability problem is to verify the consistency of a set of probability values or intervals for logical propositions. The (tight) probabilistic entailment problem is to find best bounds on the probability of an additional proposition. The local approach to these problems applies rules on small sets of logical sentences and probabilities to tighten given probability intervals. The global approach uses linear programming to find best bounds. We show that merging these approaches is profitable to both: local solutions can be used to find global solutions more quickly through stabilized column generation, and global solutions can be used to confirm or refute the optimality of the local solutions found. As a result, best bounds are found, together with their step-by-step justification.