关于PB求解器的弱化策略
On Weakening Strategies for PB Solvers
摘要：
当前的伪布尔解算器实现切割平面证明系统的不同变体，以在冲突分析期间推断新的约束。这些变体之一是广义分辨率，它允许推断强约束，但在组合伪布尔约束时产生的系数增长。另一种变体包括使用弱化和除法，这在实践中更有效，但可能推断出较弱的约束。在这两种情况下，削弱是强制性的，以获得冲突的约束。然而，其对伪布尔解算器性能的影响迄今尚未得到评估。本文研究了该规则的新的应用策略，旨在推断具有小系数的强约束。我们在Sat4j中实现了它们，并观察到它们中的每一个都提高了求解器的运行时间。虽然它们在所有基准上都没有表现得比其他人更好，但在冲突方面应用弱化具有令人惊讶的良好表现，而在冲突和原因方面应用部分弱化和划分则提供了最好的整体结果。
英文摘要：
Current pseudo-Boolean solvers implement different variants of the cutting planes proof system to infer new constraints during conflict analysis. One of these variants is generalized resolution, which allows to infer strong constraints, but suffers from the growth of coefficients it generates while combining pseudo-Boolean constraints. Another variant consists in using weakening and division, which is more efficient in practice but may infer weaker constraints. In both cases, weakening is mandatory to derive conflicting constraints. However, its impact on the performance of pseudo-Boolean solvers has not been assessed so far. In this paper, new application strategies for this rule are studied, aiming to infer strong constraints with small coefficients. We implemented them in Sat4j and observed that each of them improves the runtime of the solver. While none of them performs better than the others on all benchmarks, applying weakening on the conflict side has surprising good performance, whereas applying partial weakening and division on both the conflict and the reason sides provides the best results overall.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
