Watched Data Structures for QBF Solvers

Abstract In the last few years, we have seen a tremendous boost in the efficiency of SAT solvers, this boost being mostly due to Chaff. Chaff owes 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 ) two Chaff -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.

Authors

• Ian P. Gent
• Enrico Giunchiglia
• Massimo Narizzano
• Andrew G. D. Rowley
• Armando Tacchella

Keywords

No keywords are indexed for this paper.