AI 中文总结
该研究提出两种结合CEGAR的QBF求解新方法，经实验验证，CEGAR驱动的求解器性能优于现有求解器，且该学习技术可提升基于DPLL的QBF求解器性能，为QBF研究开辟了新方向。
AI 中文摘要
我们提出两种在量化布尔公式（QBF）求解器中使用反例引导的抽象精化（CEGAR）的新方法。第一种方法开发了一种递归算法，其搜索由CEGAR驱动（而非DPLL）。第二种方法将CEGAR作为额外的学习技术应用于现有基于DPLL的QBF求解器。对实现的原型进行的实验评估表明，在QBF-LIB的多个测试族上，由CEGAR驱动的求解器性能优于现有求解器，且采用该额外学习技术的DPLL求解器也从中受益。因此，本文为QBF研究开辟了两个有前景的方向：作为现有方法替代方案的CEGAR驱动求解器，以及DPLL中一种新型学习技术。
英文摘要
We propose two novel approaches for using Counterexample-Guided Abstraction Refinement (CEGAR) in Quantified Boolean Formula (QBF) solvers. The first approach develops a recursive algorithm whose search is driven by CEGAR (rather than by DPLL). The second approach employs CEGAR as an additional learning technique in an existing DPLL-based QBF solver. Experimental evaluation of the implemented prototypes shows that the CEGAR-driven solver outperforms existing solvers on a number of families in the QBF-LIB and that the DPLL solver benefits from the additional type of learning. Thus this article opens two promising avenues in QBF: CEGAR-driven solvers as an alternative to existing approaches and a novel type of learning in DPLL.
DOI：10.1007/978-3-642-31612-8_10
