Local Two-Level And-Inverter Graph / Minimization without Blowup

Robert Brummayer; Armin Biere

Local Two-Level And-Inverter Graph / Minimization without Blowup

Robert Brummayer, Armin Biere

Institute of Formal Models and Verification

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

Abstract

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.

Original language	English
Title of host publication	2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'06)
Number of pages	7
Publication status	Published - 2006

Fields of science

101013 Mathematical logic
102 Computer Sciences

Cite this

@inproceedings{15eb1a3a921c477ea4d2d65aadf9efa8,

title = "Local Two-Level And-Inverter Graph / Minimization without Blowup",

abstract = "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.",

author = "Robert Brummayer and Armin Biere",

year = "2006",

language = "English",

booktitle = "2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'06)",

}

TY - GEN

T1 - Local Two-Level And-Inverter Graph / Minimization without Blowup

AU - Brummayer, Robert

AU - Biere, Armin

PY - 2006

Y1 - 2006

N2 - 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.

AB - 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.

M3 - Conference proceedings

BT - 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'06)

ER -