文献阅读——A Problem Meta-Data Library for Research in SAT

Abstract:

Experimental data and benchmarks play a crucial role in developing new algorithms and implementations of SAT solvers. Besides comparing and evaluating solvers, they provide the basis for all kinds of experiments, for setting up hypothesis and for testing them. Currently – even though some initiatives for setting up benchmark databases have been undertaken, and the SAT Competitions provide a “standardized” collection of instances – it is hard to assemble benchmark sets with prescribed properties. Moreover, the origin of SAT instances is often not clear, and benchmark collections might contain duplicates. In this paper we suggest an approach to store meta-data information about SAT instances, and present an implementation that is capable of collecting, assessing and distributing benchmark meta-data.

译文：在本文中，我们提出了一种存储SAT实例元数据信息的方法，并提出了一种能够收集、评估和分发基准元数据的实现。

 The experiment is the core sources of knowledge in science. It is the vital source of data in a feedback loop between hypothesis formation and theory falsification. Algorithm engineers use experiments to evaluate their methods. Runtime experiments are often based on publicly available sets of benchmark problems. A set of characteristics or meta-data can be associated with each benchmark problem.

译文：可以将一组特征或元数据与每个基准测试问题相关联。

Benchmark meta-data can be used for benchmark classification and for differentiated analysis of algorithmic methods. It is very common that a certain algorithmic method or heuristic configuration works well on a specific type of problems but not so on others. Such correlations between the feature space of our benchmarks and the configuration space (or even fundamental algorithms) are of great interest. Disclosure and analysis of such correlations can lead to better hypotheses and thus more solid theories.

译文：基准元数据可用于基准分类和算法方法的差异化分析。

译文：很常见的是，某种算法方法或启发式配置在特定类型的问题上工作得很好，但在其他类型的问题上则不然。

译文：我们的基准测试的特征空间和配置空间(甚至是基本算法)之间的这种相关性是非常有趣的。揭示和分析这种相关性可以产生更好的假设，从而产生更可靠的理论。

Recent approaches in SAT solver development show that automatic feature extraction and algorithm selection or heuristic configuration through machine learning are crucial to state-ofthe-art solver performance [4, 3]. Increasing the number of automatically extracted problem features can improve predictions made by machine learning. But problem meta-data is not only useful for the training of machine models, it can also help improve the interpretation of experimental results. And if problem meta-data is used like this, there is no restriction to data that can be automatically and efficiently extracted from the problem.

译文：最近的SAT求解器开发方法表明，通过机器学习进行自动特征提取和算法选择或启发式配置对于最先进的求解器性能至关重要[4,3]。

译文：增加自动提取问题特征的数量可以改进机器学习的预测。但是问题元数据不仅对机器模型的训练有用，它还可以帮助改进对实验结果的解释。

Initializing the database with benchmarks from the agile set of SAT Competition 2017 showed that more than half of them are duplicates of one another. This could easily be detected, as only less than 50% unique hashes have been generated and the resolve command often returned multiple candidates for the same hash within the agile set of benchmark problems. There is no problem with the hash function, a quick check with the diff command showed that in fact the problems are identical.

译文：使用2017年敏捷SAT竞赛的基准初始化数据库显示，其中一半以上是彼此重复的。这可以很容易地检测到，因为只生成了不到50%的唯一哈希值，并且resolve命令经常在敏捷基准问题集中返回相同哈希值的多个候选值。

译文：哈希函数没有问题，使用diff命令快速检查后发现，实际上问题是相同的

In addition to present database selection, which requires physical exchange of files, new methods to setup a REST web-service for database-exposure are currently under development. Setup of a directory service where sources of benchmarks together with their meta-information can be publicly collected might be a future step of our work, or even a community effort.

译文：除了目前需要物理交换文件的数据库选择之外，目前正在开发为数据库公开设置REST web服务的新方法。

译文：建立一个目录服务，可以公开收集基准源代码及其元信息，这可能是我们未来的工作步骤，甚至是社区的努力。

Functions to import and merge tables from another database are currently under development. Future work includes functionality to automatically extract meta-information from benchmark files. This could include meta-data from specially formatted comments, but also the automatic execution of specialized algorithms.

译文：未来的工作包括从基准文件中自动提取元信息的功能。这可能包括来自特殊格式注释的元数据，也可能包括专门算法的自动执行。

Currently, only the most basic ideas of decentralized meta-data collection are implemented. The implementation of specific use-cases on top of basic meta-data collection and distribution is considered future work. Such use-cases include automatic detection of correlations between solver performance and other meta-data and automatic solver comparison.

译文：目前，只实现了分散元数据收集的最基本思想。在基本元数据收集和分发的基础上实现特定的用例被认为是未来的工作。

译文：这些用例包括自动检测求解器性能与其他元数据之间的相关性，以及自动求解器比较。

参考文献：

References

[1] GBD public repository. https://github.com/Udopia/gbd. Accessed: 2019-01-15.

[2] SAT competitions. http://satcompetition.org/. Accessed: 2017-04-17.

[3] Tomás Balyo, Armin Biere, Markus Iser, and Carsten Sinz. SAT Race 2015. Artif. Intell., 241:45–65, 2016.

[4] Bernd Bischl, Pascal Kerschke, Lars Kotthoff, Marius Thomas Lindauer, Yuri Malitsky, Alexandre Fréchette, Holger H. Hoos, Frank Hutter, Kevin Leyton-Brown, Kevin Tierney, and Joaquin Vanschoren. Aslib: A benchmark library for algorithm selection. Artif. Intell., 237:41–58, 2016. 

[5] Holger Hoos and Thomas Stützle. Satlib. http://www.cs.ubc.ca/~hoos/SATLIB/index-ubc.html. Accessed: 2017-04-17.

[6] Holger Hoos and Thomas Stützle. SATLIB: An online resource for research on SAT. 2000.