py-aiger-sat


Namepy-aiger-sat JSON
Version 3.0.7 PyPI version JSON
download
home_pagehttps://github.com/mvcisback/py-aiger-sat
SummaryPythonic interface between AIGs and SAT solvers.
upload_time2024-03-16 19:29:05
maintainer
docs_urlNone
authorMarcell Vazquez-Chanlatte
requires_python>=3.10,<4.0
licenseMIT
keywords
VCS
bugtrack_url
requirements No requirements were recorded.
Travis-CI No Travis.
coveralls test coverage No coveralls. 
            # py-aiger-sat
Pythonic interface between AIGs and SAT solvers.

[![Build Status](https://cloud.drone.io/api/badges/mvcisback/py-aiger-sat/status.svg)](https://cloud.drone.io/mvcisback/py-aiger-sat)
[![PyPI version](https://badge.fury.io/py/py-aiger-sat.svg)](https://badge.fury.io/py/py-aiger-sat)
[![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](https://opensource.org/licenses/MIT)

<!-- markdown-toc start - Don't edit this section. Run M-x markdown-toc-generate-toc again -->
**Table of Contents**

- [Installation](#installation)
- [Usage](#usage)

<!-- markdown-toc end -->


# 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](https://poetry.eustace.io/) 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

```python
from aiger_sat import SolverWrapper

solver = SolverWrapper()  # defaults to Glucose4

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

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


```python
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.

```python
# 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

```python
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.

```python
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)}
```

Raw data

            {
    "_id": null,
    "home_page": "https://github.com/mvcisback/py-aiger-sat",
    "name": "py-aiger-sat",
    "maintainer": "",
    "docs_url": null,
    "requires_python": ">=3.10,<4.0",
    "maintainer_email": "",
    "keywords": "",
    "author": "Marcell Vazquez-Chanlatte",
    "author_email": "mvc@linux.com",
    "download_url": "https://files.pythonhosted.org/packages/e8/ba/81ac15ed663d6e5d2b7b5ef3fecc2c0a3dbb8a32d388ae353cc2fe8ed16d/py_aiger_sat-3.0.7.tar.gz",
    "platform": null,
    "description": "# py-aiger-sat\nPythonic interface between AIGs and SAT solvers.\n\n[![Build Status](https://cloud.drone.io/api/badges/mvcisback/py-aiger-sat/status.svg)](https://cloud.drone.io/mvcisback/py-aiger-sat)\n[![PyPI version](https://badge.fury.io/py/py-aiger-sat.svg)](https://badge.fury.io/py/py-aiger-sat)\n[![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](https://opensource.org/licenses/MIT)\n\n<!-- markdown-toc start - Don't edit this section. Run M-x markdown-toc-generate-toc again -->\n**Table of Contents**\n\n- [Installation](#installation)\n- [Usage](#usage)\n\n<!-- markdown-toc end -->\n\n\n# Installation\n\nIf you just need to use `aiger_sat`, you can just run:\n\n`$ pip install py-aiger-sat`\n\nFor developers, note that this project uses the\n[poetry](https://poetry.eustace.io/) python package/dependency\nmanagement tool. Please familarize yourself with it and then\nrun:\n\n`$ poetry install`\n\n# Usage\n\n`aiger_sat` has two seperate API's. The first, called the Object API,\ncenters around the `SolverWrapper` object - a thin wrapper around a\n`pysat` solver. The second is a Function API which exposes 4 functions\n`solve`, `is_sat`, `is_valid`, and `are_equiv`. The function API is\nprimarily useful for simple 1-off SAT instances, where as the object\nAPI is more useful when incremental solves are needed, or the\nunderlying `pysat` solver must be exposed.\n\n## Object API\n\n```python\nfrom aiger_sat import SolverWrapper\n\nsolver = SolverWrapper()  # defaults to Glucose4\n\nfrom pysat.solvers import Glucose3\nsolver2 = SolverWrapper(solver=Glucose3)\n```\n\n`solver` operate on boolean expressions in the form of `aiger`\ncircuits with a single output. For example,\n\n\n```python\nimport aiger\n\nx, y, z = map(aiger.atom, ['x', 'y', 'z'])\n\nexpr = (x & y) | ~z\nsolver.add_expr(expr)\nassert solver.is_sat()\nmodel = solver.get_model()\nprint(model)  # {'x': True, 'y': False, 'z': False}\nassert expr(model)\n```\n\nFurther, `aiger_sat` supports making assumptions and computing\nunsat_cores.\n\n```python\n# Make invalid assumption.\nassert not solver.is_sat(assumptions={\n    'x': False,\n    'z': True,\n})\nassert not solver.unsolved\n\ncore = solver.get_unsat_core()\nassert core == {'x': False, 'z': True}\n```\n\n## Function API\n\n```python\nimport aiger\nimport aiger_sat\n\nx, y, z = map(aiger.atom, ['x', 'y', 'z'])\nassert aiger_sat.is_sat(x & y & z)\n\nmodel = aiger_sat.solve(x & y & z)\nassert model == {'x': True, 'y': True, 'z': True}\n\nassert aiger_sat.is_valid(aiger.atom(True))\n\nexpr1 = x & y\nexpr2 = x & y & (z | ~z)\nassert aiger_sat.are_equiv(expr1, expr2)\n```\n\n## BitVector Support\n\n`py-aiger-sat` also natively supports the `py-aiger-bv` bitvector\nlibrary.\n\nTo enable this support, make sure that `py-aiger-bv` is installed,\neither manually:\n\n`$ pip install py-aiger-bv`\n\nor by installing `py-aiger-sat` with the `bitvector` option:\n\n`$ pip install py-aiger-sat[bitvector]` or `$ poetry install --extras=bitvector`\n\nUsage is analogous to the non-bitvector usage.\n\n```python\nfrom aiger_bv import atom\nfrom aiger_sat import sat_bv\n\n# Object API\nexpr = atom(4, 'x') & atom(4, 'y') < 2\nf = sat_bv.SolverBVWrapper()\nf.add_expr(expr)\n\nmodel = f.get_model()\n\n# Function API.\nmodel = sat_bv.solve(expr)\n\nprint(model)\n# {'x': (False, False, True, True), 'y': (False, False, True, True)}\n```\n",
    "bugtrack_url": null,
    "license": "MIT",
    "summary": "Pythonic interface between AIGs and SAT solvers.",
    "version": "3.0.7",
    "project_urls": {
        "Homepage": "https://github.com/mvcisback/py-aiger-sat",
        "Repository": "https://github.com/mvcisback/py-aiger-sat"
    },
    "split_keywords": [],
    "urls": [
        {
            "comment_text": "",
            "digests": {
                "blake2b_256": "a6053b1ce109e32a7136c1942841f784d700bc26e12132acd94dc510ce21cb52",
                "md5": "ac9730ee1c72cae46de61d57ba2a60ae",
                "sha256": "301bf572ff67b14bb0121fa74a838219c6867506949206d462568e1c55e7ddbb"
            },
            "downloads": -1,
            "filename": "py_aiger_sat-3.0.7-py3-none-any.whl",
            "has_sig": false,
            "md5_digest": "ac9730ee1c72cae46de61d57ba2a60ae",
            "packagetype": "bdist_wheel",
            "python_version": "py3",
            "requires_python": ">=3.10,<4.0",
            "size": 6111,
            "upload_time": "2024-03-16T19:29:04",
            "upload_time_iso_8601": "2024-03-16T19:29:04.838607Z",
            "url": "https://files.pythonhosted.org/packages/a6/05/3b1ce109e32a7136c1942841f784d700bc26e12132acd94dc510ce21cb52/py_aiger_sat-3.0.7-py3-none-any.whl",
            "yanked": false,
            "yanked_reason": null
        },
        {
            "comment_text": "",
            "digests": {
                "blake2b_256": "e8ba81ac15ed663d6e5d2b7b5ef3fecc2c0a3dbb8a32d388ae353cc2fe8ed16d",
                "md5": "3de9ed7909468e38cae32e60e4edaff1",
                "sha256": "d59532d92ffb5f8de87f41503c3ef6890bbbe9494a9e13d96509294acf01e2e9"
            },
            "downloads": -1,
            "filename": "py_aiger_sat-3.0.7.tar.gz",
            "has_sig": false,
            "md5_digest": "3de9ed7909468e38cae32e60e4edaff1",
            "packagetype": "sdist",
            "python_version": "source",
            "requires_python": ">=3.10,<4.0",
            "size": 4727,
            "upload_time": "2024-03-16T19:29:05",
            "upload_time_iso_8601": "2024-03-16T19:29:05.867150Z",
            "url": "https://files.pythonhosted.org/packages/e8/ba/81ac15ed663d6e5d2b7b5ef3fecc2c0a3dbb8a32d388ae353cc2fe8ed16d/py_aiger_sat-3.0.7.tar.gz",
            "yanked": false,
            "yanked_reason": null
        }
    ],
    "upload_time": "2024-03-16 19:29:05",
    "github": true,
    "gitlab": false,
    "bitbucket": false,
    "codeberg": false,
    "github_user": "mvcisback",
    "github_project": "py-aiger-sat",
    "travis_ci": false,
    "coveralls": false,
    "github_actions": false,
    "lcname": "py-aiger-sat"
}
Marcell Vazquez-Chanlatte
Elapsed time: 0.81912s