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
- Standort
-
Deutsche Nationalbibliothek Frankfurt am Main
- Umfang
-
Online-Ressource
- Sprache
-
Englisch
- Anmerkungen
-
27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). - Wadern, 2024. - 6:1-6:25, ISBN: 978-3-95977-334-8
- Ereignis
-
Veröffentlichung
- (wo)
-
Freiburg
- (wer)
-
Universität
- (wann)
-
2024
- Urheber
- DOI
-
10.4230/lipics.sat.2024.6
- URN
-
urn:nbn:de:bsz:25-freidok-2566577
- Rechteinformation
-
Open Access; Der Zugriff auf das Objekt ist unbeschränkt möglich.
- Letzte Aktualisierung
-
15.08.2025, 07:32 MESZ
Datenpartner
Dieses Objekt wird bereitgestellt von:
Deutsche Nationalbibliothek. Bei Fragen zum Objekt wenden Sie sich bitte an den Datenpartner.
Deutsche Nationalbibliothek. Bei Fragen zum Objekt wenden Sie sich bitte an den Datenpartner.
Beteiligte
- Biere, Armin
- Fazekas, Katalin
- Fleury, Mathias
- Froleyks, Nils
- Universität
Entstanden
- 2024
Ähnliche Objekte (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
NP-completeness of small conflict set generation for congruence closure
Benefits of matching consumers’ personality: creating perceived trustworthiness via actual self-congruence and perceived competence via ideal self-congruence
Congruence constructs as mediators of stereotypic image perceptions’ effect on student volunteering intention
The dynamics of consumer boycott intention: Examining the roles of moral reasoning, cognitive dissonance, and self-congruence
The pursuit of the ideal self: an investigation of the relationship of authenticity and 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 properties of endoclasses...
Linking actual self-congruence, ideal self-congruence, and functional congruence to donor loyalty: the moderating role of issue involvement
Linking actual self-congruence, ideal self-congruence, and functional congruence to donor loyalty: the moderating role of issue involvement
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
NP-completeness of small conflict set generation for congruence closure
Benefits of matching consumers’ personality: creating perceived trustworthiness via actual self-congruence and perceived competence via ideal self-congruence
Congruence constructs as mediators of stereotypic image perceptions’ effect on student volunteering intention
The dynamics of consumer boycott intention: Examining the roles of moral reasoning, cognitive dissonance, and self-congruence
The pursuit of the ideal self: an investigation of the relationship of authenticity and 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 properties of endoclasses...
Linking actual self-congruence, ideal self-congruence, and functional congruence to donor loyalty: the moderating role of issue involvement
Linking actual self-congruence, ideal self-congruence, and functional congruence to donor loyalty: the moderating role of issue involvement
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
NP-completeness of small conflict set generation for congruence closure
Benefits of matching consumers’ personality: creating perceived trustworthiness via actual self-congruence and perceived competence via ideal self-congruence
Congruence constructs as mediators of stereotypic image perceptions’ effect on student volunteering intention
The dynamics of consumer boycott intention: Examining the roles of moral reasoning, cognitive dissonance, and self-congruence
The pursuit of the ideal self: an investigation of the relationship of authenticity and 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 properties of endoclasses...
Linking actual self-congruence, ideal self-congruence, and functional congruence to donor loyalty: the moderating role of issue involvement