SI-6582 Use Tseitin's algorithm for CNF.

This resolves the `AnalysisBudgetException` problem for big pattern matches.

Initial experiments indicate that the problem is even simpler than initially
thought: all formulae I got from the exhaustiveness check could be transformed
directly into CNF. Thus the framework introduced here might be overkill
and a much simpler implementation could work as well.

For Scala 2.11 I'd suggest to replace the DPLL procedure with Sat4j.