Solving QBF with SMV

Francesco M. Donini, Paolo Liberatore, Fabio Massacci, and Marco Schaerf

Proceedings of the Eighth International Conference on Principles of Knowledge Representation and Reasoning (KR 2002)

The possibility of solving the Quantified Boolean Formulae (QBF) problems using the SMV system is a consequence of two well-known theoretical results: the membership of QBF to PSPACE, and the PSPACE-hardness of LTL (and therefore, of SMV). Nevertheless, such results do not imply the existence of a reduction that is also of practical utility. In this paper, we show a reduction from QBF to SMV that is linear (instead of cubic), and uses a constant-size specification. This new reduction has three applications the previous one has not: first, it allows for solving QBF problems using SMV-like systems, which are now more developed than direct QBF solvers; second, we can use it to verify whether the performance behavior of direct QBF solvers is intrinsic of the problem, or rather an effect of the solving algorithm; third, random hard SMV instances can be easily generated by reduction from QBF hard instances (whose generation method is now established).


 @inproceedings{DLMS-KR-02,
 title = {Solving QBF with SMV},
 year = {2002},
 author = {Donini, Francesco M. and Liberatore, Paolo and
 Massacci, Fabio and Schaerf, Marco},
 booktitle = {Proceedings of the Eighth International Conference
 on Principles of Knowledge Representation and Reasoning
 (KR 2002)},
 pages = {578--589},
 }
 
HTTP download.