Toto je webové rozhraní pro SAT solver (MiniSat zkompilovaný do JavaScriptu odsud).
Vstupní formát DIMACS je standardní formát pro zápis formulí v konjunktivní normální formě (CNF). Pro připomenutí, CNF je formule ve tvaru konjunkce disjunkcí (tzv. klauzulí), ve které se negace objevují pouze před proměnnými. DIMACS soubor vždy začíná hlavičkou, která udává počet proměnných a počet klauzulí ve formuli:
p cnf <pocet-promennych> <pocet-klauzuli>
Dále následuje samotná formule. Jako názvy proměnných jsou použity celá nenulová čísla v rozsahu vymezeném hlavičkou. Negace před proměnnou je zapsána pomocí symbolu mínus -. Jednotlivé klauzule jsou pak zapisovány po řádcích ukončených znakem 0 (0 tedy nelze použít jako proměnnou). Komentáře jsou řádky začínající symbolem c.
Například, formuli (𝑥₁) ∧ (¬𝑥₂ ∨ ¬𝑥₃) ∧ (𝑥₁ ∨ 𝑥₂ ∨ 𝑥₃) lze zapsat jako:
p cnf 3 3
1 0
-2 -3 0
1 2 3 0