Watched data structures for QBF solvers

I Gent, E Giunchiglia, M Narizzano, A Rowley, A Tacchella

Research output: Chapter in Book/Report/Conference proceedingConference contribution

17 Citations (Scopus)


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.

Original languageEnglish
Title of host publicationTheory and applications of satisfiability testing
Subtitle of host publication6th international conference, SAT 2003, Santa Margherita Ligure, Italy, May 5-8 2003 : selected revised papers
EditorsE Giunchiglia, A Tacchella
Number of pages12
ISBN (Print)3-540-20851-8
Publication statusPublished - 2004

Publication series

NameLecture notes in computer science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Dive into the research topics of 'Watched data structures for QBF solvers'. Together they form a unique fingerprint.

Cite this