Gröbner Bases for Boolean Function Minimization
International audience Boolean function minimization techniques try to find, for a given formula, a smaller equivalent formula. In this work, we present a novel technique for heuristic boolean function minimization. By using an algebraic encoding, we embed the minimization problem into an algebraic...
Main Authors: | , |
---|---|
Other Authors: | , , , , , , , , |
Format: | Conference Object |
Language: | English |
Published: |
HAL CCSD
1481
|
Subjects: | |
Online Access: | https://inria.hal.science/hal-04315477 https://inria.hal.science/hal-04315477/document https://inria.hal.science/hal-04315477/file/short4.pdf |
id |
ftunilorrainehal:oai:HAL:hal-04315477v1 |
---|---|
record_format |
openpolar |
spelling |
ftunilorrainehal:oai:HAL:hal-04315477v1 2023-12-31T10:23:43+01:00 Gröbner Bases for Boolean Function Minimization Faroß, Nicolas Schwarz, Simon Universität des Saarlandes Saarbrücken Max-Planck-Institut für Informatik (MPII) Max-Planck-Gesellschaft Modeling and Verification of Distributed Algorithms and Systems (VERIDIS) Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM) Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA) Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA) Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS) Tromsø, Norway 2024-07-28 https://inria.hal.science/hal-04315477 https://inria.hal.science/hal-04315477/document https://inria.hal.science/hal-04315477/file/short4.pdf en eng HAL CCSD hal-04315477 https://inria.hal.science/hal-04315477 https://inria.hal.science/hal-04315477/document https://inria.hal.science/hal-04315477/file/short4.pdf http://creativecommons.org/licenses/by/ info:eu-repo/semantics/OpenAccess Proceedings of the 8th SC-Square Workshop https://inria.hal.science/hal-04315477 Proceedings of the 8th SC-Square Workshop, Jul 2024, Tromsø, Norway Multi-level Logic Optimization Boolean Function Synthesis Gröbner Bases Multi-level Logic Optimization Boolean Function Synthesis Gröbner Bases [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] info:eu-repo/semantics/conferenceObject Conference papers 1481 ftunilorrainehal 2023-12-05T23:39:17Z International audience Boolean function minimization techniques try to find, for a given formula, a smaller equivalent formula. In this work, we present a novel technique for heuristic boolean function minimization. By using an algebraic encoding, we embed the minimization problem into an algebraic domain, where algorithms for computing Gröbner bases are applicable. A Gröbner basis usually forms a compact representation of our encoded function. From the Gröbner basis, we then reconstruct an equivalent, more compact boolean formula. Our approach is the first to use Gröbner bases for function minimization. Combined with advances of algebraic Gröbner bases in satisfiability checking, this motivates further research on applications of Gröbner bases in the context of boolean logic. Conference Object Tromsø Université de Lorraine: HAL |
institution |
Open Polar |
collection |
Université de Lorraine: HAL |
op_collection_id |
ftunilorrainehal |
language |
English |
topic |
Multi-level Logic Optimization Boolean Function Synthesis Gröbner Bases Multi-level Logic Optimization Boolean Function Synthesis Gröbner Bases [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] |
spellingShingle |
Multi-level Logic Optimization Boolean Function Synthesis Gröbner Bases Multi-level Logic Optimization Boolean Function Synthesis Gröbner Bases [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] Faroß, Nicolas Schwarz, Simon Gröbner Bases for Boolean Function Minimization |
topic_facet |
Multi-level Logic Optimization Boolean Function Synthesis Gröbner Bases Multi-level Logic Optimization Boolean Function Synthesis Gröbner Bases [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] |
description |
International audience Boolean function minimization techniques try to find, for a given formula, a smaller equivalent formula. In this work, we present a novel technique for heuristic boolean function minimization. By using an algebraic encoding, we embed the minimization problem into an algebraic domain, where algorithms for computing Gröbner bases are applicable. A Gröbner basis usually forms a compact representation of our encoded function. From the Gröbner basis, we then reconstruct an equivalent, more compact boolean formula. Our approach is the first to use Gröbner bases for function minimization. Combined with advances of algebraic Gröbner bases in satisfiability checking, this motivates further research on applications of Gröbner bases in the context of boolean logic. |
author2 |
Universität des Saarlandes Saarbrücken Max-Planck-Institut für Informatik (MPII) Max-Planck-Gesellschaft Modeling and Verification of Distributed Algorithms and Systems (VERIDIS) Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM) Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA) Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA) Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS) |
format |
Conference Object |
author |
Faroß, Nicolas Schwarz, Simon |
author_facet |
Faroß, Nicolas Schwarz, Simon |
author_sort |
Faroß, Nicolas |
title |
Gröbner Bases for Boolean Function Minimization |
title_short |
Gröbner Bases for Boolean Function Minimization |
title_full |
Gröbner Bases for Boolean Function Minimization |
title_fullStr |
Gröbner Bases for Boolean Function Minimization |
title_full_unstemmed |
Gröbner Bases for Boolean Function Minimization |
title_sort |
gröbner bases for boolean function minimization |
publisher |
HAL CCSD |
publishDate |
1481 |
url |
https://inria.hal.science/hal-04315477 https://inria.hal.science/hal-04315477/document https://inria.hal.science/hal-04315477/file/short4.pdf |
op_coverage |
Tromsø, Norway |
genre |
Tromsø |
genre_facet |
Tromsø |
op_source |
Proceedings of the 8th SC-Square Workshop https://inria.hal.science/hal-04315477 Proceedings of the 8th SC-Square Workshop, Jul 2024, Tromsø, Norway |
op_relation |
hal-04315477 https://inria.hal.science/hal-04315477 https://inria.hal.science/hal-04315477/document https://inria.hal.science/hal-04315477/file/short4.pdf |
op_rights |
http://creativecommons.org/licenses/by/ info:eu-repo/semantics/OpenAccess |
_version_ |
1786835481099501568 |