Conflict driven learning in a quantified Boolean satisfiability solver
Conflict driven learning in a quantified Boolean satisfiability solver
复制标题
量化布尔可满足性求解器中的冲突驱动学习
DOI：
10.1145/774572.774637
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
S. Malik
中科院分区：
文献类型：
--
作者：
Lintao Zhang;S. Malik
在验证社区中，最近对量化布尔公式评估 (QBF) 的兴趣有所增加，因为许多有趣的顺序电路验证问题可以表述为 QBF 实例。与 QBF 密切相关的一个研究领域是布尔可满足性 (SAT)。 SAT 研究的最新进展产生了一些非常高效的 SAT 求解器。这些求解器中采用的关键技术之一是冲突驱动学习。在本文中，我们将冲突驱动学习应用于 QBF 设置中。我们表明，冲突驱动的学习可以被视为条款的解决过程。我们证明，在一定条件下，QBF 解析得到的同义反复子句也遵循正则（非同义反复）子句的蕴含和冲突规则；因此它们可以被视为常规子句并在将来的搜索中使用。我们已经在一个名为 Quaffle 的新 QBF 求解器中实现了这个想法，我们的初步实验表明，冲突驱动学习可以大大加快我们测试的大多数基准的求解过程。
Within the verification community, there has been a recent increase in interest in Quantified Boolean Formula evaluation (QBF) as many interesting sequential circuit verification problems can be formulated as QBF instances. A closely related research area to QBF is Boolean Satisfiability (SAT). Recent advances in SAT research have resulted in some very efficient SAT solvers. One of the critical techniques employed in these solvers is Conflict Driven Learning. In this paper, we adapt conflict driven learning for application in a QBF setting. We show that conflict driven learning can be regarded as a resolution process on the clauses. We prove that under certain conditions, tautology clauses obtained from resolution in QBF also obey the rules for implication and conflicts of regular (non-tautology) clauses; and therefore they can be treated as regular clauses and used in future search. We have implemented this idea in a new QBF solver called Quaffle and our initial experiments show that conflict driven learning can greatly speed up the solution process for most of the benchmarks we tested.