The Configurable SAT Solver Challenge (CSSC)
The Configurable SAT Solver Challenge (CSSC)
复制标题
DOI：
10.1016/j.artint.2016.09.006
复制
发表时间：
2015-05
期刊：
影响因子：
--
通讯作者：
F. Hutter;M. Lindauer;A. Balint;Sam Bayless;H. Hoos;Kevin Leyton-Brown
中科院分区：
文献类型：
--
作者：
F. Hutter;M. Lindauer;A. Balint;Sam Bayless;H. Hoos;Kevin Leyton-Brown
众所周知，不同的求解策略对于不同类型的难组合问题很好地工作。因此，命题可满足性问题(SAT)的大多数求解器都会公开参数，这些参数允许将它们定制为特定的实例族。在国际SAT竞赛系列中，这些参数被忽略：对于给定赛道中的所有基准实例，解算器使用单一默认参数设置(由作者提供)运行。虽然此竞赛格式奖励具有强大默认设置的求解器，但它并不反映只关心某个特定应用程序的性能并花费一些时间调整此应用程序的求解器参数的从业者所面临的情况。新的可配置SAT求解器竞赛(CSSC)比较后一种设置中的求解器，根据在全自动配置步骤后获得的性能对每个求解器进行评分。本文更详细地描述了CSSC，并报告了到目前为止在CSSC 2013和2014两个实例中获得的结果。
It is well known that different solution strategies work well for different types of instances of hard combinatorial problems. As a consequence, most solvers for the propositional satisfiability problem (SAT) expose parameters that allow them to be customized to a particular family of instances. In the international SAT competition series, these parameters are ignored: solvers are run using a single default parameter setting (supplied by the authors) for all benchmark instances in a given track. While this competition format rewards solvers with robust default settings, it does not reflect the situation faced by a practitioner who only cares about performance on one particular application and can invest some time into tuning solver parameters for this application. The new Configurable SAT Solver Competition (CSSC) compares solvers in this latter setting, scoring each solver by the performance it achieved after a fully automated configuration step. This article describes the CSSC in more detail, and reports the results obtained in its two instantiations so far, CSSC 2013 and 2014.