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. I also wrote a short blog entry about this.

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!

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 Validity Check Same as Validity Check, but with expanded input language adding ∀ (written as #) and ∃ (written as ?). Uses DepQBF.
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 |).

Loading and Processing WebAssembly of Limboole...

Input

Output

Errors