DepQBF 6.0：超越传统QCDCL的基于搜索的QBF求解器
DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL
摘要：
我们提出了基于QCDCL的量化布尔公式（QBF）求解器DepQBF的最新主要发布版本6.0。QCDCL是冲突驱动子句学习（CDCL）范式的扩展，在最先进的命题可满足性（SAT）求解器中实现。Q-resolution演算（QRES）是QCDCL的一个QBF证明系统。QCDCL求解器可以产生QBFs的QRES证明在前束合取范式（PCNF）作为求解过程的副产品。与基于QRES的传统QCDCL相比，DepQBF 6.0实现了基于QRES概括的QCDCL变体。这种推广是由于一组额外的公理，并保持原来的Q-归结规则不变。QRES的推广使QCDCL可能产生比传统变体更短的指数证明。我们提出了一个概述DepQBF中实现的功能和报告的实验结果表明，广义QRES在QCDCL的有效性。
英文摘要：
We present the latest major release version 6.0 of the quantified Boolean formula (QBF) solver DepQBF, which is based on QCDCL. QCDCL is an extension of the conflict-driven clause learning (CDCL) paradigm implemented in state of the art propositional satisfiability (SAT) solvers. The Q-resolution calculus (QRES) is a QBF proof system which underlies QCDCL. QCDCL solvers can produce QRES proofs of QBFs in prenex conjunctive normal form (PCNF) as a byproduct of the solving process. In contrast to traditional QCDCL based on QRES, DepQBF 6.0 implements a variant of QCDCL which is based on a generalization of QRES. This generalization is due to a set of additional axioms and leaves the original Q-resolution rules unchanged. The generalization of QRES enables QCDCL to potentially produce exponentially shorter proofs than the traditional variant. We present an overview of the features implemented in DepQBF and report on experimental results which demonstrate the effectiveness of generalized QRES in QCDCL.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
