AAAI Publications, Workshops at the Thirtieth AAAI Conference on Artificial Intelligence

Font Size: 
Solving QBF Instances with Nested SAT Solvers
Bart Bogaerts, Tomi Janhunen, Shahab Tasharrofi

Last modified: 2016-03-29


We present a new approach towards solving quantifiedBoolean formulas (QBFs) using nested SAT solvers with lazyclause generation. The approach has been implemented ontop of the Glucose solver by adding mechanisms for nestingsolvers as well as clause learning. Our preliminary experiments show that nested SAT solving performs (out of the box)relatively well on QBF, when taking into account that no particular QBF-oriented solving techniques were incorporated.The most important contribution of this work is that it provides a systematic way of lifting advances in SAT solvers toQBFs with low implementation effort.


sat-to-sat; qbf; sat

Full Text: PDF