UNSAT theory has bad output

QuMuLab / dsharp

MIT License

16 stars 5 forks source link

UNSAT theory has bad output #1

Closed haz closed 3 years ago

haz commented 4 years ago

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 commented 3 years ago

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.