===========================================
pycosat: bindings to picosat (a SAT solver)
===========================================
`PicoSAT <http://fmv.jku.at/picosat/>`_ is a popular
`SAT <http://en.wikipedia.org/wiki/Boolean_satisfiability_problem>`_ solver
written by Armin Biere in pure C.
This package provides efficient Python bindings to picosat on the C level,
i.e. when importing pycosat, the picosat solver becomes part of the
Python process itself. For ease of deployment, the picosat source (namely
picosat.c and picosat.h) is included in this project. These files have
been extracted from the picosat source (picosat-965.tar.gz).
Usage
-----
The ``pycosat`` module has two functions ``solve`` and ``itersolve``,
both of which take an iterable of clauses as an argument. Each clause
is itself represented as an iterable of (non-zero) integers.
The function ``solve`` returns one of the following:
* one solution (a list of integers)
* the string "UNSAT" (when the clauses are unsatisfiable)
* the string "UNKNOWN" (when a solution could not be determined within the
propagation limit)
The function ``itersolve`` returns an iterator over solutions. When the
propagation limit is specified, exhausting the iterator may not yield all
possible solutions.
Both functions take the following keyword arguments:
* ``prop_limit``: the propagation limit (integer)
* ``vars``: number of variables (integer)
* ``verbose``: the verbosity level (integer)
Example
-------
Let us consider the following clauses, represented using
the DIMACS `cnf <http://en.wikipedia.org/wiki/Conjunctive_normal_form>`_
format::
p cnf 5 3
1 -5 4 0
-1 5 3 4 0
-3 -4 0
Here, we have 5 variables and 3 clauses, the first clause being
(x\ :sub:`1` or not x\ :sub:`5` or x\ :sub:`4`).
Note that the variable x\ :sub:`2` is not used in any of the clauses,
which means that for each solution with x\ :sub:`2` = True, we must
also have a solution with x\ :sub:`2` = False. In Python, each clause is
most conveniently represented as a list of integers. Naturally, it makes
sense to represent each solution also as a list of integers, where the sign
corresponds to the Boolean value (+ for True and - for False) and the
absolute value corresponds to i\ :sup:`th` variable::
>>> import pycosat
>>> cnf = [[1, -5, 4], [-1, 5, 3, 4], [-3, -4]]
>>> pycosat.solve(cnf)
[1, -2, -3, -4, 5]
This solution translates to: x\ :sub:`1` = x\ :sub:`5` = True,
x\ :sub:`2` = x\ :sub:`3` = x\ :sub:`4` = False
To find all solutions, use ``itersolve``::
>>> for sol in pycosat.itersolve(cnf):
... print sol
...
[1, -2, -3, -4, 5]
[1, -2, -3, 4, -5]
[1, -2, -3, 4, 5]
...
>>> len(list(pycosat.itersolve(cnf)))
18
In this example, there are a total of 18 possible solutions, which had to
be an even number because x\ :sub:`2` was left unspecified in the clauses.
The fact that ``itersolve`` returns an iterator, makes it very elegant
and efficient for many types of operations. For example, using
the ``itertools`` module from the standard library, here is how one
would construct a list of (up to) 3 solutions::
>>> import itertools
>>> list(itertools.islice(pycosat.itersolve(cnf), 3))
[[1, -2, -3, -4, 5], [1, -2, -3, 4, -5], [1, -2, -3, 4, 5]]
Implementation of itersolve
---------------------------
How does one go from having found one solution to another solution?
The answer is surprisingly simple. One adds the *inverse* of the already
found solution as a new clause. This new clause ensures that another
solution is searched for, as it *excludes* the already found solution.
Here is basically a pure Python implementation of ``itersolve`` in terms
of ``solve``::
def py_itersolve(clauses): # don't use this function!
while True: # (it is only here to explain things)
sol = pycosat.solve(clauses)
if isinstance(sol, list):
yield sol
clauses.append([-x for x in sol])
else: # no more solutions -- stop iteration
return
This implementation has several problems. Firstly, it is quite slow as
``pycosat.solve`` has to convert the list of clauses over and over and over
again. Secondly, after calling ``py_itersolve`` the list of clauses will
be modified. In pycosat, ``itersolve`` is implemented on the C level,
making use of the picosat C interface (which makes it much, much faster
than the naive Python implementation above).
Raw data
{
"_id": null,
"home_page": "https://github.com/ContinuumIO/pycosat",
"name": "pycosat",
"maintainer": "",
"docs_url": null,
"requires_python": "",
"maintainer_email": "",
"keywords": "",
"author": "Ilan Schnell",
"author_email": "ilan@continuum.io",
"download_url": "https://files.pythonhosted.org/packages/5b/81/cf8ebf77fc4f06f680ad3ee43d0d01826f6d6054828f1cf3b42d944b82a1/pycosat-0.6.6.tar.gz",
"platform": null,
"description": "===========================================\npycosat: bindings to picosat (a SAT solver)\n===========================================\n\n`PicoSAT <http://fmv.jku.at/picosat/>`_ is a popular\n`SAT <http://en.wikipedia.org/wiki/Boolean_satisfiability_problem>`_ solver\nwritten by Armin Biere in pure C.\nThis package provides efficient Python bindings to picosat on the C level,\ni.e. when importing pycosat, the picosat solver becomes part of the\nPython process itself. For ease of deployment, the picosat source (namely\npicosat.c and picosat.h) is included in this project. These files have\nbeen extracted from the picosat source (picosat-965.tar.gz).\n\nUsage\n-----\n\nThe ``pycosat`` module has two functions ``solve`` and ``itersolve``,\nboth of which take an iterable of clauses as an argument. Each clause\nis itself represented as an iterable of (non-zero) integers.\n\nThe function ``solve`` returns one of the following:\n * one solution (a list of integers)\n * the string \"UNSAT\" (when the clauses are unsatisfiable)\n * the string \"UNKNOWN\" (when a solution could not be determined within the\n propagation limit)\n\nThe function ``itersolve`` returns an iterator over solutions. When the\npropagation limit is specified, exhausting the iterator may not yield all\npossible solutions.\n\nBoth functions take the following keyword arguments:\n * ``prop_limit``: the propagation limit (integer)\n * ``vars``: number of variables (integer)\n * ``verbose``: the verbosity level (integer)\n\n\nExample\n-------\n\nLet us consider the following clauses, represented using\nthe DIMACS `cnf <http://en.wikipedia.org/wiki/Conjunctive_normal_form>`_\nformat::\n\n p cnf 5 3\n 1 -5 4 0\n -1 5 3 4 0\n -3 -4 0\n\nHere, we have 5 variables and 3 clauses, the first clause being\n(x\\ :sub:`1` or not x\\ :sub:`5` or x\\ :sub:`4`).\nNote that the variable x\\ :sub:`2` is not used in any of the clauses,\nwhich means that for each solution with x\\ :sub:`2` = True, we must\nalso have a solution with x\\ :sub:`2` = False. In Python, each clause is\nmost conveniently represented as a list of integers. Naturally, it makes\nsense to represent each solution also as a list of integers, where the sign\ncorresponds to the Boolean value (+ for True and - for False) and the\nabsolute value corresponds to i\\ :sup:`th` variable::\n\n >>> import pycosat\n >>> cnf = [[1, -5, 4], [-1, 5, 3, 4], [-3, -4]]\n >>> pycosat.solve(cnf)\n [1, -2, -3, -4, 5]\n\nThis solution translates to: x\\ :sub:`1` = x\\ :sub:`5` = True,\nx\\ :sub:`2` = x\\ :sub:`3` = x\\ :sub:`4` = False\n\nTo find all solutions, use ``itersolve``::\n\n >>> for sol in pycosat.itersolve(cnf):\n ... print sol\n ...\n [1, -2, -3, -4, 5]\n [1, -2, -3, 4, -5]\n [1, -2, -3, 4, 5]\n ...\n >>> len(list(pycosat.itersolve(cnf)))\n 18\n\nIn this example, there are a total of 18 possible solutions, which had to\nbe an even number because x\\ :sub:`2` was left unspecified in the clauses.\n\nThe fact that ``itersolve`` returns an iterator, makes it very elegant\nand efficient for many types of operations. For example, using\nthe ``itertools`` module from the standard library, here is how one\nwould construct a list of (up to) 3 solutions::\n\n >>> import itertools\n >>> list(itertools.islice(pycosat.itersolve(cnf), 3))\n [[1, -2, -3, -4, 5], [1, -2, -3, 4, -5], [1, -2, -3, 4, 5]]\n\n\nImplementation of itersolve\n---------------------------\n\nHow does one go from having found one solution to another solution?\nThe answer is surprisingly simple. One adds the *inverse* of the already\nfound solution as a new clause. This new clause ensures that another\nsolution is searched for, as it *excludes* the already found solution.\nHere is basically a pure Python implementation of ``itersolve`` in terms\nof ``solve``::\n\n def py_itersolve(clauses): # don't use this function!\n while True: # (it is only here to explain things)\n sol = pycosat.solve(clauses)\n if isinstance(sol, list):\n yield sol\n clauses.append([-x for x in sol])\n else: # no more solutions -- stop iteration\n return\n\nThis implementation has several problems. Firstly, it is quite slow as\n``pycosat.solve`` has to convert the list of clauses over and over and over\nagain. Secondly, after calling ``py_itersolve`` the list of clauses will\nbe modified. In pycosat, ``itersolve`` is implemented on the C level,\nmaking use of the picosat C interface (which makes it much, much faster\nthan the naive Python implementation above).\n",
"bugtrack_url": null,
"license": "MIT",
"summary": "bindings to picosat (a SAT solver)",
"version": "0.6.6",
"project_urls": {
"Homepage": "https://github.com/ContinuumIO/pycosat"
},
"split_keywords": [],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "5b81cf8ebf77fc4f06f680ad3ee43d0d01826f6d6054828f1cf3b42d944b82a1",
"md5": "403fa7f4fdad824682f81a643fa6fafc",
"sha256": "a376cfae20b16fcfbef24bf3c047a8a294c35032bb051fa98842c12bbab6f0ff"
},
"downloads": -1,
"filename": "pycosat-0.6.6.tar.gz",
"has_sig": false,
"md5_digest": "403fa7f4fdad824682f81a643fa6fafc",
"packagetype": "sdist",
"python_version": "source",
"requires_python": null,
"size": 71623,
"upload_time": "2023-10-03T15:45:48",
"upload_time_iso_8601": "2023-10-03T15:45:48.058830Z",
"url": "https://files.pythonhosted.org/packages/5b/81/cf8ebf77fc4f06f680ad3ee43d0d01826f6d6054828f1cf3b42d944b82a1/pycosat-0.6.6.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2023-10-03 15:45:48",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "ContinuumIO",
"github_project": "pycosat",
"travis_ci": false,
"coveralls": false,
"github_actions": true,
"lcname": "pycosat"
}
JSON
