Tjark Weber. In Tim King and Ruzica Piskac, editors, Proceedings of the 14th International Workshop on Satisfiability Modulo Theories, Coimbra, Portugal, July 1-2, 2016, volume 1617 of CEUR Workshop Proceedings, pages 31-40, July 2016.
Each year, the benchmarks for the SMT Competition are drawn from a known pool of benchmarks, the SMT Library. Competing solvers, rather than determine benchmark satisfiability from scratch, could thus cheat by simply looking up the correct answer for each benchmark in the library. To make this form of cheating more difficult, benchmarks in the SMT Competition are scrambled. We demonstrate that the current scrambling algorithm, which has been in use since 2011, is ineffective at obscuring the original benchmark. We propose an improved scrambling algorithm, and show that the problem of identifying the original benchmark under this improved algorithm is GI-complete.
@inproceedings{weber16scrambling,
author = {Tjark Weber},
title = {Scrambling and Descrambling {SMT-LIB} Benchmarks},
editor = {Tim King and Ruzica Piskac},
booktitle = {Proceedings of the 14th International Workshop on Satisfiability Modulo Theories, Coimbra, Portugal, July~1-2, 2016},
volume = {1617},
series = {CEUR Workshop Proceedings},
pages = {31--40},
month = jul,
year = {2016},
url = {http://ceur-ws.org/Vol-1617/paper3.pdf}
}
The software and evaluation data below accompany the paper. Please see the paper for further explanations and analysis. The original SMT-LIB benchmarks are available on StarExec.