@InProceedings{ ayari.ea:qubos:2002, abstract = {We describe Qubos (QUantified BOolean Solver), a decision procedure for quantified Boolean logic. The procedure is based on nonclausal simplification techniques that reduce formulae to a propositional clausal form after which off-the-shelf satisfiability solvers can be employed. We show that there are domains exhibiting structure for which this procedure is very effective and we report on experimental results.}, author = {Abdelwaheb Ayari and David Basin}, booktitle = {Formal Methods in Computer-Aided Design, Fourth International Conference, FMCAD 2002}, language = {USenglish}, pdf = {papers/2002/0_root-camera-ready.pdf}, ps = {papers/2002/1_root-camera-ready.ps.gz}, publisher = {Springer-Verlag}, title = {Qubos: Deciding Quantified Boolean Logic using Propositional Satisfiability Solvers}, year = 2002 }