Certified Branch-and-Bound MaxSAT Solving (Extended Version)
Dieter Vandesande, Jordi Coll, Bart Bogaerts
在过去的几十年中,组合式求解器已经看到了显着的性能改进,使他们能够在实际应用中实际应用。 在其中一些应用程序中,确保求解器输出的正确性至关重要。 然而,现代求解器的复杂性使他们容易受到源代码中的错误。 在可理解性检查(SAT)领域,这个问题已通过证明记录来解决,其中求解器生成其答案的正确性的正式证明。 对于更多的表现问题,如 SAT 的优化变体 MaxSAT,证明日志记录直到最近才出现类似的突破。 在本文中,我们展示了如何在Branch-and-Bound MaxSAT解决中实现最先进的技术证明日志记录。 这包括验证此类算法中使用的超前瞻方法,以及基于所谓的多有价值决策图(MDD)的伪布尔约束的高级类法规编码。 我们在主要的分支和绑定求解器MaxCDCL中实现这些想法,并实验证明证明日志记录在有限的开销下是可行的,而证明检查仍然是一个挑战。
Over the past few decades, combinatorial solvers have seen remarkable performance improvements, enabling their practical use in real-world applications. In some of these applications, ensuring the correctness of the solver's output is critical. However, the complexity of modern solvers makes them susceptible to bugs in their source code. In the domain of satisfiability checking (SAT), this issue has been addressed through proof logging, where the solver generates a formal proof of the correctnes...