The Role of a Skeptic Agent in Testing and Benchmarking of SAT Algorithms
F. Brglez, Xiao Yu Li, Matthias F. M. Stallmann · 2002
This paper introduces a persistent agent called skeptic who supplies instances from well-defined equivalence classes to test and benchmark SAT solvers. On such classes, metrics such as max/min ratio of time-to-solve should approach the value of 1.0. Experiments suggested by the skeptic on the instances of the same class show (1) the time-to-solve max/min ratios for a given solver can exhibit a range from 2 to 1000 and beyond, and (2) max/min ratios for another solver may be several orders of magnitude better, including a significantly lower time-to-solve average value. Both of these factors point out that (1) SAT solvers can not only be much improved but also more reliably tested for any such improvement, and (2) the intrinsic complexity or `hardness' of SAT instances cannot be gauged reliably with the current generation of SAT solvers.