SAT Solving

The logic platform supports logical satisfiability solving. To make use of it you should:

• Specify some propositions. They may take any grammar-valid format. We recommend you don't make use of True or False literals, because SAT solvers typically treat them as variables. Instead, use some of your grey matter to eliminate the literals yourself.
• Specify that you want to solve SAT:

cmd solve satisfiability

• Specify which solver to use.

config solver="<solver-slug>"

• Run!

Supported solvers

To make use of a solver, you should get its binary, name it appropriately, and place it in the app's working directory.

Solver	Binary	slug
Sat4j	sat4j.jar	sat4j

Result

After running, the resulting text file will start with either Satisfiable or Unsatisfiable depending on the result. In the former case, one solution will follow in the form terminal=value per line. E.g.:

Satisfiable
A=True
B=False
C=True