py-aiger-sat 0.1.0

Pythonic interface between AIGs and SAT solvers.

py-aiger-sat

Pythonic interface between AIGs and SAT solvers.

Table of Contents

• Installation
• Usage

Installation

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

$ pip install py-aiger-sat

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

$ poetry install

Usage

The primary entry point for aiger_sat is the SolverWrapper object which is a thin wrapper around a pysat solver.

from aiger_sat import SolverWrapper

solver = SolverWrapper()  # defaults to Glucose4

from pysat.solver import Glucose3
solver2 = SolverWrapper(solver=Glucose3)

solver operate on boolean expressions in the form of aiger circuits with a single output. For example,

import aiger

x, y, z = map(aiger.atom, ['x', 'y', 'z'])

expr = (x & y) | ~z
solver.add_expr(expr)
assert solver.is_sat()
model = solver.get_model()
print(model)  # {'x': True, 'y': False, 'z': False}
assert expr(model)

Further, aiger_sat supports making assumptions and computing unsat_cores.

# Make invalid assumption.
assert not solver.is_sat(assumptions={
    'x': False,
    'z': True,
})
assert not solver.unsolved

core = solver.get_unsat_core()
assert core == {'x': False, 'z': True}