Submitter: Shahab Tasharrofi
Description: Devised by B. Bogaerts, T. Janhunen, and S. Tasharrofi, is based on nested SAT solving and theory transformations. The main tools utilized for translation are:
  • sat-to-sat, a (non-)prenex (non-)CNF QBF solver that is based on nested SAT solving, and it is able to do early propagation of information between nested solvers.
  • qbf2sts [42], a translator from QDIMACS/QCIR input format to sat- to-sat input format with the ability to reverse engineer circuits and apply several theory transformations to simplify the representation of QBF formulas.

Details are available in
Janhunen, T., Tasharrofi, S., Ternovska, E.: SAT-TO-SAT: Declarative extension of SAT solvers with new propagators. In: Proceedings of AAAI. (2016)
Bogaerts, B., Janhunen, T., Tasharrofi, S.: Solving QBF instances with nested SAT solvers. Proceedings of Beyond NP (2016)