论文标题

SAT Heritage:以社区为导向的努力,用于归档,建造和运行超过成千上万的SAT求解器

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

论文作者

Audemard, Gilles, Paulevé, Loïc, Simon, Laurent

论文摘要

由于每年举办的比赛,SAT Research具有悠久的源代码和二进制版本的历史。但是,由于每个竞争的周期都有自己的一套规则,并且是发布源代码和二进制文件的信奉方式,因此编译甚至运行任何求解器可能都比看起来更难。此外,到目前为止,已经发布了一千多个求解器,其中一些在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.

扫码加入交流群

加入微信交流群

微信交流群二维码

扫码加入学术交流群,获取更多资源