Pycosat doesn't work with tuples

[asmeurer]

>>> pycosat.itersolve(((1,),))
Traceback (most recent call last):
  File "<ipython-input-9-d23eeeed2c7b>", line 1, in <module>
    pycosat.itersolve(((1,),))
TypeError: iterable or list expected

This is particularly annoying because it's often convenient to put clauses in a set, (and even have the clauses themselves be frozensets), so that duplicates are sorted out automatically.

[msoos]

"duplicates are sorted out automatically" --> actually, this sounds trivial, but it's a bit reinventing the wheel. Modern SAT solvers (e.g. precosat) will do better than that: shorter clauses will even subsume longer clauses. So 1 2 means that 1 2 -3 is a useless clause and precosat will find this and remove 1 2 -3 or any clause that contains 1 2 for that matter.

[asmeurer]

Sure, but my issue is that I want to store a bunch (a bunch) of clauses before sending them to the SAT solver. Storing duplicates means using a lot more memory.

In general, generating clauses can take longer and use more memory than the solving itself, so it really is something that you have to optimize on.

[msoos]

On a related point, you could use an API like this:

a = pycosat.solver
a.add_clause([1,2,3])
....
a.solve()

This would mean that pycosat is storing the clauses which is more efficient, as pycosat trims the clauses immediately of variables that have already been set: e.g. if [1] is passed, then [1,2,3] is not added at all and [-1, 2, 3] is added as [2,3]. Also, pycosat might also have the optimization where 2- and 3-long clauses are stored as "implicit" which is much better in terms of memory fragmentation & footprint. Furthermore, it automatically pre-propagates facts, so if [1] is passed and then [-1 2] is passed, then [2,3] is not added, since [1] is true and so [2] is propagated, so [2, 3] is automatically satisfied.

[asmeurer]

Does picosat have this functionality built in?

If not, what is the best kind of data structure to do this?

[msoos]

Picosat has implicit 2-long, but not 3-long I think. However, typically 2-longs are the most prevalent. It does have the auto-propagation and auto-literal-removal/auto-clause-removal inside. It probably doesn't have subsumption ([2,3] removes [2,3,4]), though -- you need precosat for that. To access these functionalities, just use the system you are using in pycosat.cpp -- adding literals and "0" at the end. Add the clauses this way, literal by literal, and don't store them in Python. There is no need, picosat will take care of storing them. With cryptominisat, I could make it even such that you can later access the clauses if you need them (but not change them inside the solver -- for that, you would instantiate another cryptominisat, take the clauses one-by-one from the original solver and feed them to the new one in a changed way). Also, all these solvers have the capability to add new clauses once the solving has finished with the solution being "SATISFIABLE". (or even soft "UNSATISFIABLE" if you use something called 'assumptions' which are mentioned in another github issue by Jordi Planes and chek for okay() in cryptominisat and something very similar in picosat for the UNSAT being "soft")

By the way, precosat should have exactly the same interface as picosat, so you can substitute one for the other and it's done. Nothing important needs to be changed, just the .cpp copied over and the #include fixed. Then it would be pyprecosat or something :)

[asmeurer]

I would just add precosat support in pycosat.

[msoos]

Sounds good. Also you might want to add the interface with the solver.add_clause([1, 2, 3]) as mentioned above, for speed. Precosat is cool but beware of lingeling: newer versions are under a restrictive license and it's probably not cheap for anything commercial.

[asmeurer]

@ilanschnell this is causing a serious slowdown in conda. Converting a set of 5434776 tuples to lists takes about 20 seconds.

If I understand #4 correctly this is already fixed, so a release just needs to be made.

[nmz787]

In the current PIP version this doesn't work :( and python is crashing when I pass my list of clauses... I guess it is too big

a = pycosat.solver
a.add_clause([1,2,3])

[msoos]

Well, I am not a developer of pycosat. I develop cryptominisat. I suggest you use pycryptominisat. It will work out of the box. Also, I promise to fix it asap. I have >300 closed issues on CryptoMiniSat: https://github.com/msoos/cryptominisat/issues and over 9000 commits.

[github-actions]

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!