Syntax

Use either a conventional formula syntax like

(a -> b) & a & -b

or a dimacs version of the clause normal form syntax like

-1 2
1
-2

which is a conjunction of disjunction lines with numbers standing for variables: the last example means simply (-x1 v x2) & x1 & -x2

For conventional formula syntax:

• negation symbols are -, ~
• conjunction symbols are &, and
• disjunction symbols are |, v, V, or
• xor symbols are +, xor
• implication symbols are ->, =>
• equivalence symbols are <->, <=>

There is no operator precedence; all operators are bound from left:
a & b v c & d v e is read as ((((a & b) v c) & d) v e)

For dimacs you may use or skip the initial comment lines starting with c, the special p line and the final 0 symbols at the end of each disjunct.
We allow the trailing 0-s only at the end of a line.

I.e. you may use the full dimacs version like

c comment
p cnf 2 3
-1 2 0
1 0
-2 0

or just

-1 2
1
-2

hide syntax