arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 2006.01503cs.AI
收藏

SAT Heritage:由社区推动的工作,用于归档、构建和运行上千个SAT求解器

SAT Heritage: a community-driven effort for archiving, building and running more than thousand SAT solvers

CRIL;Artois University(阿尔图瓦大学);Univ. Bordeaux(波尔多大学);Bordeaux INP(波尔多国立理工学院);CNRS(法国国家科学研究中心)

Gilles Audemard, Loïc Paulevé, Laurent Simon

摘要:

SAT研究有着悠久的源代码和二进制版本的历史,这要归功于每年组织的竞赛。然而,由于每个竞争周期都有自己的一套规则和发布源代码和二进制文件的特殊方式,编译甚至运行任何求解器可能比看起来更难。此外,到目前为止,已经有超过一千个求解器发布,其中一些是在90年代初发布的。如果SAT社区想要存档并能够跟踪所有创造历史的求解器,它迫切需要部署一项重要的工作。我们建议发起一个社区驱动的努力,存档并允许轻松编译和运行迄今为止发布的所有SAT求解器。我们依靠最好的工具来归档和构建二进制文件(感谢Docker,GitHub和Zenodo),并为此提供一致且简单的方法。多亏了我们的工具,从源代码(或二进制文件)构建(或运行)求解器可以在一行中完成。

英文摘要:

SAT research has a long history of source code and binary releases, thanks to competitions organized every year. However, since every cycle of competitions has its own set of rules and an adhoc way of publishing source code and binaries, compiling or even running any solver may be harder than what it seems. Moreover, there has been more than a thousand solvers published so far, some of them released in the early 90's. If the SAT community wants to archive and be able to keep track of all the solvers that made its history, it urgently needs to deploy an important effort. We propose to initiate a community-driven effort to archive and to allow easy compilation and running of all SAT solvers that have been released so far. We rely on the best tools for archiving and building binaries (thanks to Docker, GitHub and Zenodo) and provide a consistent and easy way for this. Thanks to our tool, building (or running) a solver from its source (or from its binary) can be done in one line.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑