PropSat uses syntax adapted from PDDL.

PropSat onLine lets you define a domain and a set of constraintsrun PropPlan with a 60 second timeou. You can paste in your own examples, or use, or edit, the examples provided.

A variety of different domains is available. When you select a new domain, its description will appear above.

For each problem, PropSat prints statistics: BDD size; number of satisfying states; number of boolean variables, and gives a satisfying valuation.