You may either scroll through the examples or enter your own boolean or propositional formulas in the ENTER YOUR FORMULA box. Although PBL has many other features, the online interface allows you convert the formula to cnf (exponentially sized) or negation normal form. The syntax was made to be robust and intuitive. See the examples to get an idea. The exact language spec can be seen here. These are only two features of PBL. Other features include:

- Parsing files dimacs files
- Parsing files custom language (like in examples)
- Convert to cnf, nne, or polynomial sized cnf
- Output dimacs file
- Propagate variable values

Parsing is accomplished using the PLY library

This library makes a good base to write various SAT algorithms including DPLL and BDDs.

This package implements algorithms from the Bradley and Manna book "The Calculus of Computation"

Currently there is no simplification algorithms implemented. Email me if you are interested in contributing :)

These tools are mostly for educational purposes! There are probably better choices for large, robust projects.

PyBool can handle parse DIMACS files, but also a more expressive in-house language.
A short summary of the language is as follows:

**Variables :** Can be named anything alpha numeric, except for keywords. Literal variables must
be declared in a Var_Order statement.

**Var_Order :** declares variables and order of variables (important for BDDs) used as such:

*Var_Order : {variable name}*

You can have multi Var_Order statements, just don't declare variables multiple times.

Variables storing sub-formulas should not be in Var_Order statements

**Constants :** Represents logical True or False in expressions

*1 - True
0 - False*

variable now refers to expression and can be used later on.

Where the base cases are Variables or constants as expressions

- () : parentheses
- ! | ~ : negation
- & : conjunction (and)
- | : disjunction (or)
- => | -> : implication
- XOR : exclusive-or
- <=> | <-> : iff

They are listed in order of precedence, and => associates from right to left.

**Main_Exp :** The only expression considered by the BDD. simply

* Main_Expr : Expression*

**Comments :** denoted with #

Please view the examples on the main BDD page for better understanding.