Towards a Symmetric Treatment of Satisfaction and Conflicts in Quantified Boolean Formula Evaluation
Towards a Symmetric Treatment of Satisfaction and Conflicts in Quantified Boolean Formula Evaluation
复制标题
DOI：
10.1007/3-540-46135-3_14
复制
发表时间：
2002-09
期刊：
影响因子：
--
通讯作者：
Lintao Zhang;S. Malik
中科院分区：
文献类型：
--
作者：
Lintao Zhang;S. Malik
在本文中，我们描述了一种新的量化布尔公式(QBF)求值框架。新的框架基于Davis-Putnam(DPLL)搜索算法。在现有的基于DPLL的QBF算法中，问题库以合取范式(CNF)的形式表示为一组子句，由这些子句生成蕴涵关系，并按时间顺序在搜索树中回溯。在这项工作中，我们用冲突驱动的学习以及可满足性指导的蕴涵和学习来扩充基本的DPLL算法。除了传统的子句数据库外，我们在数据结构中增加了一个立方体数据库。我们证明了立方体可以用来生成可满足性导向蕴涵，类似于由子句产生的冲突导向蕴涵。我们证明了在QBF环境下，搜索树的冲突叶和满意叶都以对称的方式为求解器提供了有价值的信息。我们已经在新的QBF解算器Quaffle中实现了我们的算法。实验结果表明，对于某些测试用例，可满足性指导的蕴涵和学习显著地削减了搜索。
In this paper, we describe a new framework for evaluating Quantified Boolean Formulas (QBF). The new framework is based on the Davis-Putnam (DPLL) search algorithm. In existing DPLL based QBF algorithms, the problem database is represented in Conjunctive Normal Form (CNF) as a set of clauses, implications are generated from these clauses, and backtracking in the search tree is chronological. In this work, we augment the basic DPLL algorithm with conflict driven learning as well as satisfiability directed implication and learning. In addition to the traditional clause database, we add a cube database to the data structure. We show that cubes can be used to generate satisfiability directed implications similar to conflict directed implications generated by the clauses. We show that in a QBF setting, conflicting leaves and satisfying leaves of the search tree both provide valuable information to the solver in a symmetric way. We have implemented our algorithm in the new QBF solver Quaffle. Experimental results show that for some test cases, satisfiability directed implication and learning significantly prunes the search.