Add unit tests for Tseitin CNF conversion.

We compare the results using the Tseitin transformation with the results of a
conversion via expansion of the formula (using distributive laws), e.g.,

```
             +-------+
             |Formula|
             +---+---+
                 |
     +-----------+-----------+
     |                       |
     v                       v
+---------+              +-------+
|Expansion|              |Tseitin|
+----+----+              +---+---+
     |        +-----+        |
     +------->| =?= |<-------+
              +-----+
```

both methods should deliver the same results (i.e., models).

Author: gbasler