可满足性的早期征兆
计算机科学中的逻辑
2016-12-16 v1
摘要
本短文考虑命题子句集（SAT 实例）的可满足性检验。它表明，子句的“单极集”（unipolar sets）在求解 SAT 问题的过程中所有子句均被满足之前，提供了 SAT 实例可满足性的一个“早期征兆”。在此征兆处，处理可通过“单极集终止”（UST）来结束，从而早于通常由 SAT 求解器完成的时间（表 1）。对 SAT 竞赛中使用的基准 SAT 实例的分析表明，UST 能够加速源自许多现实世界问题的 SAT 实例的求解。UST 的效率随着被检验 SAT 集的“偏斜度”而增加，即该集中否定文字与未否定文字的概率之差。许多现实世界问题因其语义而具有偏斜性（表 2）。UST 的效率可通过揭示 SAT 集的“隐藏偏斜度”来提高（表 3）。
引用
@article{arxiv.1612.05019,
title = {An early sign of satisfiability},
author = {Eliezer L. Lozinskii},
journal= {arXiv preprint arXiv:1612.05019},
year = {2016}
}