通过子句选择求解量化布尔公式（QBF）
Solving QBF by Clause Selection
浏览论文内容
中文总结 AI 辅助
该研究针对QBF问题，开发了一种推广隐式击中集枚举概念的新颖算法，经实验验证其性能可与现有最优QBF求解器媲美且常更优。
中文摘要 AI 辅助
基于隐式击中集枚举的算法应用日益广泛，包括最大可满足性和基于模型的诊断等领域。本文在量化布尔公式（Quantified Boolean Formulas，QBF）的语境中利用隐式击中集枚举方法。首先开发了一种适用于两层量化QBF的简单算法，该算法既与现有的隐式击中集枚举研究相关，也与近期基于抽象精化的QBF研究相关。随后将这些思路扩展，开发出一种新颖的QBF算法，该算法推广了隐式击中集枚举的概念。在代表性问题实例上获得的实验结果表明，该新颖算法与QBF求解的现有最优水平具有竞争力，且通常表现更优。
英文摘要
Algorithms based on the enumeration of implicit hitting sets find a growing number of applications, which include maximum satisfiability and model based diagnosis, among others. This paper exploits enumeration of implicit hitting sets in the context of Quantified Boolean Formulas (QBF). The paper starts by developing a simple algorithm for QBF with two levels of quantification, which is shown to relate with existing work on enumeration of implicit hitting sets, but also with recent work on QBF based on abstraction refinement. The paper then extends these ideas and develops a novel QBF algorithm, which generalizes the concept of enumeration of implicit hitting sets. Experimental results, obtained on representative problem instances, show that the novel algorithm is competitive with, and often outperforms, the state of the art in QBF solving.
