关于PB求解器中专用CDCL策略的研究
人工智能
2021-09-03 v1
摘要
当前基于原生PB约束的伪布尔（PB）求解器实现依赖于CDCL架构，该架构赋予了现代高效SAT求解器强大能力。具体而言，此类PB求解器不仅实现了（基于割平面的）冲突分析过程，还实现了对CDCL效率至关重要的组件补充策略，即分支启发式、学习约束删除与重启。然而，这些策略大多被PB求解器直接复用，而未考虑其所处理PB约束的特殊形式。本文中，我们提出并评估了使CDCL策略适应PB约束特性同时保持其在子句环境下行为的方法。我们在两种不同的求解器（即Sat4j（考虑三种配置）与RoundingSat）中实现了这些策略。实验表明，这些专用策略能够提升这些求解器在决策与优化问题上的性能，有时提升显著。
引用
@article{arxiv.2109.01013,
title = {On Dedicated CDCL Strategies for PB Solvers},
author = {Daniel Le Berre and Romain Wallon},
journal= {arXiv preprint arXiv:2109.01013},
year = {2021}
}