Skip to main content

Bindings to CryptoMiniSat, an advanced SAT solver

Project description

pycryptosat SAT solver

This directory provides Python bindings to CryptoMiniSat on the C++ level, i.e. when importing pycryptosat, the CryptoMiniSat solver becomes part of the Python process itself.

Installing

pip install pycryptosat

Compiling

If you don't want to use the pip package, you can compile it locally.

You must first build and install CryptoMiniSat using the instructions in the root README.

Then you can compile the python package from the root directory (the one with setup.py) as:

apt-get install python-dev
python -m build

To help with debug, you can also:

python setup.py bdist_wheel

Usage

The pycryptosat module has one object, Solver that has two functions solve and add_clause.

The funcion add_clause() takes an iterable list of literals such as [1, 2] which represents the truth 1 or 2 = True. For example, add_clause([1]) sets variable 1 to True.

The function solve() solves the system of equations that have been added with add_clause():

>>> from pycryptosat import Solver
>>> s = Solver()
>>> s.add_clause([1, 2])
>>> sat, solution = s.solve()
>>> print sat
True
>>> print solution
(None, True, True)

The return value is a tuple. First part of the tuple indicates whether the problem is satisfiable. In this case, it's True, i.e. satisfiable. The second part is a tuple contains the solution, preceded by None, so you can index into it with the variable number. E.g. solution[1] returns the value for variable 1.

The solve() method optionally takes an argument assumptions that allows the user to set values to specific variables in the solver in a temporary fashion. This means that in case the problem is satisfiable but e.g it's unsatisfiable if variable 2 is FALSE, then solve([-2]) will return UNSAT. However, a subsequent call to solve() will still return a solution. If instead of an assumption add_clause() would have been used, subsequent solve() calls would have returned unsatisfiable.

Solver takes the following keyword arguments:

  • time_limit: the time limit (integer)
  • confl_limit: the propagation limit (integer)
  • verbose: the verbosity level (integer)

Both time_limit and confl_limit set a budget to the solver. The former is based on time elapsed while the former is based on number of conflicts met during search. If the solver runs out of budget, it returns with (None, None). If both limits are used, the solver will terminate whenever one of the limits are hit (whichever first). Warning: Results from time_limit may differ from run to run, depending on compute load, etc. Use confl_limit for more reproducible runs.

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 pycryptosat
>>> solver = pycryptosat.Solver()
>>> solver.add_clause([1, -5, 4])
>>> solver.add_clause([-1, 5, 3, 4])
>>> solver.add_clause([-3, -4])
>>> solver.solve()
(True, (None, True, False, False, True, True))

This solution translates to: x\ :sub:1 = x\ :sub:4 = x\ :sub:5 = True, x\ :sub:2 = x\ :sub:3 = False

Special options (e.g. LARGEMEM, etc)

In case you need to e.g. have LARGEMEM, you must modify setup.py and add '-DLARGE_OFFSETS' to extra_compile_args. Similarly for other options.

Project details


Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distributions

No source distribution files available for this release.See tutorial on generating distribution archives.

Built Distributions

pycryptosat-5.11.23-pp310-pypy310_pp73-manylinux_2_17_x86_64.manylinux2014_x86_64.whl (687.4 kB view details)

Uploaded PyPy manylinux: glibc 2.17+ x86-64

pycryptosat-5.11.23-pp39-pypy39_pp73-manylinux_2_17_x86_64.manylinux2014_x86_64.whl (687.4 kB view details)

Uploaded PyPy manylinux: glibc 2.17+ x86-64

pycryptosat-5.11.23-pp38-pypy38_pp73-manylinux_2_17_x86_64.manylinux2014_x86_64.whl (687.4 kB view details)

Uploaded PyPy manylinux: glibc 2.17+ x86-64

pycryptosat-5.11.23-pp37-pypy37_pp73-manylinux_2_17_x86_64.manylinux2014_x86_64.whl (700.8 kB view details)

Uploaded PyPy manylinux: glibc 2.17+ x86-64

pycryptosat-5.11.23-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl (9.0 MB view details)

Uploaded CPython 3.12 manylinux: glibc 2.17+ x86-64

pycryptosat-5.11.23-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl (9.0 MB view details)

Uploaded CPython 3.11 manylinux: glibc 2.17+ x86-64

pycryptosat-5.11.23-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl (9.0 MB view details)

Uploaded CPython 3.10 manylinux: glibc 2.17+ x86-64

pycryptosat-5.11.23-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl (9.0 MB view details)

Uploaded CPython 3.9 manylinux: glibc 2.17+ x86-64

pycryptosat-5.11.23-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl (9.0 MB view details)

Uploaded CPython 3.8 manylinux: glibc 2.17+ x86-64

pycryptosat-5.11.23-cp37-cp37m-manylinux_2_17_x86_64.manylinux2014_x86_64.whl (9.0 MB view details)

Uploaded CPython 3.7m manylinux: glibc 2.17+ x86-64

File details

Details for the file pycryptosat-5.11.23-pp310-pypy310_pp73-manylinux_2_17_x86_64.manylinux2014_x86_64.whl.

File metadata

File hashes

Hashes for pycryptosat-5.11.23-pp310-pypy310_pp73-manylinux_2_17_x86_64.manylinux2014_x86_64.whl
Algorithm Hash digest
SHA256 339d34aacca0c95f7eab671ace0559a8f438ec292c0d7774b9e071c5411cdd01
MD5 a89308df347506d23f262a340abda5c4
BLAKE2b-256 091ac92ea4b507a7d9f99e133d89803ddfba3865533eb025982136e05371e2db

See more details on using hashes here.

File details

Details for the file pycryptosat-5.11.23-pp39-pypy39_pp73-manylinux_2_17_x86_64.manylinux2014_x86_64.whl.

File metadata

File hashes

Hashes for pycryptosat-5.11.23-pp39-pypy39_pp73-manylinux_2_17_x86_64.manylinux2014_x86_64.whl
Algorithm Hash digest
SHA256 f242a4cc4e423c8db3fb5b1350867756f3ed4f194ac674246270457b17f5fc1c
MD5 cf4094d8d487dd46e07d03cfa9ad0134
BLAKE2b-256 2e48efd434877277e077913c47bfa88f808ab103bc9b083152164b03b1afcbc4

See more details on using hashes here.

File details

Details for the file pycryptosat-5.11.23-pp38-pypy38_pp73-manylinux_2_17_x86_64.manylinux2014_x86_64.whl.

File metadata

File hashes

Hashes for pycryptosat-5.11.23-pp38-pypy38_pp73-manylinux_2_17_x86_64.manylinux2014_x86_64.whl
Algorithm Hash digest
SHA256 7380f22f43e39916e538ff1e49c7ae03b50e0e11c22ea69a6642b236c4e15d50
MD5 cf6df6ddf71782119638b6b270f13891
BLAKE2b-256 1437cf51921ef0fc440ac2359d114defeab7bad2442010f6ec83fa37974068f9

See more details on using hashes here.

File details

Details for the file pycryptosat-5.11.23-pp37-pypy37_pp73-manylinux_2_17_x86_64.manylinux2014_x86_64.whl.

File metadata

File hashes

Hashes for pycryptosat-5.11.23-pp37-pypy37_pp73-manylinux_2_17_x86_64.manylinux2014_x86_64.whl
Algorithm Hash digest
SHA256 5d0f20f750fb3031fba46687a142e878d3f87a13276660a61d837c9f25ae47d7
MD5 ddc7a34c4805bdad01e9070e85ddfca8
BLAKE2b-256 5600b50c2041f9520dd3d353c6e7fcb51e31f5d510bd6e9aa903491c6da8a6db

See more details on using hashes here.

File details

Details for the file pycryptosat-5.11.23-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl.

File metadata

File hashes

Hashes for pycryptosat-5.11.23-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl
Algorithm Hash digest
SHA256 a145543e837712af95733a5f6c1bcd038351a4b96322b8cda622b7af73e2d10a
MD5 1f5bb1f50053f0ceab35c2827a57a0ef
BLAKE2b-256 ee19c5c4d84201ac4fa9b86d074d578c3d1b8259faecbc45dbe8ec8ffbf8a285

See more details on using hashes here.

File details

Details for the file pycryptosat-5.11.23-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl.

File metadata

File hashes

Hashes for pycryptosat-5.11.23-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl
Algorithm Hash digest
SHA256 08c3dd63ca49346a71c3824a7f0e68e7a69399b6c5bacc23b36df4beca0e1381
MD5 10ca5a1b9b5c13651e335ae4db98af60
BLAKE2b-256 310bd04a5f762443fc60d75093cb349abaa80ce7475f352099bd5c2b4148deb5

See more details on using hashes here.

File details

Details for the file pycryptosat-5.11.23-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl.

File metadata

File hashes

Hashes for pycryptosat-5.11.23-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl
Algorithm Hash digest
SHA256 093243014d74c1a1f070f2a7dc6ffa215d2dd769f66531430c105faba876908b
MD5 fd960edbeb25246df611b8f57d134446
BLAKE2b-256 ed8d6ac767410d9610233b6fe257f009af74938357982eb0dd44e3f3f1bd81bd

See more details on using hashes here.

File details

Details for the file pycryptosat-5.11.23-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl.

File metadata

File hashes

Hashes for pycryptosat-5.11.23-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl
Algorithm Hash digest
SHA256 33154987c1d1dcf0e041a91c091c7b33d39d6769a6e83ecd833429d47d0e4c19
MD5 8ff71654b60a8660c3632be060fbc45e
BLAKE2b-256 6e3af7986b4cc60503e4388bbc7adf23a1404d05c9c536e837ff6d7fc61c7f0c

See more details on using hashes here.

File details

Details for the file pycryptosat-5.11.23-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl.

File metadata

File hashes

Hashes for pycryptosat-5.11.23-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl
Algorithm Hash digest
SHA256 c8b409e4f2c0386f434d0a21edb2400500d2e0f4bc72edb394c4f786d74c19d6
MD5 2e1ea9d99c2ccb99d9bceed6b835581e
BLAKE2b-256 78f37b112bbb06eb649bc4fe374cddbf281c9b1724bff53db212b7a9a67704f7

See more details on using hashes here.

File details

Details for the file pycryptosat-5.11.23-cp37-cp37m-manylinux_2_17_x86_64.manylinux2014_x86_64.whl.

File metadata

File hashes

Hashes for pycryptosat-5.11.23-cp37-cp37m-manylinux_2_17_x86_64.manylinux2014_x86_64.whl
Algorithm Hash digest
SHA256 3bff4c295bf6c1ba1c1edf71083f8eb17f7dfc896a5c599a4cbade77aff1edbf
MD5 c67dbfef68b34948251e709222494237
BLAKE2b-256 15eb963ce695eef1bdf65c865cc8fe5f24713139c3eeb6cd372bb9ee241603ce

See more details on using hashes here.

Supported by

AWS AWS Cloud computing and Security Sponsor Datadog Datadog Monitoring Fastly Fastly CDN Google Google Download Analytics Microsoft Microsoft PSF Sponsor Pingdom Pingdom Monitoring Sentry Sentry Error logging StatusPage StatusPage Status page