@InProceedings{qubos,
  author = {Abdelwaheb Ayari and David Basin},
  title = {{QUBOS}: Deciding Quantified Boolean Logic using Propositional Satisfiability Solvers},
  booktitle = {Formal Methods in Computer-Aided Design, Fourth
International Conference (FMCAD 2002)},
  pages = {187--201}
  year = 2002,
  volume = 2517,
  series = {Lecture Notes in Computer Science},
  address = {Portland Oregon}
  month = {November},
  publisher = {Springer-Verlag},
  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.  }
}