GoRRiLA and Hard Reality
GoRRiLA and Hard Reality
复制标题
GoRRiLA 和残酷的现实
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
A. Voronkov
中科院分区：
文献类型：
--
作者：
Konstantin Korovin;A. Voronkov
我们称理论问题为理论文字的连接，理论求解器为任何解决理论问题的系统。为了实现有效的理论求解器，需要基准问题，特别是困难的问题。不幸的是，理论求解器的硬基准是出了名的难以获得。在本文中，我们提出了两个工具：硬现实生成理论问题，从现实生活中的问题与非平凡的布尔结构和GoRRiLA生成随机理论问题的线性算术。使用GoRRiLA可以生成仅包含少数变量的问题，然而这对于我们尝试的所有最先进的求解器来说都是困难的。这些问题对于调试和评估小而难的问题的求解器很有用。使用硬现实可以生成硬理论问题，这些问题类似于现实应用中发现的问题，例如，来自SMT-LIB的问题[2]。
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 [2].