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. W e show that there are domains exhibiting structure for which this procedure is very effective and we report on experimental results.
CITATION STYLE
Ayari, A., & Basin, D. (2002). QUBOS: Deciding quantified boolean logic using propositional satisfiability solvers. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2517, pp. 187–201). Springer Verlag. https://doi.org/10.1007/3-540-36126-x_12
Mendeley helps you to discover research relevant for your work.