From 654912f5020d4f42dff8e2f5a17bdfa5d37befa5 Mon Sep 17 00:00:00 2001 From: Gerard Basler Date: Sun, 26 Oct 2014 23:41:28 +0100 Subject: Avoid the `CNF budget exceeded` exception via smarter translation into CNF. The exhaustivity checks in the pattern matcher build a propositional formula that must be converted into conjunctive normal form (CNF) in order to be amenable to the following DPLL decision procedure. However, the simple conversion into CNF via negation normal form and Shannon expansion that was used has exponential worst-case complexity and thus even simple problems could become untractable. A better approach is to use a transformation into an _equisatisfiable_ CNF-formula (by generating auxiliary variables) that runs with linear complexity. The commonly known Tseitin transformation uses bi- implication. I have choosen for an enhancement: the Plaisted transformation which uses implication only, thus the resulting CNF formula has (on average) only half of the clauses of a Tseitin transformation. The Plaisted transformation uses the polarities of sub-expressions to figure out which part of the bi-implication can be omitted. However, if all sub-expressions have positive polarity (e.g., after transformation into negation normal form) then the conversion is rather simple and the pseudo-normalization via NNF increases chances only one side of the bi-implication is needed. I implemented only optimizations that had a substantial effect on formula size: - formula simplification, extraction of multi argument operands - if a formula is already in CNF then the Tseitin/Plaisted transformation is omitted - Plaisted via NNF - omitted: (sharing of sub-formulas is also not implemented) - omitted: (clause subsumption) --- src/intellij/test/files/neg/virtpatmat_exhaust_big.flags | 1 + 1 file changed, 1 insertion(+) create mode 100644 src/intellij/test/files/neg/virtpatmat_exhaust_big.flags (limited to 'src/intellij/test/files/neg/virtpatmat_exhaust_big.flags') diff --git a/src/intellij/test/files/neg/virtpatmat_exhaust_big.flags b/src/intellij/test/files/neg/virtpatmat_exhaust_big.flags new file mode 100644 index 0000000000..b5a8748652 --- /dev/null +++ b/src/intellij/test/files/neg/virtpatmat_exhaust_big.flags @@ -0,0 +1 @@ +-Xfatal-warnings -unchecked -- cgit v1.2.3