GSAT 中搜索的实证分析

我们描述了对 GSAT（命题可满足性近似程序）搜索的大规模研究。GSAT 对命题可满足性问题进行贪心爬坡，以满足子句的数量为目标。我们的实验提供了关于 GSAT 搜索的更完整图景，超越了以前的报告。我们详细描述了两个搜索阶段：快速爬坡随后是长期的平坡搜索。我们演示，当应用于随机生成的 3SAT 问题时，问题规模对平均满足子句数和平均分支率都有一个非常简单的标度。我们的结果使我们能够对爬坡阶段的长度、平均梯度以及平坡搜索中平均得分和平均分支率是否呈指数衰减作出详细的数值猜想。我们最终展示了这些结果如何用于指导未来的理论分析。这项工作提供了一个案例研究，说明计算机实验如何用于改进对算法理论属性的理解。