PrSAT 2.5

A
Decision Procedure for Probability Calculus

Branden Fitelson (Northeastern University)

…with invaluable
assistance from Jason Alexander (London School of Economics) and Ben Blum

PrSAT 2.5 should be compatible with *Mathematica*
version 12. Please send any bugs, comments, *etc.* to branden@fitelson.org. [Package
last updated 02/20/21]

A paper
about PrSAT and some of
its applications (which has appeared in *RSL*) is available at

What is PrSAT?

PrSAT is a user-friendly, *Mathematica* function
for testing the satisfiability of (arbitrary) sets of statements in the
probability calculus.

Version 2.5 of PrSAT should be compatible with *Mathematica*
12 (as well as versions 6–11).

This *Mathematica* 12 notebook, which briefly explains the functions in
the PrSAT 2.5 package, is included in the archive
mentioned in the installation instructions.

Installation
instructions

**1**.
Download the PrSAT zip archive from the following location, and
unzip it somewhere on your local machine:

http://fitelson.org/PrSAT/PrSAT.zip

**2.**
Copy PrSAT.m to the
directory returned when you evaluate the following cell in *Mathematica* on your machine.

**$UserBaseDirectory<>"/Applications"**

**3**. Open PrSAT.nb in *Mathematica* (version 6 or later –
now including version 12).

Initialization
Cell (loading PrSAT)

If the above installation was successful, evaluating
the cell (in PrSAT.nb)
initialization cell should evaluate without any errors. And, none of the cells below should generate
errors, *etc*. [If you obtain
errors here, then try to re-run the notebook on a fresk *Mathematica*
kernel session.]

**<<PrSAT`
**

Using PrSAT

The PrSAT function itself takes as its main argument a
set of statements (equations, inequations, and/or inequalities) in the
probability calculus.

If that set
is satisfiable, then (in principle) PrSAT will return a probability model which makes all
the statements in the set true. If the
set is not satisfiable, then (in principle) PrSAT will reutrn the empty set {}.

PrSAT accepts upper or lower case letters
(subscripts are also allowed) as propositional variables. PrSAT recognizes "∧", "∨", and "¬" for the logical connectives
"and", "or", and "not", respectively.

PrSAT uses the notation "Pr[X]" for "the unconditional probability
of X", and the notation "Pr[X|Y]" for "the conditional probability of
X, given Y."

Here is a
simple PrSAT example, involving two jointly satisfiable
probabilistic equations:

M1 =
PrSAT[

{

Pr[X∧Y]==1/6,

Pr[X|Y]==1/4

}

]

When it
finds a model (as in this first example), PrSAT's default output is not a terribly readable
representation of a probability model.

A
“stochastic truth-table” (to use the language of the* RSL* paper mentioned
above) formatting function **STT** is included.

Here's an
example of its output on the above PrSAT data structure:

STT[M1]

The**
****𝕒 _{i}** are the probabilities assigned by the
discovered model to the

Suppose you
wanted to find a *positive* (or *regular*) probability distribution
satisfying the above constraints. The
optional argument Probabilities makes this possible. The default value of Probabilities is "NotRegular", which means that zeros are allowed in
the probability functions PrSAT reports in its model output. But, by adding "Probabilities ➝ Regular" as an optional argument to PrSAT, only strictly positive probability models are
returned. Applied to the last example,
this yields:

M2 =
PrSAT[

{

Pr[X∧Y]==1/6,

Pr[X|Y]==1/4

},

Probabilities➝Regular

]

STT[M2]

One can
easily verify properties of a PrSAT generated model, using the function EvaluateProbability:

EvaluateProbability[{Pr[X∧Y]==1/6,Pr[X|Y]==1/4},M2]

{True,True}

Indeed, one
can use EvaluateProbability to compute the value of any probability
expression (or list thereof) on a PrSAT generated model:

EvaluateProbability[{Pr[X∧Y],Pr[X|Y]},M2]

{1/6,1/4}

The
complexity of the decision procedure used by PrSAT grows (doubly) exponentially in the number of
propositions involved in the set of statements. For sets involving three or more events, the
decision procedure in PrSAT can consume significant computational
resources. For this reason, a *random
search* feature has been included in PrSAT. Note
that the random search feature may not find a model even if one exists, and it
can return different probability models for the same input. By default, PrSAT first tries several random searches. If these random searches fail, then the
problem is fed to the decision procedure (exhasutive search) underlying PrSAT. Here's
an example of an unsatisfiable set of formulas, in which the random search
phase fails (as does the exhaustive search!):

PrSAT[

{

Pr[H | ¬(H∧A)] > Pr[H]

}

]

PrSAT::srchfail: Search phase failed;
attempting FindInstance

{}

We can turn
off the random search functionality, using the BypassSearch option (which, by default, is turned off).

PrSAT[

{

Pr[H | ¬(H∧A)] > Pr[H]

},

BypassSearch➝True

]

{}

Here's a
non-trivial example of PrSAT at work.
Every introductory probability text explains that it is possible for a
set of three propositions to be *pairwise* independent, but *not*
independent *simpliciter*. That is,
the following set of four statements is jointly satisfiable:

IND={

Pr[X∧Y∧Z]!=Pr[X]Pr[Y]Pr[Z],

Pr[X∧Y]==Pr[X]Pr[Y],

Pr[X∧Z]==Pr[X]Pr[Z],

Pr[Y∧Z]==Pr[Y]Pr[Z]

};

Using PrSAT, we can find a model that proves this. The naive way to do this is to simply run PrSAT on the set IND with no equational side-constraints. The
random search algorthm will find a model pretty quickly (given a sufficient
number of SearchAttempts—the
default number of SearchAttempts is 3, which may not be sufficient for this
example).

M3=PrSAT[IND,Probabilities➝Regular,SearchAttempts➝6]

** STT[M3]**

STT[M3]//N

This
problem takes *much* longer for PrSAT to solve if it does not use random
search. However, if we add just a single
additional equational constraint to the problem, then even the decision
procedure can solve this one in reasonable time (and it finds a much more
pleasant looking model — which is typically the case for the decision procedure
as opposed to the random search algorithm):

CONS1={Pr[X]==1/3};

M4=PrSAT[IND ⋃ CONS1,BypassSearch➝True,Probabilities➝Regular]

STT[M4]

Of course,
if IND ⋃ {Pr[X]==1/3} is satisfiable, then so is IND alone.
It's just much easier to find models
when you know you only have to look at ones in which ** Pr[X]==1/3** (since there are *a lot *fewer of
these!). However, one must be careful *not*
to infer that a set S is *un*satisfiable on the grounds that S ⋃ C is unsatisfiable, for some set of equational
side-constraints C. *That* would be a fallacy.

For
instance, we could easily add side constraints to the problem above that would
render the problem unsatisfiable (even though the original set of constraints
is satisfiable). For instance,

CONS2={Pr[X]==1/2,Pr[Y]==1/2,Pr[X ∧ Y]==1/8};

PrSAT[IND ⋃ CONS2,BypassSearch➝True]

{}

PrSAT also contains some "scratchpad"
functionality, which allows the user to work directly with PrSAT’s underlying algebraic representations of
probabilistic statements. The main
sratchpad function is AlgebraicForm.

Let's
examine the previous example using AlgebraicForm.

INDa=AlgebraicForm[IND,{X,Y,Z}]

This is PrSAT’s
underlying algebraic representation
of the system **IND**. We can
now work directly with the algebraic representation. For instance, we can solve the equational part
of INDa, as follows:

Simplify[Solve[Drop[INDa,1]]]