Skip to Main content Skip to Navigation

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


Files produced by the author(s)


  • HAL Id : inria-00609519, version 1



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



Record views


Files downloads