Simplification of Boolean Affine Formulas

Paul Feautrier 1
1 COMPSYS - Compilation and embedded computing systems
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
Abstract : 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.
Complete list of metadatas

Cited literature [3 references]  Display  Hide  Download

https://hal.inria.fr/inria-00609519
Contributor : Paul Feautrier <>
Submitted on : Tuesday, July 19, 2011 - 1:07:56 PM
Last modification on : Wednesday, November 20, 2019 - 3:27:40 AM
Long-term archiving on: Monday, November 12, 2012 - 11:15:43 AM

File

RR-7689.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00609519, version 1

Collections

Citation

Paul Feautrier. Simplification of Boolean Affine Formulas. [Research Report] RR-7689, INRIA. 2011, pp.15. ⟨inria-00609519⟩

Share

Metrics

Record views

322

Files downloads

238