gbasler/scala — pull request #1 by gbasler (2013-06-30 11:10:18+00:00)
Title: Switch to SAT4j instead of old fashioned DPLL solver. Use Tseitin transf...

...ormation 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 (more code than you think it is, despite its name... Sat4J is already based on MiniSat so it's a matter of copy-paste Java-to-Scala and downsizing).
- use CafeSat (Solver is not reentrant and even worse it seems to fail sometimes for no reason, I even got nondeterministic errors)
- stick to original DPLL implementation (I'll give this a try on a separate branch)