Generating Satisfiable SAT Instances Using Random Subgraph Isomorphism
Generating Satisfiable SAT Instances Using Random Subgraph Isomorphism
复制标题
使用随机子图同构生成可满足的 SAT 实例
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
L. Olson
中科院分区：
文献类型：
--
作者：
Calin Anton;L. Olson
我们报告了使用随机子图同构模型的变体生成可满足的SAT实例的初步经验结果。实验表明，该模型呈现出易-难-易的经验硬度模式。对于完全求解器和不完全求解器，峰值处的实例的硬度似乎随着实例大小呈指数增加。由该模型生成的实例的难度似乎与具有空洞的拟群实例相当，这对于可满足性求解器来说是困难的。我们测试的少数最先进的SAT解算器在应用于这些实例时，彼此具有不同的性能。
We report preliminary empirical results on Generating Satisfiable SAT instances using a variation of the Random Subgraph Isomorphism model. The experiments show that the model exhibits an easy-hard-easy pattern of empirical hardness. For both complete and incomplete solvers the hardness of the instances at the peak seems to increase exponentially with the instance size. The hardness of the instances generated by the model appears to be comparable with that of Quasigroup with Holes instances, known to be hard for Satisfiability solvers. A handful of state of the art SAT solvers we tested have different performances with respect to each other, when applied to these instances.