SI-6582 Use Tseitin transformation to convert propositional formulae into CNF. #2724
Conversation
|
SPURIOUS ABORT? -- PLS REBUILD/pr-checkin-per-commit@6668e60769267e3c49b345a355f602375d9c61c9 |
|
(kitty-note-to-self: ignore 20855896) |
Opening a ticket at https://issues.scala-lang.org/ would raise the visibility of this suggestion. Then comes classifying that ticket at "improvement" or "performance bug". |
|
Weird, do we have heavy load on the build servers? @gbasler I can't comment on the technical aspects, but let me know if you need help with the processes around contributing (this is your first PR on scala/scala, right?). |
|
Thanks, @gbasler! Looks like one of the tests in test/files/pos/*.scala is causing the algorithm to loop? You can reproduce locally with |
…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. For Scala 2.11 I'd suggest to replace the DPLL procedure with Sat4j.
|
retest this please |
|
@adriaanm Thanks, I saw that the tests were not finishing but thought it was a problem with my setup (since it was one of the very last ones that failed). All test should pass now. |
|
@magarciaEPFL I've created a ticket here: https://issues.scala-lang.org/browse/SI-7663 @soc This is indeed my first PR, I might come back to your offer. I've just seen that there is a corresponding ticket here: https://issues.scala-lang.org/browse/SI-6582. |
|
Cool! (Btw, the build bot rebuilds automatically as you push new commits to the PR) |
|
So sorry this has been slipping -- I've been buried with other stuff. |
|
Don't worry ;-) |
|
Perfect! |
|
@adriaanm: ping |
|
This is outstanding work! I'm very sorry about the delay in reviewing, so I'll address my only review comment myself: I'd like to chop this up in a few smaller commits. Working on that today. |
|
One performance question: this seems to undo the optimization added in f539781 -- is that necessary/safe now? |
|
@adriaanm The CNF conversion is not composable anymore (since each translation would need to know the auxiliary variables of the others and the mapping from subformulas to literals), thus the (CNF(...) + CNF(...) ...) approach doesn't work anymore. Even better, the simplification is not needed because 1) the conversion can't blow the stack anymore, 2) the formula is simplified as a whole before the conversion. |
|
Ok, makes sense -- I'll merge the last two commits of the rework I submitted. |
This resolves the
AnalysisBudgetExceptionproblem 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.
For Scala 2.11 I'd suggest to replace the DPLL procedure with Sat4j. See separate branch.
Review by @adriaanm