Actin - 技术报告

布尔可满足性问题 (SAT) 可以通过 DPLL 算法的变体高效求解。对于工业级 SAT 问题，带有冲突分析相关动态决策启发式的 DPLL 算法已被证明特别高效，例如在 Chaff 中。在本工作中，我们利用遗传规划 (GP) 演化出了通过分析 CNF 来初始化求解器 MiniSAT v1.14 中变量活性值的算法，旨在减少搜索过程中的冲突总数和求解时间。我们通过使用随机数初始化来考察使用非零初始活性的效果。我们还研究了通过改进初始化来抵消重排 CNF 所带来的不利影响的可能性。找到的最佳结果（经进一步问题验证测试）被用于求解器 Actin，该求解器已提交至 SAT-Race 2006。