Limboole on the Go!
Uses Limboole (MIT licensed), PicoSAT (MIT licensed), and DepQBF (GPLv3 licensed) to parse an easy SAT and QBF DSL (instead of relying on DIMACS). Compiled using Emscripten, Source Code and Modifications are available on GitHub. Created by Max Heisinger. Support on GitHub.
How-To
Usage
Write formulas into the left text input, press the button and get results on the right side. The formula can also be analyzed using Shift + Enter. Every time a formula is analyzed, the link in your URL-bar (awesome-bar, location-bar or some other name) updates and can be copied. This link can be opened at other browsers and directly executes the given formula. Give it a try! Additionally, Drag & Drop support works by dragging and dropping an input file onto the input area on the left hand side. Browser support is required and indicated by the grey box next to the input heading if available.
Modes
| Validity Check | Check if the formula is valid, i.e. all possible combinations of variables satisfy the formula. |
| Satisfiability Check | Check if there is any assignment of variables so that the formula is satisfied. |
| QBF Satisfiability Check | Same as Satisfiability Check, but with expanded input language adding ∀ (written as #) and ∃ (written as ?). Uses DepQBF. |
Syntax
The input format has the following syntax in EBNF ( [ ... ] means optional, { ... } means repeated arbitrary many times).
expr ::= iff
iff ::= implies { '<->' implies }
implies ::= or [ '->' or | '<-' or ]
or ::= and { ('|' | '/') and }
and ::= not { '&' not }
not ::= basic | '!' not
basic ::= var | '(' expr ')'var is a string over letters, digits and the following characters: - _ . [ ] $ @.
The last character of var should be different from -.
Compared to classical Limboole, the syntax is improved for mobile devices: The / symbol also counts as OR (same as |).