SAT solving
And-inverter graph
Abbreviated AIG
A graph representation built from and nodes and complemented edges.
Definition
And-inverter graph
An and-inverter graph (AIG) represents Boolean structure with conjunction nodes and optional negation on edges.
AIGs make sharing and local simplification explicit. Axeyum can lower an AIG to CNF before SAT search.
01
Example
The shared subexpression a and b can appear once as a node even when several outputs use it.
02
Important distinction
An AIG is a representation of the formula, not the search algorithm that decides it.
After reading this article, you should be able to
- Define AIG in the sense used on this site.
- Explain why a graph can share repeated Boolean subexpressions.