Simplification of Boolean Affine Formulas

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.

1  Method

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.

2  Benchmarks, C Syntax

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].

3  Benchmarks, Mathematica Syntax

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.

References

[1]

Christophe Alias, Bogdan Pasca, and Alexandru Plesco. Automatic generation of fpga-specific pipelined accelerators. In Andreas Koch, Ram Krishnamurthy, John McAllister, Roger Woods, and Tarek A. El-Ghazawi, editors, Reconfigurable Computing: Architectures, Tools and Applications - 7th International Symposium, ARC 2011, Belfast, UK, volume 6578 of Lecture Notes in Computer Science, pages 53–66, 2011.

[2]

Pierre Boulet and Paul Feautrier. Scanning polyhedra without DO loops. In PACT’98, October 1998.

[3]

Isil Dillig, Thomas Dillig, and Alex Aiken. Small formulas for large programs: On-line constraint simplification in scalable static analysis. In Radhia Cousot and Mathieu Martel, editors, SAS 2010, LNCS 6337, pages 236–252. Springer, 2010.

[4]

Paul Feautrier. Simplification of Boolean Affine Formulas. Technical Report RR-7689, INRIA, July 2011.

[5]

David Monniaux. Quantifier elimination by lazy model enumeration. In Tayssir Touili, Byron Cook, and Paul Jackson, editors, Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, volume 6174 of Lecture Notes in Computer Science, pages 585–599, 2010.

[6]

Christoph Scholl, Stefan Disch, Florian Pigorsh, and Stefan Kupferschmid. Computing optimized representations for non-convex polyhedra by detection and removal of redundant linear constraints. In Kowalewski S. and Philippou A., editors, TACAS 2009, LNCS 5505, pages 383–397. Springer, 2009.

This document was translated from L^AT_EX by H^EV^EA.