GoRRiLA and Hard Reality
We call a theory problem a conjunction of theory literals and a theory solver any system that solves theory problems. For implementing efficient theory solvers one needs benchmark problems, and especially hard ones. Unfortunately, hard benchmarks for theory solvers are notoriously difficult to obtain. In this paper we present two tools: Hard Reality for generating theory problems from real-life problems with non-trivial boolean structure and GoRRiLA for generating random theory problems for linear arithmetic. Using GoRRiLA one can generate problems containing only a few variables, which however are difficult for all state-of-the-art solvers we tried. Such problems can be useful for debugging and evaluating solvers on small but hard problems. Using Hard Reality one can generate hard theory problems which are similar to problems found in real-life applications, for example, those taken from SMT-LIB .
Unable to display preview. Download preview PDF.
- 2.Barrett, C., Ranise, S., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library, SMT-LIB (2008), www.SMT-LIB.org
- 5.Brummayer, R., Biere, A.: Fuzzing and delta-debugging SMT solvers. In: 7th Intl. Workshop on on Satisfiability Modulo Theories, SMT 2009 (2009)Google Scholar
- 8.Hagen, G., Zucchelli, D., Tinelli, C.: SMT parser v3.0, http://combination.cs.uiowa.edu/smtlib/
- 9.Mitchell, D.G., Selman, B., Levesque, H.J.: Hard and easy distributions of SAT problems. In: AAAI 1992, pp. 459–465. AAAI Press/MIT Press (1992)Google Scholar