		Search-engine friendly clone of the ACL2 documentation.

Boolean-reasoning

Aig

A hons-based And-Inverter Graph (AIG) library for representing and manipulating Boolean functions.

Introduction

And-Inverter Graphs are a way to represent Boolean functions using only the operations and and not.

This AIG library, found in centaur/aig, is sometimes called the Hons-AIG library to distinguish it from another AIG library, aignet. Very briefly:

Hons-AIGs are simpler, easier to work with, and easier to reason about.
aignet is faster.

We won't say anything more about Aignet here. A much more detailed comparison of the libraries is available in: Jared Davis and Sol Swords. Verified AIG Algorithms in ACL2. In ACL2 Workshop 2013. May, 2013. EPTCS 114. Pages 95-110.

Representation of AIGs

We always construct AIGs with hons so that existing pieces of AIGs will be automatically reused. We represent AIGs as arbitrary cons trees, which we interpret as follows:

T represents the constant-true function.
NIL represents the constant-false function.
Any other atom represents a Boolean variable (i.e., an input to the function.)
A cons of the form (A . NIL) represents the negation of A.
Any other cons, (A . B), represents the conjunction of A and B.

Note that every ACL2 object is a well-formed AIG under this definition.

This meaning of cons trees is given by the evaluation function aig-eval, which returns the (Boolean) value of an AIG under some particular assignment to its variables. This function naturally induces an equivalence relation, aig-equiv: two AIGs are semantically equivalent if they have the same evaluation under every possible variable assignment.

You might wonder why we would restrict ourselves to using only and and not? On the surface, using a richer language like S-expressions might seem more compact. For instance, with S-expressions we could represent (or a b) is much smaller looking than its and/not equivalent: (not (and (not a) (not b))).

But another critical part of memory efficiency is structure sharing. That is, suppose that we already need (not a) and (not b) elsewhere in the function. With s-expressions, these terms would have nothing in common with (or a b), but with AIGs we can reuse the existing parts of (not (and (not a) (not b))).

Library Functions

Besides the aig-semantics functions like aig-eval and aig-equiv, the real core of the library includes:

Basic, low-level aig-constructors for building AIGs (and, or, etc.). We prove these operations correct with respect to aig-eval.
Somewhat higher-level aig-substitution operations, like aig-restrict, aig-compose, and aig-partial-eval.
Operations for collecting the variables from an AIG, such as aig-vars.

We provide some tools to "solve" AIGs. Historically we have heavily used the bddify algorithm, which constructs a BDD from an AIG. More recently, aig-sat provides a nice alternative using aignet and satlink to give the problem to a SAT solver.

Beyond this, the rest of the library is a hodgepodge of aig-other algorithms for working with AIGs.

AIGs versus BDDs

Another option for representing Boolean functions would be to use BDDs. In comparison with BDDs, AIGs are:

cheaper to construct, e.g., if we want to or together the functions f and g, it only takes a few conses with AIGs, whereas with BDDs we need to walk through f and g to construct a new structure (which might be quite large); but
more expensive to compare, e.g., with BDDs we can determine if f and g are equal via pointer equality, whereas with AIGs this is a satisfiability problem.

This tradeoff is often worth it. For instance, it can often be more faster to construct an AIG and then bddify it than to just directly build the BDD. Why? With the whole AIG visible, the bddify algorithm can often "prune" branches of the AIG that turn out to be irrelevant, and hence avoid constructing large parts of the BDD that aren't really needed.

Subtopics

Aig-constructors: Low-level functions for constructing AIGs.
Aig-vars: (aig-vars x) returns the variables of the AIG X.
Aig-sat: Determine whether an AIG is satisfiable.
Bddify: An verified algorithm for converting aigs into ubdds.
Aig-substitution: AIG operations for carrying out substitutions, compositions, and partial evaluations.
Aig-other: Various hard-to-categorize algorithms for working with AIGs.
Aig-semantics: Functions related to the semantic meaning of AIGs, e.g., aig-eval and aig-equiv.
Aig-and-count: Counts how many ANDs are in an AIG.