digama0
Behavior difference between -ss and -s
Hello,
We (@florianpollitt and I) are observing the following strange behavior on aws-c-common:aws_priority_queue_s_sift_either.cnf (SAT Comp 2022):
./target/release/frat-rs elab proof.frat -s file.cnf proof.lrat
elaborating...
takes forever (>10 hours, it gets stuck after printing "elaborating..."), while the version with superstrict take 45s on my machine:
./target/release/frat-rs elab proof.frat -ss file.cnf proof.lrat
elaborating...
parsing DIMACS...
trimming...
verifying...
VERIFIED
The super-strict proof generated by frat-rs is correct (according to cake_lpr).
The proof file was generated by an older version of CaDiCaL version (--lrat --lratfrat), but we provide all the files directly for easier reproduction (see here). It is a CaDiCaL version that is able to produce LRAT and FRAT proofs directly (FRAT with full chains).
Do you know what is happening here? Can you also explain what is the conceptual difference between super-strict and strict?
The spec of -s and -ss flags is given in the readme: in -s mode it will attempt to use the hint and give an error if the hint fails, but if there is no hint then it will use no-hint mode and do the DRAT thing to construct a hint on its own. In -ss mode the behavior is the same except that if you don't give a hint then it errors instead.
Based on that description, there is no reason why -s would be slow if -ss is fast and succeeds, since this implies that there are no missing proofs and hence no reason for -s and -ss to differ. I will investigate.
