并行 SAT 求解器中的学习子句最小化
数据结构与算法
2019-08-06 v1 计算机科学中的逻辑
摘要
学习子句最小化 (LCM) 为现代 SAT 求解器带来了性能提升，尤其在求解困难 SAT 实例时。尽管 LCM 方法在串行求解器中取得成功，它们并未被广泛引入并行 SAT 求解器。在本文中，我们通过定义基于子句活化的多种 LCM 方法，比较它们在不同 SAT 求解器中的运行时间，并讨论性能增益与损失的原因，来探索 LCM 在并行 SAT 求解器中的潜力。结果表明 LCM 仅在一小部分 SAT 实例上提升并行 SAT 求解器性能。更普遍地应用 LCM 会降低性能。仅有特定的 LCM 方法能够改善并行 SAT 求解器的整体性能。
引用
@article{arxiv.1908.01624,
title = {Learned Clause Minimization in Parallel SAT Solvers},
author = {Marc Hartung and Florian Schintke},
journal= {arXiv preprint arXiv:1908.01624},
year = {2019}
}
备注
accepted at Pragmatics of SAT 2019