Clausal congruence closure
Abstract: Many practical applications of satisfiability solving employ multiple steps to encode an original
problem formulation into conjunctive normal form. Often circuits are used as intermediate representation before encoding those circuits into clausal form. These circuits however might contain
redundant isomorphic sub-circuits. If blindly translated into clausal form, this redundancy is retained and increases solving time unless specific preprocessing algorithms are used. Furthermore, such redundant sub-formula structure might only emerge during solving and needs to be addressed by
inprocessing. This paper presents a new approach which extracts gate information from the formula
and applies congruence closure to match and eliminate redundant gates. Besides new algorithms for gate extraction, we also describe previous unpublished attempts to tackle this problem. Experiments focus on the important problem of combinational equivalence checking for hardware designs and show that our new approach yields a substantial gain in CNF solver performance
- Location
-
Deutsche Nationalbibliothek Frankfurt am Main
- Extent
-
Online-Ressource
- Language
-
Englisch
- Notes
-
27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). - Wadern, 2024. - 6:1-6:25, ISBN: 978-3-95977-334-8
- Event
-
Veröffentlichung
- (where)
-
Freiburg
- (who)
-
Universität
- (when)
-
2024
- Creator
- DOI
-
10.4230/lipics.sat.2024.6
- URN
-
urn:nbn:de:bsz:25-freidok-2566577
- Rights
-
Open Access; Der Zugriff auf das Objekt ist unbeschränkt möglich.
- Last update
-
25.03.2025, 1:57 PM CET
Data provider
Deutsche Nationalbibliothek. If you have any questions about the object, please contact the data provider.
Associated
- Biere, Armin
- Fazekas, Katalin
- Fleury, Mathias
- Froleyks, Nils
- Universität
Time of origin
- 2024
Other Objects (12)
Linking actual self-congruence, ideal self-congruence, and functional congruence to donor loyalty: the moderating role of issue involvement
Message (in)congruence: tweeting while competing for donations
Benefits of matching consumers’ personality: creating perceived trustworthiness via actual self-congruence and perceived competence via ideal self-congruence
Managing vascular access and closure for percutaneous mechanical circulatory support
Phagophore closure, autophagosome maturation and autophagosome fusion during macroautophagy in the yeast Saccharomyces cerevisiae
Congruence constructs as mediators of stereotypic image perceptions’ effect on student volunteering intention
Congruence properties of endoclasses...
Closure
Linking actual self-congruence, ideal self-congruence, and functional congruence to donor loyalty: the moderating role of issue involvement
Congruence classes in universal algebra
Dagger closure
Blessing or Curse for Congruence? How Interest Mobilization Affects Congruence between Citizens and Elected Representatives
Linking actual self-congruence, ideal self-congruence, and functional congruence to donor loyalty: the moderating role of issue involvement
Message (in)congruence: tweeting while competing for donations
Benefits of matching consumers’ personality: creating perceived trustworthiness via actual self-congruence and perceived competence via ideal self-congruence
Managing vascular access and closure for percutaneous mechanical circulatory support
Phagophore closure, autophagosome maturation and autophagosome fusion during macroautophagy in the yeast Saccharomyces cerevisiae
Congruence constructs as mediators of stereotypic image perceptions’ effect on student volunteering intention
Congruence properties of endoclasses...
Closure
Linking actual self-congruence, ideal self-congruence, and functional congruence to donor loyalty: the moderating role of issue involvement
Congruence classes in universal algebra
Dagger closure
Blessing or Curse for Congruence? How Interest Mobilization Affects Congruence between Citizens and Elected Representatives
Linking actual self-congruence, ideal self-congruence, and functional congruence to donor loyalty: the moderating role of issue involvement
Message (in)congruence: tweeting while competing for donations
Benefits of matching consumers’ personality: creating perceived trustworthiness via actual self-congruence and perceived competence via ideal self-congruence
Managing vascular access and closure for percutaneous mechanical circulatory support
Phagophore closure, autophagosome maturation and autophagosome fusion during macroautophagy in the yeast Saccharomyces cerevisiae
Congruence constructs as mediators of stereotypic image perceptions’ effect on student volunteering intention
Congruence properties of endoclasses...
Closure
Linking actual self-congruence, ideal self-congruence, and functional congruence to donor loyalty: the moderating role of issue involvement
Congruence classes in universal algebra
Dagger closure