Code smell in DefaultSolver#fixContradiction

[rtaupe]

DefaultSolver#fixContradiction returns conflictAnalysisResult.learnedNoGood, which, however, must always be null. The caller, DefaultSolver#ingest, then checks if the returned value is not null (which can never be the case). Something is not right here!

[AntoniusW]

I cannot fully follow this analysis. Yes, the last return statement of DefaultSolver#fixContradiction could be return null; but this is not the only return statement, as it can earlier also return NoGood.UNSAT, which is a special indicator NoGood (i.e., the empty one). For some reason the caller DefaultSolver#ingest also checks for this special NoGood. This, however, seems to be the only use of NoGood.UNSAT.

Together with the information that DefaultSolver#fixContradiction either returns null or NoGood.UNSAT a clean way to resolve that seems to be: change the method to return a boolean and then use that in DefaultSolver#ingest.

[rtaupe]

Thank you, I have realized that part of my issue description is incorrect. The correct issue description is as follows:

DefaultSolver#fixContradiction returns conflictAnalysisResult.learnedNoGood, which, however, must always be null.

I like your proposal to change the method to return a boolean!

[AntoniusW]

While doing those changes I noticed other stuff that should be cleaned up, though. For example, it seems to not be fully documented that the Assignment#add does not record the nogood if it causes a conflict. Furthermore, when dealing with this situation the DefaultSolver seems to attempt resolving it in multiple different steps (with DefaultSolver#fixContradiction but also DefaultSolver#addAndBackjumpIfNecessary). I assume the underlying cause of those multiple methods is the fact that computing the decision level for backjumping is less efficient when out-of-order literals are involved, hence it is attempted to be postponed.

Furthermore, the NoGood.UNSAT member now also serves only as equality-checker for other empty NoGoods in DefaultSolver#ingest. Either checking directly for being the empty Nogood or tracing the origins of those and returning UNSAT instead would be cleaner.