熵与解密度对若干选定SAT启发式方法的影响
人工智能
2018-10-17 v1 计算机科学中的逻辑
摘要
在近期一篇文章[Oh'15]中，Oh考察了竞争性SAT求解器中各种关键启发式方法（例如删除策略、重启策略、衰减因子、数据库缩减）的影响。他的核心发现是，这些方法的预期成功取决于输入公式是否可满足。为了进一步研究这些发现，我们关注了可满足公式的两个性质：公式的熵（它近似于我们在变量赋值上的自由度）和解密度（即解的数量除以搜索空间）。我们发现这两者能更好地预测这些启发式方法的效果，并且具有小熵的可满足公式“表现”类似于不可满足公式。
引用
@article{arxiv.1706.05637,
title = {The impact of Entropy and Solution Density on selected SAT heuristics},
author = {Dor Cohen and Ofer Strichman},
journal= {arXiv preprint arXiv:1706.05637},
year = {2018}
}