SCSat: A Soft Constraint Guided SAT Solver
SCSat: A Soft Constraint Guided SAT Solver
复制标题
SCSat：软约束引导 SAT 求解器
DOI：
10.1007/978-3-642-39071-5_32
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Ryuzo Hasegawa
中科院分区：
文献类型：
--
作者：
Hiroshi Fujita;Miyuki Koshimura;Ryuzo Hasegawa
SCSat是一个SAT求解器，旨在使用软约束快速找到硬可满足实例的模型。软约束本身不一定最大限度地满足，如果它们太强而无法获得模型，则可以放松。适当地给定软约束可以在不丢失大量模型的情况下大大减少搜索空间，从而有助于更快地找到模型。通过这种方法，我们成功地得到了几个罕见的Ramsey图，这些图有助于将Ramsey数R（4，8）的已知最佳下界从56提高到58。
SCSat is a SAT solver aimed at quickly finding a model for hard satisfiable instances using soft constraints. Soft constraints themselves are not necessarily maximally satisfied and may be relaxed if they are too strong to obtain a model. Appropriately given soft constraints can reduce search space drastically without losing many models, thus help find a model faster. In this way, we have succeeded to obtain several rare Ramsey graphs which contribute to raise the known best lower bound for the Ramsey number R(4,8) from 56 to 58.