arminbiere
commented
4 years ago Well, restart intervals are hard to get right. We tried many things (some times exactly around 200 is OK, not more, not less):
Armin Biere, Andreas Fröhlich. Evaluating CDCL Restart Schemes. In Proc. Intl. Workshop on Pragmatics of SAT 2015 and 2018, http://fmv.jku.at/papers/BiereFroehlich-POS15.pdf
The current settings are default for the SAT competition or SAT race benchmarks. I bet that in certain situations some other values are better. However, maybe you are right. The '--sat' mode in Kissat still switches between 'stable' and 'focused' mode, while CaDiCaL only does 'stable' search. During 'stable' search, Kissat (as well as CaDiCaL) use pretty long reluctant doubling base intervals 'reluctanint' (1024 by default). I think this should be large enough (but I am happy to be proved wrong). However, the short 'restartint' of '1' (with 'log10 n' scaling) in Kissat for '--sat' mode might be bad (I will try to set this to something larger (say 50 - default for Glucose) and see whether this improves satisfiable instances .
in your CPAIOR Master class SAT video, around minute 40, you say a few words about restart intervalls. I was surprised about the small intervall and looked at the Kissat parameters, how to increase it. i played with various values for --restartint and the larger, the better. i run kissat with --sat --restartint=10000 . Runtimes decrease between 25% and 75%, which is quite good. The output says, that the default value 1 was replaced by 10000. i propose to use a (much) larger default value when --sat is given. the Luby-sequence is just too slow to grow to large values. Maybe it can be made adaptive to problem-size, that is number of variables or clauses ?
for those, who haven't seen the video: https://youtu.be/t3bJcU1aQJI