Skip to main content
Join the official 2019 Python Developers SurveyStart the survey!

Pythonic interface between AIGs and SAT solvers.

Project description

py-aiger-sat

Pythonic interface between AIGs and SAT solvers.

Build Status codecov PyPI version License: MIT

Table of Contents

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

aiger_sat has two seperate API's. The first, called the Object API, centers around the SolverWrapper object - a thin wrapper around a pysat solver. The second is a Function API which exposes 4 functions solve, is_sat, is_valid, and are_equiv. The function API is primarily useful for simple 1-off SAT instances, where as the object API is more useful when incremental solves are needed, or the underlying pysat solver must be exposed.

Object API

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}

Function API

import aiger
import aiger_sat

x, y, z = map(aiger.atom, ['x', 'y', 'z'])
assert aiger_sat.is_sat(x & y & z)

model = aiger_sat.solve(x & y & z)
assert model == {'x': True, 'y': True, 'z': True}

assert aiger_sat.is_valid(aiger.atom(True))

expr1 = x & y
expr2 = x & y & (z | ~z)
assert aiger_sat.are_equiv(expr1, expr2)

BitVector Support

py-aiger-sat also natively supports the py-aiger-bv bitvector library.

To enable this support, make sure that py-aiger-bv is installed, either manually:

$ pip install py-aiger-bv

or by installing py-aiger-sat with the bitvector option:

$ pip install py-aiger-sat[bitvector] or $ poetry install --extras=bitvector

Usage is analogous to the non-bitvector usage.

from aiger_bv import atom
from aiger_sat import sat_bv

# Object API
expr = atom(4, 'x') & atom(4, 'y') < 2
f = sat_bv.SolverBVWrapper()
f.add_expr(expr)

model = f.get_model()

# Function API.
model = sat_bv.solve(expr)

print(model)
# {'x': (False, False, True, True), 'y': (False, False, True, True)}

Project details


Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Files for py-aiger-sat, version 1.0.1
Filename, size File type Python version Upload date Hashes
Filename, size py_aiger_sat-1.0.1-py3-none-any.whl (6.1 kB) File type Wheel Python version py3 Upload date Hashes View hashes
Filename, size py-aiger-sat-1.0.1.tar.gz (5.5 kB) File type Source Python version None Upload date Hashes View hashes

Supported by

Elastic Elastic Search Pingdom Pingdom Monitoring Google Google BigQuery Sentry Sentry Error logging AWS AWS Cloud computing DataDog DataDog Monitoring Fastly Fastly CDN SignalFx SignalFx Supporter DigiCert DigiCert EV certificate StatusPage StatusPage Status page