Pythonic interface between AIGs and SAT solvers.
Project description
py-aiger-sat
Pythonic interface between AIGs and SAT solvers.
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
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}
Project details
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distribution
Hashes for py_aiger_sat-0.1.0-py3-none-any.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 5399c036ca838a34874596c1f8c078fbaa20f0e403c7acc80864ad1d0a82756f |
|
MD5 | 59a89e76c4ba0f86281a77ab400b4d7b |
|
BLAKE2b-256 | 88741b2ca222f52a48a4de4ea0997b11ea0fca4720f971cc10a50f87c2d23364 |