search

cjdrake / pyeda

Python EDA
BSD 2-Clause "Simplified" License
304 stars 54 forks source link

Adding solver class with add_clause(clause) and solve() methods for picosat interface would be nice #135

Closed nmz787 closed 7 years ago

nmz787 commented 8 years ago

I have attempted to do this here for pycosat, but it is not solving some kind of memory issue with lots of clauses. I will try to use your tool now, but it seems like being able to pass data from Python to C would be beneficial. https://github.com/ContinuumIO/pycosat/compare/master...nmz787:patch-1

cjdrake commented 8 years ago

Could you please provide more detail? We might be able to solve your problem w/o meddling with the CPython API.

Lately I have been putting more energy into the boolexpr library. It uses MiniSAT 4.5.3, and might give you better results.

nmz787 commented 8 years ago

Just that I have a few hundred million clauses right now (going to work on optimizing the clause generation tomorrow)... so it would be nice to create a solver object, then add clauses to it as I generate them, and then finally call solve on the solver. This way I don't have to append them to a huge Python list, finally passing the list to the pyeda picosat interface. Oh, and BTW, it DID work to solve the problem I threw at it. So for now it actually seems like my clause generation needs serious optimization. If you feel like mucking in the C++ to make a class object with the add_clause and solve methods, well feel free... but at this point it isn't necessarily breaking my path forward testing this out. Thanks!

cjdrake commented 7 years ago

Not going to fix this one. Feel free to look into using minisat/glucose C++ APIs.