Question about cpog output for UNSAT instances

[latower]

Dear developers,

Mate Soos and I are working on a fuzzer for model counters. We have implemented support for running cpog to obtain verified model counts of the generated instances. For satisfiable instances, this works very well: cpog explicitly reports a verified count, and explicitly states that the proof is successful. However, cpog's output for unsatisfiable instances confuses me, and I was hoping that you could help me interpret cpog's output for these instances?

Expected behaviour: Since cpog's README states that it is a "certifying results from the D4 knowledge compiler", I would expect unsatisfiable instances to be verified as unsatisfiable.

Observed behaviour: For unsatisfiable instances, I see cpog generate the output:

PROOF FAILED
proof done but some clause is neither the asserted root nor a POG definition

I am attaching two example CNFs along with the outputs I get from running cpog on them. Both instances are unsatisfiable according to cadical, both produce the above output, but they differ in their intermediate output.

[EDIT: I forgot to mention that I created symbolic links to the different binaries to make coding a bit easier. This is reflected in my commands below.]

The first example is ex002.cnf:

$ ./d4 -dDNNF ex002.cnf -out=ex002.nnf >> ex002.output 2>&1
$ ./cpog-gen -v 2 -L ex002.log ex002.cnf ex002.nnf ex002.cpog  >> ex002.output 2>&1
$ ./cpog_checker -c ex002.cnf ex002.cpog >> ex002.output 2>&1
$ cat ex002.output
[...]
GEN: Time = 0.00.  Read input file with 139 variables and 475 clauses
c Read D4 NNF file with 3 nodes (2 explicit) and 1 edges
c Compressing POG with 3 nodes (3 accessible from root) and root literal 140
c Compressed POG has 1 nodes, root literal -1, and 0 defining clauses
c GEN: Time = 0.00.  Generated POG representation
c Time = 0.00.  Justifications of 1 nodes, including root, completed.  89 total clauses
c GEN: Time = 0.01.  Deleted asserted clauses
c ERROR: Unknown POG type 1 for node N140
c WARNING: Execution incomplete.  Here's the results so far:
c GEN: Formula
c GEN:    input variables: 139
c GEN:    input clauses  : 475
[...]
c WARNING: Results not valid
Parsing CNF..
done.
Parsing CPOG..
done.
Checking proof..
PROOF FAILED
proof done but some clause is neither the asserted root nor a POG definition

(full output in attachment).

The second example is ex047.cnf:

$ ./d4 -dDNNF ex047.cnf -out=ex047.nnf >> ex047.output 2>&1
$ ./cpog-gen -v 2 -L ex047.log ex047.cnf ex047.nnf ex047.cpog >> ex047.output 2>&1
$ ./cpog_checker -c ex047.cnf ex047.cpog >> ex047.output 2>&1
$ cat ex047.output 
[...]
c GEN: Time = 0.00.  Read input file with 283 variables and 974 clauses
c Read D4 NNF file with 3 nodes (2 explicit) and 1 edges
c Compressing POG with 3 nodes (3 accessible from root) and root literal 284
c Compressed POG has 1 nodes, root literal -1, and 0 defining clauses
c GEN: Time = 0.00.  Generated POG representation
c WARNING: Execution of command 'cadical --unsat -q --no-binary reduction-1000001.cnf -' shows formula satisfiable
Validation of literal -1 failed
c WARNING: Failed to justify root literal -1
[...]
Parsing CNF..
done.
Parsing CPOG..
done.
Checking proof..
PROOF FAILED
proof done but some clause is neither the asserted root nor a POG definition

(full output in attachment).

It seems that both instances are unsatisfiable, but that they trigger slightly different outputs from cpog. I am now wondering how I should interpret these outputs? Are they an indication of verified unsatisfiability? If not, is there a mistake in how I use cpog? Or isn't cpog intended to verify unsatisfiability and should I use, e.g., cadical to obtain a proof of unsatisfiability? Am I missing something?

I would really appreciate your help in this matter!

Kind regards,
Anna Latour

ex002.cnf.txt
ex002.output.txt
ex047.cnf.txt
ex047.output.txt

[Vtec234]

Hi @latower! Thank you for your interest, and sorry for the super slow response.

Or isn't cpog intended to verify unsatisfiability and should I use, e.g., cadical to obtain a proof of unsatisfiability?

This is the right answer. cpog is only intended to verify nontrivial model counts. We have recently made changes to handle tautological formulas correctly, but for unsatisfiable formulas, standard proof formats such as DRAT remain a better fit. With the new changes, cpog-gen should print out a better warning:

$ ./src/cpog-gen -v 2 -L ex002.log ex002.cnf ex002.nnf ex002.cpog  
c GEN: Program options
c GEN:   Multi-literal:   yes
c GEN:   Use lemmas:      yes
c GEN:   Delete files:    yes
c GEN:   One-sided:       no
c GEN:   Monolithic mode: no
c GEN:   DRAT threshold:  1000
c GEN:   Clause limit:    2147483647
c GEN:   BCP limit:       1
c GEN: Time = 0.00.  Read input file with 139 variables and 475 clauses
c Read D4 NNF file with 3 nodes (2 explicit) and 1 edges
c Compressing POG with 3 nodes (3 accessible from root) and root literal 140
c Compiled formula unsatisfiable.  Cannot verify
c WARNING: Error reading D4 NNF file.  Aborting proof generation