`pumpkin-proof-processor` error on non-continguous identifiers

[Dekker1]

With the attached scaffold proof generated by Huub, the proof processor crashes. Maarten indicated that the problem is that the identifiers are non-continguous.

jobshop_trace.zip

[maartenflippo]

I looked into this just now and believe I have found the problem, which is actually not what I initially thought.

Originally, I thought the problem was that the constraint IDs in the scaffold were not contiguous. However, it turns out the processor only requires them to be monotonically increasing. So gaps in the IDs are fine and not a problem.

However, a problem is that we expect the $n$ FZN constraints to have IDs from $1$ to $n$. What I think is happening here, however, is that the deduction IDs are less than $n$, which does not work for the processor (or checker, for that matter). Ideally, I do not want to have to support arbitrary IDs for model constraints.

If @Dekker1 can confirm this is what is happening, then I think this issue can be closed. It is not a fault in the processor; there is a mismatch between how the DRCP proof works in the abstract and how Huub implements it. Either Huub has to be updated, or we need to somehow support this in the system.

[Dekker1]

Just making sure I understand. The problem with the attached is that my n <id> <lit>... lines have <id> numbers that conflict with the constraint numbers? (They are the clause numbers that CaDiCaL gives them). Instead, you would want the first n to have id 725 (since there are 724) constraints in the FlatZinc file.

This still leaves me with some questions:

• Do those n lines then have to be consecutive?
• Does this issue mostly stem from the larger (complete) format? We never actually use any constraint identifiers in the proof-skeleton, so the identifiers are mostly meaningless, right?

[maartenflippo]

Just making sure I understand. The problem with the attached is that my n ... lines have numbers that conflict with the constraint numbers? (They are the clause numbers that CaDiCaL gives them). Instead, you would want the first n to have id 725 (since there are 724) constraints in the FlatZinc file.

Correct.

Do those n lines then have to be consecutive?

No, as long as they are increasing (which I expect is the case for you). Gaps are supported.

Does this issue mostly stem from the larger (complete) format? We never actually use any constraint identifiers in the proof-skeleton, so the identifiers are mostly meaningless, right?

Correct. Perhaps we should really have a dedicated skeleton format that does not include IDs. However, if you would want to log an entire proof, this problem would re-appear.