Abstract:

Qubos: Deciding Quantified Boolean Logic using Propositional Satisfiability Solvers

Abdelwaheb Ayari and David Basin


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.