Activity: Talk or presentation › Contributed talk › unknown
Description
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.
Period
28 Oct 2006
Event title
2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'06), Mikulov, Czechia