I am looking for a solid reference (peer-reviewed publication) on the design and/or benchmarking of SAT solvers for random k-SAT ($4 \leq k \leq 8$) operating at satisfiability threshold.
The majority of published algorithmic works I know on SAT solving focuses on solvers running in polynomial time (at least empirically) up to a threshold ("algorithmic threshold") strictly smaller than the satisfiability threshold. On the other hand, the benchmarking of solvers in the regime between the algorithmic and satisfiability thresholds seems much less considered. In this region, SAT solvers are not expected to be efficient, i.e. to run in polynomial time. Still, assuming an exponential running time for simplicity, it makes sense to extract the scaling exponents and compare them between solvers.
Do you know of any published work taking this approach? If not, why do you think this has not be considered? For instance, is the reason that many solvers operate in the "thermodynamic" limit, hence would not work on the small instances you're restricted to when working at satisfiability threshold?
N.B.: I have personally already carried out experiments of the kind using widely available solvers, e.g. the ones from the PySAT library. For these solvers and the following parameters: $k = 8, \frac{m}{n} = 176.54$ (8-SAT at satisfiability threshold), the exponential scaling is neat and exponents can be easily extracted. However, to confirm whether this matches the state-of-the-art, and out of concern for not reinventing the wheel, a reference would be big plus.
