search

crillab / d4

d4 Model Counter
GNU Lesser General Public License v3.0
14 stars 4 forks source link

d-DNNF output has undefined nodes when generating DRAT proof #8

Open vroland opened 3 years ago

vroland commented 3 years ago

Hello, I noticed that when requesting a DRAT proof with ./d4 -dDNNF ../cachet/Grid/75-10-10-q.cnf -out=test.nnf -drat=test.drat D4 seems to introduce new variables. But these new varaibles occur in the NNF only as children of OR nodes, but are not defined by a a/o/t/f line. Is there something missing from the NNF or are the nodes implicitly defined in the new format? If they are, which node type would they have? Regards, Valentin

vroland commented 3 years ago

It might be related to this issue https://github.com/crillab/d4/issues/1, since the certified output was not fixed, yet?