Python library to convert between AIGER and CNF

Table of Contents

• Installation
• Usage

If you just need to use aiger_cnf, you can just run:

$ pip install py-aiger-cnf

For developers, note that this project uses the poetry python package/dependency management tool. Please familarize yourself with it and then run:

$ poetry install

The primary entry point for using aiger_cnf is the aig2cnf function which, unsurprisingly, maps AIG objects to CNF objects.

import aiger
from aiger_cnf import aig2cnf

x, y, z = map(aiger.atom, ('x', 'y', 'z'))
expr = (x & y) | ~z
cnf = aig2cnf(expr.aig)

Note that this library also supports aiger wrapper libraries so long as they export a .aig attribute. Thus, could also write:

cnf = aig2cnf(expr)

The CNF object is a NamedTuple with the following three fields:

1. clauses: A list of tuples of ints, e.g., [(1,2,3), (-1, 2)]. Each integer represents a variable's id, with the sign indicating the polarity of the variable.
2. input2lit: A bidict from input names to variable ids.
3. output2lit: A bidict from output names to variable ids.