High-level Python interface over Mate Soos's
CryptoMiniSat
.
Copyright (C) 2019 Alexander Scheel
Licensed under the terms of the GPLv3.
GPLv3 | Building Instructions | API Documentation | Design | Version 0.4
The only dependencies are CryptoMiniSat, Python, and a working C++ compiler with C++20 support.
(For more complete documentation, refer to building.md
)
To build cmsh
, first build CryptoMiniSat with Gaussian Elimination support:
make cms
This will pull down the latest CryptoMiniSat and build it with Gaussian Elimination support. If you wish to build at a specific release version instead of latest HEAD, run:
cd msoos_cryptominisat && git checkout <REVISION> && cd ..
make distclean cms
Then, build cmsh
:
make clean all check
To install:
cd build/
pip3 install --user -e .
(For more complete documentation, refer to api.md
)
A single CryptoMiniSat SATSolver instance is exposed by a Model
:
import cmsh
m = cmsh.Model()
Variables can be created with Model.var()
:
a = m.var()
b = m.var()
Asserting a variable is true is done via Model.add_assert(...)
:
stmt = a ^ -b
m.add_assert(stmt)
Solutions can be seen by calling Model.solve()
and printing the
corresponding variables:
print(a, b)
print(m.solve())
print(a, b)
Variables can also be coerced to int
(to get the corresponding CNF
identifier) or bool
(to get the value after solving):
print(int(a))
print(bool(b))
Note that int(Variable)
can be less than zero if Variable is a negation of
another value:
c = m.var()
not_c = -c
print(int(c), int(not_c))
Logic also works with mixed types:
stmt2 = (c == True) | (c == -a)
m.add_assert(stmt2)
m.solve()
print(a, b, c)
There are also vectors!
vec = m.vec(4)
m.add_assert(vec == 3)
m.solve()
print(vec, int(vec))
Cool! \o/ Happy to have help. The core of cmsh
is done; mostly it is the
hard parts that remain (see the shortcomings section in the design document
for ideas). Nearly every project could use more tests and benchmarks so I'd
definitely merge those. I wouldn't be too adverse to build system improvements
either. Send a PR, file an issue, or shoot me an email if your interested, I'm
not particularly picky about these types of things or processes. I'd also take
constructive code review comments or feedback about using it in your own
projects.
Happy hacking!