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.