krobelus
commented
2 years ago Your proof looks suspicious. How exactly did you generate it? The reason I'm asking is that rate shows that your proof has "bad" unit deletions[^1]:
c reason deletions shrinking trail: 242but if I create a proof myself with kissat version 02cd69626a53e93e09286b1978ccb5d6bec58b8e and check it with rate, I get 0 "reason deletions shrinking trail". This is more what I expected, because kissat is a reimplementation of CaDiCaL, which always has 0 here. Repeated invocations of kissat give me exactly the same proof.
[^1]: These deletion instructions are ignored by drat-trim but not by rate, hence the different results. They normally indicate a bug in the solver since there is hardly ever a reason to delete such a unit clause.
It's possible but not very likely that there is a bug in rate. rate's
rejections are actually double checked: after we find a lemma that fails the
redundancy check, we compute an incorrectness certificate that gives hints as
to why the lemma does not have the given redundancy property (usually RAT).
Much like LRAT, this certificate is easy to validate. We validate it by
reading the formula + proof again, applying the proof until the failing step
and then fully checking that it does not have the redundancy property
(without doing any expensive/complex unit progagation).
The incorrectness certificate is checked automatically internally, but it can
be written out with the -S option and checked separately with sick-check
from the rate-sick-check crate.
DennisYurichev
Downloaded your 'rate' today...
Can't process these two files. PROOFs are generated by Kissat.
https://yurichev.com/tmp/rate-issues/
drat-trim and ACL2 can process them all.