search

conda / pycosat

Python bindings to picosat (a SAT solver)
MIT License
183 stars 36 forks source link

Adding hundreds of millions of clauses crashes solve #27

Closed nmz787 closed 2 years ago

nmz787 commented 8 years ago

I assumed this had something to do with passing too-large an array to the solve method at once... so I attempted to enhance the extension with a Solver class (I didn't change it's name from the Noddy template example though): https://github.com/ContinuumIO/pycosat/compare/master...nmz787:patch-1

but when I run this, at 234 million clauses the python.exe RAM usage is just under 4GB (~3.89 GB), and it crashes.

I am not sure what to do, but will keep thinking.

nmz787 commented 8 years ago

This will also crash pycosat as-is, without my modifications: pycosat.solve([[i for i in range(1,235000000)]])

confirmed by a friend who initially tried this on his pypi installed pycosat: pycosat.solve([[i for i in range(1,1000000000)]])

github-actions[bot] commented 2 years ago

Hi there, thank you for your contribution!

This issue has been automatically marked as stale because it has not had recent activity. It will be closed automatically if no further activity occurs.

If you would like this issue to remain open please:

  1. Verify that you can still reproduce the issue at hand
  2. Comment that the issue is still reproducible and include:
    • What OS and version you reproduced the issue on
    • What steps you followed to reproduce the issue

NOTE: If this issue was closed prematurely, please leave a comment.

Thanks!