基于高斯-若尔当消元的CDCL求解器证明生成
计算机科学中的逻辑
2023-04-11 v1
摘要
基于冲突驱动子句学习(conflict-driven clause-learning, CDCL)框架的传统布尔可满足性(SAT)求解器在涉及大量奇偶约束的公式上表现不佳。CryptoMiniSat求解器以高斯-若尔当消元增强CDCL，大幅提升了在这类公式上的性能。将TBUDDY可生成证明的BDD库集成进CryptoMiniSat，使其能在使用高斯-若尔当消元时生成不可满足性证明。这些证明与标准的子句证明框架兼容。
引用
@article{arxiv.2304.04292,
title = {Proof Generation for CDCL Solvers Using Gauss-Jordan Elimination},
author = {Mate Soos and Randal E. Bryant},
journal= {arXiv preprint arXiv:2304.04292},
year = {2023}
}
备注
Presented at 2022 Workshop on the Pragmatics of SAT