https://github.com/conda/pycosat

Python bindings to picosat (a SAT solver)

Science Score: 26.0%

This score indicates how likely this project is to be science-related based on various indicators:

○
CITATION.cff file
✓
codemeta.json file
Found codemeta.json file
✓
.zenodo.json file
Found .zenodo.json file
○
DOI references
○
Academic publication links
○
Committers with academic emails
○
Institutional organization owner
○
JOSS paper metadata
○
Scientific vocabulary similarity
Low similarity (9.3%) to scientific vocabulary

Keywords from Contributors

conda package-management numerical-methods notebook optimizing-compiler gtk qt tk wx tensor

Last synced: 10 months ago · JSON representation

Repository

Python bindings to picosat (a SAT solver)

Basic Info

Host: GitHub
Owner: conda
License: mit
Language: C
Default Branch: main
Homepage:
Size: 266 KB

Statistics

Stars: 191
Watchers: 69
Forks: 37
Open Issues: 5
Releases: 3

Created over 13 years ago · Last pushed over 1 year ago

Metadata Files

Readme Changelog License Code of conduct Authors

README.rst

===========================================
pycosat: bindings to picosat (a SAT solver)
===========================================

`PicoSAT `_ is a popular
`SAT `_ 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 `_
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).

Owner

Name: conda
Login: conda
Kind: organization

Website: https://conda.org
Twitter: condaproject
Repositories: 29
Profile: https://github.com/conda

conda is system-level, binary package and environment manager running on all major operating systems and platforms.

GitHub Events

Total

Issues event: 1
Watch event: 7
Issue comment event: 1
Push event: 7
Pull request review event: 7
Pull request event: 17
Fork event: 1

Last Year

Issues event: 1
Watch event: 7
Issue comment event: 1
Push event: 7
Pull request review event: 7
Pull request event: 17
Fork event: 1

Name	Email	Commits
Ilan Schnell	i**l@g**m	155
Conda Bot	1****t	47
Daniel Holth	d**h@a**m	12
Ken Odegard	k**d@a**m	9
William Schwartz	w**z@g**m	8
Ray Donnelly	m**d@g**m	2
Travis E. Oliphant	t**t@g**m	1
Ondřej Čertík	o**k@g**m	1
Bradley M. Froehle	b**e@g**m	1
Aaron Meurer	a**r@g**m	1

Issues and Pull Requests

Last synced: 11 months ago

All Time

Total issues: 33
Total pull requests: 79
Average time to close issues: almost 4 years
Average time to close pull requests: 3 months
Total issue authors: 21
Total pull request authors: 15
Average comments per issue: 2.09
Average comments per pull request: 0.67
Merged pull requests: 65
Bot issues: 0
Bot pull requests: 0

Past Year

Issues: 1
Pull requests: 19
Average time to close issues: N/A
Average time to close pull requests: 10 days
Issue authors: 1
Pull request authors: 2
Average comments per issue: 0.0
Average comments per pull request: 0.11
Merged pull requests: 14
Bot issues: 0
Bot pull requests: 0

View more stats

Top Authors

Issue Authors

asmeurer (6)
msoos (5)
wkschwartz (3)
dholth (2)
stonebig (1)
debugger22 (1)
danmoser (1)
duytrung (1)
opoplawski (1)
Geethree (1)
denfromufa (1)
physicalattraction (1)
bdice (1)
jordiplanes (1)
nmz787 (1)

Pull Request Authors

conda-bot (70)
dholth (8)
kenodegard (2)
bdice (2)
wkschwartz (2)
mbargull (1)
Digenis (1)
fornwall (1)
asmeurer (1)
certik (1)
bfroehle (1)
mingwandroid (1)
Kray-G (1)
ThePrez (1)
migueltorrescosta (1)

Top Labels

Issue Labels

locked (31) stale (16) stale::closed (14) type::bug (4) type::task (3) source::community (3) backlog (2) source::anaconda (2) type::feature (2) type::support (2) in-progress (2) sync::anaconda (1) pending::feedback (1) stale::recovered (1)

Pull Request Labels

cla-signed (69) locked (50) stale::recovered (3) stale (3) in-progress (2) stale::closed (2) type::feature (1) source::community (1)

Packages

Total packages: 3
Total downloads: unknown

Total dependent packages: 8
(may contain duplicates)
Total dependent repositories: 586
(may contain duplicates)
Total versions: 12
Total maintainers: 1

alpine-edge: py3-pycosat

Python bindings to picosat (a SAT solver)

Homepage: https://github.com/conda/pycosat
License: MIT
Latest release: 0.6.6-r2
published almost 2 years ago

Versions: 4
Dependent Packages: 0
Dependent Repositories: 0

Rankings

Dependent repos count: 0.0%

Average: 12.7%

Dependent packages count: 14.6%

Stargazers count: 18.1%

Forks count: 18.1%

Maintainers (1)

jakub@jirutka.cz

Last synced: 11 months ago

conda-forge.org: pycosat

PicoSAT is a popular SAT 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.

Homepage: https://github.com/conda/pycosat
License: MIT
Latest release: 0.6.4
published over 3 years ago

Versions: 4
Dependent Packages: 6
Dependent Repositories: 293

Rankings

Dependent repos count: 1.9%

Dependent packages count: 9.0%

Average: 16.7%

Forks count: 27.6%

Stargazers count: 28.2%

Last synced: 11 months ago

anaconda.org: pycosat

Homepage: https://github.com/conda/pycosat
License: MIT
Latest release: 0.6.6
published almost 3 years ago

Versions: 4
Dependent Packages: 2
Dependent Repositories: 293

Rankings

Dependent repos count: 10.7%

Dependent packages count: 20.4%

Average: 27.8%

Stargazers count: 40.0%

Forks count: 40.2%

Last synced: 11 months ago

Dependencies

.github/workflows/cla.yml actions

conda/actions/check-cla v22.9.0 composite

.github/workflows/issues.yml actions

actions-ecosystem/action-add-labels v1.1.0 composite
actions-ecosystem/action-remove-labels v1.3.0 composite

.github/workflows/labels.yml actions

EndBug/label-sync v2.3.0 composite
actions/checkout v3 composite
andstor/file-existence-action v1.0.1 composite

.github/workflows/lock.yml actions

dessant/lock-threads v2 composite

.github/workflows/project.yml actions

actions/add-to-project v0.3.0 composite

.github/workflows/stale.yml actions

actions/stale v4 composite
conda/actions/read-yaml v22.9.0 composite

setup.py pypi

https://github.com/conda/pycosat

Science Score: 26.0%

Keywords from Contributors

Repository

Basic Info

Statistics

Metadata Files

README.rst

Owner

GitHub Events

Total

Last Year

Committers

All Time

Past Year

Top Committers

Committer Domains (Top 20 + Academic)

Issues and Pull Requests

All Time

Past Year

Top Authors

Issue Authors

Pull Request Authors

Top Labels

Issue Labels

Pull Request Labels

Packages

alpine-edge: py3-pycosat

Rankings

Maintainers (1)

conda-forge.org: pycosat

Rankings

anaconda.org: pycosat

Rankings

Dependencies