The Role of a Skeptic Agent in Testing and Benchmarking of SAT Algorithms

摘要: This paper introduces a persistent agent called skeptic who supplies instances from well-deflned equivalence classes to test and benchmark SAT solvers. On such classes, met- rics as max/min ratio of time-to-solve should approach the value 1.0. Experiments suggested by on same class show (1) ratios for given solver can exhibit range 2 1000 beyond, (2) another may be several orders magnitude better, including signiflcantly lower average value. Both these factors point out that solvers not only much improved but also more reliably tested any improvement, intrinsic complexity or 'hardness' cannot gauged with current generation