What is PrSAT?
PrSAT 3.0 is an open source web-based tool for testing the satisfiability of arbitrary sets of statements in the probability calculus. Given a set of probabilistic constraints, PrSAT determines whether they can be simultaneously satisfied and, iff so, returns a probability model witnessing satisfiability.
The new version of PrSAT requires only a web browser — no installation or software licenses required. Just enter your constraints and click "Find Model".
Try It Now
Launch PrSAT in your browser. Enter probabilistic constraints (in plain text), set options, and search for models.
The app page includes detailed syntax documentation and a short video demo of the software.
Syntax & Usage
Entering Constraints
Enter probabilistic constraints using a simple ASCII text syntax. Each constraint is displayed with live mathematical rendering so you can verify the parsed expression.
| Syntax | Meaning | Example |
|---|---|---|
Pr(X) |
Unconditional probability | Pr(H) = 1/2 |
Pr(X | Y) |
Conditional probability | Pr(H | E) > Pr(H) |
X & Y |
Conjunction (and) | Pr(A & B) = 0 |
X \/ Y or X v Y |
Disjunction (or) | Pr(A \/ B) = 1 or Pr(A v B) = 1 |
~X or -X |
Negation (not) | Pr(~E) = Pr(E) |
X -> Y |
Conditional (if-then) | Pr(P -> Q) >= Pr(Q | P) |
Comparison operators: =, !=, <,
>, <=, >=
Arithmetic operators: +, -, *, /
Options
- Regular: Check this to search for a regular (i.e., strictly positive) probability model
- Timeout: Set a maximum time limit for the solver (hours, minutes, seconds)
Understanding Results
After clicking Find Model, PrSAT returns one of two possible results:
Unsatisfiable
If the constraints are unsatisfiable, you'll see "Constraints are UNSATisfiable!" along with a truth table showing the atomic states and the algebraic form of your constraints. This means no probability distribution can simultaneously satisfy all the algebraic constraints implied by your query.
Satisfiable
If the constraints are satisfiable, you'll see "Constraints are SATisfiable!" with a probability model displayed as a truth table. The Assignment column shows the probability assigned to each atomic state. Assignments may include exact algebraic numbers with radicals when rational solutions don't exist. This is a decision procedure, so its solutions are exact (no numerical calculations or approximations are involved here).
Model Evaluation
When a satisfying model is found, the Evaluate model panel lets you compute
the value of any probability expression under that model. For example, enter a probabilistic
expression like Pr(B \/ C) to see its value, or enter a claim like
Pr(X | Y) >= Pr(X) to compute its truth-value on the model. You can also load
expressions from a file or use batch input for multiple evaluations.
Import/Export
- Save to File: Export your constraints for later use
- Copy to Clipboard: Copy constraints in a format ready to paste elsewhere
- Load From File: Import previously saved constraints or evaluation expressions
- Save translated constraints: Export the algebraic form of your constraints
- Save SMTLIB input: Export constraints in SMT-LIB format for use with external SMT solvers
Source Code
The PrSAT 3.0 source code is available on GitHub:
Reference
For the theory behind PrSAT and applications in formal epistemology, see:
Branden Fitelson. A Decision Procedure for Probability Calculus with Applications. Review of Symbolic Logic. PDF available here.
Contact
For bug reports, feature requests, or questions, please contact Branden Fitelson.
Mathematica Version of PrSAT 3.0
A fully revamped and upgraded version 3.0 of the PrSAT Mathematica package (now with external SMT-solver support) is available (from Branden Fitelson) upon request.