## 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.