Switch to SAT4j instead of old fashioned DPLL solver. Use Tseitin transformation to convert propositional formulae into 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 by formula simplification, neither expansion not Tseitin transformation where needed.
Thus the framework introduced here might be overkill and a much simpler implementation could work as well.

How do we get the SAT solver in the complier? I see the following approaches:
- add dependency to Sat4J.jar
- port MiniSat to Scala (really not much code and Sat4J is already based on MiniSat so it's a matter of copy-paste Java-to-Scala and downsizing).
- check out CafeSat (might be immature though)
- stick to original DPLL implementation (the clauses I got had mostly 2 literals so an additional unit propagation step might speed up things enough)