incorrect count for UNSAT formula

[arminbiere]

For certain UNSAT formulas the solver still says there is one solution. The simplest UNSAT formula, where this happens is just the following two line DIMACS file
p cnf 0 0
0
but also if you have two conflicting unit clauses the same issue occurs, i.e.,
p cnf 1 2
1 0
-1 0
I think this is corner case though, where the formula becomes UNSAT during parsing, since for larger UNSAT formulas which really require search, I have not seen this issue.

[haz]

I've seen this in large problems too -- solution was to run unit prop and trivial checks on the theory before handing it off to sharpSAT.

You're right about it being in the preprocessing step, and I think in both your examples the solver ends up with the empty theory when it begins the search (which is assumed to be satisfiable because all of 0 clauses are satisfied).

It's a little more subtle in larger instances, as the trivial inconsistencies are parsed away, and a count is still returned.

[ZaydH]

For the opposing unit clause issue, there is a ToDo in the code around this:

//TODO Deal properly with the situation that opposing unit clauses are learned

I could issue a pull request to address the conflict unit clause case and the no variable case. Both should be easy to fix.