TY - GEN
T1 - Watched data structures for QBF solvers
AU - Gent, I
AU - Giunchiglia, E
AU - Narizzano, M
AU - Rowley, A
AU - Tacchella, A
PY - 2004
Y1 - 2004
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=26444480521&partnerID=8YFLogxK
UR - http://www.springerlink.com/content/ndy7emh7ulea0rua/
U2 - 10.1007/978-3-540-24605-3_3
DO - 10.1007/978-3-540-24605-3_3
M3 - Conference contribution
SN - 3-540-20851-8
T3 - Lecture notes in computer science
SP - 25
EP - 36
BT - Theory and applications of satisfiability testing
A2 - Giunchiglia, E
A2 - Tacchella, A
PB - Springer
ER -