UNSAT theory has bad output

[haz]

When the CNF is unsatisfiable, and a nnf compilation is requested, then the output is largely uninformative and produces an error. There should be a check before attempting to output the nnf file to make sure at least one solution was found.

[symphorien]

It would be better to output a NNF with only node O 0 0 according to http://www.cril.univ-artois.fr/kc/d-DNNF-reasoner.html

This way one can get a valid NNF for all formulas, without special casing.