Weird itersolve behaviour

[msoos]

The return value of itersolve is very weird:

>>> from pycosat import itersolve
>>> list(itersolve([]))
[[]]
>>> list(itersolve([[]]))
[]

One of the problems is solveable, but has the only solution to it is the empty solution. The other one is UNSAT. It's weird as hell, though.

[asmeurer]

Why is one unsatisfiable?

[msoos]

The second one contains the empty clause: []. The empty clause ("0\n" in CNF) is always unsatisfiable.

[asmeurer]

Ah, I get it. One is and(), i.e., true, and the other is and(or()), i.e. and(false) = false.

[asmeurer]

So the result of itersolve([[]]) is wrong. I think [[]] is correct as the empty solution, since that would be or(and()) = true. I guess technically [] could mean unsatisfiable, since it's or() = false. That would be better than returning a string IMO (#14).

[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!