Simplification of Boolean Affine Formulas - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2011

Simplification of Boolean Affine Formulas

Résumé

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.
Les expressions affines booléennes, qui combinent des inégalités affines à l'aide d'opérateurs booléens, apparaissent dans de nombreux domaines de l'informatique comme l'analyse statique, la génération de code, la synthèse matérielle et le \emph{model checking} symbolique. Elles permettent de représenter de façon compacte des ensembles trés grands et même infinis. Les algorithmes qui permettent de les manipuler ont tendence à construire des formules fortement redondantes et de taille croissante; il est donc nécessaire d'utiliser un simplifieur si l'on veut en maintenir la complexité dans des limites raisonables. La simplification est un problème difficile, au moins aussi difficile que le test de satisfiabilité, et donc de complexité exponentielle dans le pire cas. Cet article propose une nouvelle méthode de simplification, basée sur l'analyse des chemins dans un diagramme de décision ordonné. Cette méthode est capable d'exploiter les régularités d'une formule pour en accélérer la simplification. L'algorithme a été implémenté en Java et testé sur une série d'exemples en provenance de divers domaines d'application.
Fichier principal
Vignette du fichier
RR-7689.pdf (399.52 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00609519 , version 1 (19-07-2011)

Identifiants

  • HAL Id : inria-00609519 , version 1

Citer

Paul Feautrier. Simplification of Boolean Affine Formulas. [Research Report] RR-7689, INRIA. 2011, pp.15. ⟨inria-00609519⟩
133 Consultations
152 Téléchargements

Partager

Gmail Facebook X LinkedIn More