This is a pre-production deployment of Warehouse, however changes made here WILL affect the production instance of PyPI.
Latest Version Dependencies status unknown Test status unknown Test coverage unknown
Project Description

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-957.tar.gz).


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)


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 (x1 or not x5 or x4). Note that the variable x2 is not used in any of the clauses, which means that for each solution with x2 = True, we must also have a solution with x2 = 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 ith 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: x1 = x5 = True, x2 = x3 = x4 = 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)))

In this example, there are a total of 18 possible solutions, which had to be an even number because x2 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

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).

Release History

Release History


This version

History Node

TODO: Figure out how to actually get changelog content.

Changelog content for this version goes here.

Donec et mollis dolor. Praesent et diam eget libero egestas mattis sit amet vitae augue. Nam tincidunt congue enim, ut porta lorem lacinia consectetur. Donec ut libero sed arcu vehicula ultricies a non tortor. Lorem ipsum dolor sit amet, consectetur adipiscing elit.

Show More

Download Files

Download Files

TODO: Brief introduction on what you do with files - including link to relevant help section.

File Name & Checksum SHA256 Checksum Help Version File Type Upload Date
pycosat-0.6.1-cp27-none-win32.whl (40.4 kB) Copy SHA256 Checksum SHA256 2.7 Wheel Sep 3, 2015
pycosat-0.6.1-cp27-none-win_amd64.whl (47.0 kB) Copy SHA256 Checksum SHA256 2.7 Wheel Sep 3, 2015
pycosat-0.6.1-cp33-none-win32.whl (41.9 kB) Copy SHA256 Checksum SHA256 3.3 Wheel Sep 3, 2015
pycosat-0.6.1-cp33-none-win_amd64.whl (48.6 kB) Copy SHA256 Checksum SHA256 3.3 Wheel Sep 3, 2015
pycosat-0.6.1-cp34-none-win32.whl (41.9 kB) Copy SHA256 Checksum SHA256 3.4 Wheel Sep 3, 2015
pycosat-0.6.1-cp34-none-win_amd64.whl (48.6 kB) Copy SHA256 Checksum SHA256 3.4 Wheel Sep 3, 2015
pycosat-0.6.1.tar.gz (59.3 kB) Copy SHA256 Checksum SHA256 Source Aug 20, 2015

Supported By

WebFaction WebFaction Technical Writing Elastic Elastic Search Pingdom Pingdom Monitoring Dyn Dyn DNS Sentry Sentry Error Logging CloudAMQP CloudAMQP RabbitMQ Heroku Heroku PaaS Kabu Creative Kabu Creative UX & Design Fastly Fastly CDN DigiCert DigiCert EV Certificate Rackspace Rackspace Cloud Servers DreamHost DreamHost Log Hosting