pysat
pysat copied to clipboard
pysathq
A toolkit for SAT-based prototyping in Python
Any time Ctrl+C is used to interrupt running code, it will throw a `KeyboardInterrupt`. But something is going on after doing SAT solving which causes it to not work all...
It would be great to have a way of pretty-printing formulas, by providing a dictionary between the variables (numerals) and application-specific name. This is easy to do for ordinary CNF...
Hi, Sorry, I don't know a lot about making Python packages. I wanted to add some tests for some code I was adding, but I wasn't sure how the tests...
Hello, is it possible to utilize more threads/cores when solving a SAT problem? Currently I'm using Glucose4. If not, is it even possible in principle?
Hello Alexey, as requested, I added a new [commit](https://github.com/marino-mrc/pysat/commit/f577fdddd21c02f12a4a19213b8a7c8c24078287) in my fork in order to implement a test for the get_proof() function. At the moment, I left some "print" call...
Thank you for PySAT! I went through the documentation of RC2 ([https://pysathq.github.io/docs/html/api/examples/rc2.html](https://pysathq.github.io/docs/html/api/examples/rc2.html)), and I could not find a way to extract the number of times that the underlying SAT oracle...
Thanks for creating this library, it's helped a lot in my work. Any chance you would consider integrating work such as: https://github.com/meelgroup/ApproxMC or http://fmv.jku.at/yalsat/ ? I feel like they would...
negate
The following has been puzzling me for days, until I saw a subtlety. I wanted to generate a not equals constraint. So I took the clauses generated by `CardEnc.equals`, and...
It would be nice if you had support for lexicographic comparison between two lists of literals, somewhat analogous to the support that you have for cardinality constraints.
I iteratively added clauses to an initially empty formula to be sat-solved with glucose3. For convenience, I translated between my 2D problem and the variable indices by multiplying the first...
