Skip to content

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

@vroland

Description

@vroland

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

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions