The QBFGallery 2014: The QBF Competition at the FLoC Olympic Games

摘要: The QBFGallery 2014 was a competitive evaluation for QBF solvers organized in the context of FLoC Olympic Games Vienna Summer Logic. Quantified Boolean formulas (QBF) extend propositional logic by existential and universal quantifiers over variables and, thus, lift satisfiablity problem from NP to PSPACE. In consequence, there are many application problems fields like verification, synthesis, planning that can be encoded efficiently QBF. This  motivates quest efficient solvers. invited developers submit their tools uniform environment. Gold, silver, bronze track medals were awarded solved most each three different tracks covering various kinds benchmarks. Additionally, participants successful overall decorated with Kurt G odel medals, official prizes the  Games. this paper, we give an overview setup competition, briefly review participating solvers, finally report on results 2014.