Q-PREZ: QBF evaluation using partition, resolution and elimination with ZBDDs

摘要

In recent years, there has been an increasing interest in quantified Boolean formula (QBF) evaluation, since several VLSI CAD problems can be formulated efficiently as QBF instances. Since the original resolution-based methods can suffer from space explosion, existing QBF solvers perform decision tree search using the Davis-Putnam Logemann and Loveland (DPLL) procedure. In this paper, we propose a new QBF solver, Q-PREZ, that overcomes the space explosion problem faced in resolution by using efficient data structures and algorithms, which in turn can outperform DPLL-based QBF solvers. We partition the CNF and store the clauses compactly in zero-suppressed binary decision diagrams (ZBDDs). Then, we introduce new and powerful operators to perform existential and universal quantification on the partitioned ZBDD clauses as resolution and elimination procedures. Our preliminary experimental results show that Q-PREZ is able to achieve significant speedups over state-of-the-art QBF solvers.