Armin Biere, Katalin Fazekas, Dr., Mathias Fleury, Nils Froleyks,
"Clausal Congruence Closure"
, in Supratik Chakraborty and Jie-Hong Roland Jiang: 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024), Serie Leibniz International Proceedings in Informatics, Dagstuhl Publishing, Seite(n) 6:1-6:25, 2024
Original Titel:
Clausal Congruence Closure
Sprache des Titels:
Englisch
Original Buchtitel:
27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Original Kurzfassung:
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.
Forschungs-