## 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