Simplification of Boolean Affine FormulasPaul Feautrier |
Boolean Affine Formulas, in which affine inequalities are combined by boolean connectives, are ubiquitous in computer science: static analysis, code and hardware generation, symbolic model checking and many other techniques use them as a compact representation of large or infinite sets. Common algorithms tend to generate large and highly redundant formulas, hence the necessity of a simplifier for keeping the overall complexity under control. Simplification is a difficult problem, at least as hard as SMT solving, with a worst case complexity exponential in the number of affine inequalities. This paper proposes a new method, based on path cutting in Ordered Binary Decision Diagrams, which is able to take advantage of any regularity in the subject formula to speed up simplification. The method has been implemented and was tested on benchmarks from several application domains.
Boolean affine formulas are simplified by first constructing an Ordered Binary Decision Diagram, then finding and cutting its unfeasible paths. See [4] for details. In the worst case, the method is exponential in the number of affine atoms, but in many cases is able to exploit regularities in the subjet formula to improve its running time.
Small benchmarks were used to debug the implementation. Example dillig.dat is from [3]. Example scholl2.dat is from [6].
Quasts benchmarks come from a hardware synthesis application [1] and from a code generation application [2].
name | size | before | after | time |
Small | ||||
g1g2.dat | 3 | 2 | 1 | 0.012 |
g2l3.dat | 5 | 3 | 2 | 0.015 |
split-centered.dat | 4 | 3 | 2 | 0.030 |
dillig.dat | 40 | 5 | 2 | 0.10 |
scholl2.dat | 7 | 4 | 3 | 0.018 |
Quasts | ||||
matmul-3.quast2.dat | 10 | 4 | 4 | 0.039 |
poly-1.quast1.dat | 142 | 9 | 3 | 0.14 |
poly-1.quast2.dat | 62 | 8 | 2 | 0.062 |
poly-1.quast3.dat | 131 | 8 | 4 | 0.16 |
poly-1.quast4.dat | 33 | 6 | 3 | 0.051 |
poly-3.quast1.dat | 18 | 4 | 1 | 0.023 |
poly-5.quast1.dat | 8 | 4 | 2 | 0.012 |
poly-6.quast1.dat | 11 | 4 | 2 | 0.033 |
choles-Q2.dat | 2918 | 10 | 1 | 0.22 |
choles-Q4.dat | 5291 | 11 | 3 | 0.46 |
choles-Q5.dat | 5033 | 10 | 6 | 0.41 |
choles-Q6.dat | 1196 | 9 | 1 | 0.12 |
thomr-C23.dat | 4105 | 11 | 6 | 0.54 |
thomr-SX3.dat | 2298 | 13 | 6 | 0.53 |
thomr-WC3.dat | 3275 | 16 | 3 | 0.56 |
thomr-Z12.dat | 2298 | 13 | 1 | 0.45 |
thomr-Z15.dat | 1814 | 15 | 1 | 0.28 |
These random benchmarks were created by David Monniaux for testing a new quantifier elimination method [5]. They have been selected from the Mjollnir repository. For simplification purposes, the quantifier prefix is ignored.
name | size | before | after | time |
formula-026.m | 19 | 10 | 8 | 0.60 |
formula-142.m | 19 | 10 | 9 | 0.65 |
formula-151.m | 25 | 13 | 11 | 1.9 |
formula-192.m | 25 | 13 | 10 | 1.3 |
formula-107.m | 27 | 14 | 13 | 7.1 |
formula-069.m | 27 | 14 | 12 | 11 |
formula-147.m | 29 | 15 | 11 | 37 |
formula-011.m | 29 | 15 | 14 | 11 |
formula-124.m | 31 | 16 | 14 | 28 |
formula-115.m | 31 | 16 | 14 | 81 |
formula-227.m | 33 | 17 | 11 | 8.6 |
formula-263.m | 33 | 17 | 13 | 40 |
formula-094.m | 33 | 17 | 12 | 67 |
formula-228.m | 33 | 17 | 0 | 0.12 |
This document was translated from L^{A}T_{E}X by H^{E}V^{E}A.