pybind11-based binding of glucose SAT solver
Project description
pyglucose
pybind11-based binding of glucose SAT solver.
Installation
pip install git+https://github.com/msakai/glucose-pybind11/
Basic Usage
The pyglucose
module exports Solver
and Lit
.
A SAT problem can be solved as follows:
- Construct a solver instance using
solver = Solver()
. - Allocate variables using
var = solver.new_var()
. A variable is returned as integer value and can be converted toLit
byLit(var)
. A literallit
can be negated as~lit
. - Add clauses using
solver.add_clause(clause)
. A clause is represented asIterable[Lit]
. - Solve the problem using
solver.solve()
- If
solver.okay
property isTrue
then the problem isSATISFIABLE
, and satisfying assignment can be retrieved usingsolver.model
property. Otherwise, the problem isUNSATISFIABLE
.
License
Project details
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
pyglucose-0.0.1.tar.gz
(84.4 kB
view hashes)