关于改进 PB 求解器中回跳层级的研究
人工智能
2021-07-29 v1
摘要
当前的 PB 求解器实现了许多受现代 SAT 求解器 CDCL 架构启发的技巧，以受益于其实际效率。然而，它们还需应对这样一个事实：该架构所利用的许多性质在考虑 PB 约束时不再成立。本文我们关注其中一项性质，即所谓的首个唯一蕴涵点（1-UIP）的最优性。尽管众所周知，在 SAT 求解器中学习冲突分析期间产生的首个断言子句可确保执行尽可能高的回跳，但我们表明在存在 PB 约束时并无此类保证。我们还引入并评估了不同的方法，旨在通过允许在到达 1-UIP 后继续分析来改进冲突分析期间确定的回跳层级。我们的实验表明，次优回跳在 PB 求解器中相当常见，尽管其对求解器的影响尚不清楚。
引用
@article{arxiv.2107.13085,
title = {On Improving the Backjump Level in PB Solvers},
author = {Romain Wallon},
journal= {arXiv preprint arXiv:2107.13085},
year = {2021}
}