Watched Data Structures for QBF Solvers
Watched Data Structures for QBF Solvers
复制标题
DOI：
10.1007/978-3-540-24605-3_3
复制
发表时间：
2003-05
期刊：
影响因子：
--
通讯作者：
Ian P. Gent;E. Giunchiglia;Massimo Narizzano;Andrew Rowley;A. Tacchella
中科院分区：
文献类型：
--
作者：
Ian P. Gent;E. Giunchiglia;Massimo Narizzano;Andrew Rowley;A. Tacchella
在过去的几年里，我们看到SAT求解器的效率有了巨大的提高，这种提高主要是由于箔条。chaffw的一些效率归功于它的“双文字观察”数据结构。本文给出了量化布尔公式（QBF）可满足性解算器的数据结构。特别地，我们提出了(i)两个类似于chafff的单位子句文本监视方案；以及（ii）另外两个监视的数据结构，一个用于检测纯字面量，另一个用于检测无效量词。我们使用随机生成的和真实世界的基准测试，对提出的数据结构进行了实验评估。我们的结果表明，子句监视非常有效，而2和3字面值监视数据结构随着子句长度的增加而变得更加有效。量词观察结构似乎对所考虑的实例无效。
In the last few years, we have seen a tremendous boost in the efficiency of SAT solvers, this boost being mostly due toChaff.Chaffowes some of its efficiency to its “two-literal watching” data structure.In this paper we present watched data structures for Quantified Boolean Formula (QBF) satisfiability solvers. In particular, we propose (i) twoChaff-like literal watching schemes for unit clause detection; and (ii) two other watched data structures, one for detecting pure literals and the other for detecting void quantifiers. We have conducted an experimental evaluation of the proposed data structures, using both randomly generated and real-world benchmarks. Our results indicate that clause watching is very effective, while the 2 and 3 literal watching data structures become more effective as the clause length increases. The quantifier watching structure does not appear to be effective on the instances considered.