Local Two-Level And-Inverer Graph Minimization without Blowup

Beschreibung

And-Inverter Graphs (AIGs) are an efficient and scalable representation for boolean formulas and circuits. We present a maximal set of rules for local two-level optimization of AIGs. This set consists of rules which can be applied before node creation greedily without affecting structural sharing negatively. We implemented these techniques in the AIG library of our tool SMV2QBF and report on experimental results in the context of SAT based model checking.

Zeitraum	28 Okt. 2006
Ereignistitel	2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'06), Mikulov, Czechia
Veranstaltungstyp	Konferenz
Ort	Tschechische RepublikAuf Karte anzeigen