SAT Heritage：一项用于归档、构建并运行逾千个 SAT 求解器的社区驱动计划
人工智能
2020-06-03 v1
摘要
得益于每年举办的竞赛，SAT 研究在源代码与二进制发布方面有着悠久的历史。然而，由于每一轮竞赛都有其自身的规则以及发布源代码与二进制文件的临时方式，编译甚至运行任一求解器可能比看上去更为困难。此外，迄今为止已发布超过一千个求解器，其中一些早在 90 年代初便已发布。如果 SAT 社区希望归档并能够追踪所有在其历史上发挥作用的求解器，则迫切需要进行重要的努力。我们提议发起一项社区驱动的计划，以归档并支持对已发布的所有 SAT 求解器进行简易编译与运行。我们依托最佳的归档与二进制构建工具（借助 Docker、GitHub 与 Zenodo），为此提供一致且简便的方法。借助我们的工具，从其源代码（或二进制文件）构建（或运行）一个求解器可在一行命令内完成。
引用
@article{arxiv.2006.01503,
title = {SAT Heritage: a community-driven effort for archiving, building and running more than thousand SAT solvers},
author = {Gilles Audemard and Loïc Paulevé and Laurent Simon},
journal= {arXiv preprint arXiv:2006.01503},
year = {2020}
}