QBF画廊：幕后花絮
The QBF Gallery: Behind the Scenes
摘要：
近年来，在求解量化布尔公式（QBF）的理论和实践方面都取得了很大的进展。新的求解器已经成功地提高了既定的技术或实现新的解决范式。强大的预处理器已经实现，可以调整公式的编码，使其更容易求解。认证和解决方案提取的框架出现，允许一个QBF求解器的结果的详细解释，和新类型的QBF编码提出了各种应用问题。为了捕捉这些发展，QBF画廊于2013年成立。QBF画廊旨在提供一个论坛，以评估QBF工具，并收集新的，有表现力的基准，允许记录现状，并指出有前途的研究方向。这些基准成为在2013年QBF画廊和后续评估背景下进行的实验的基础。在本文中，我们报告的QBF画廊的设置。为此，我们进行了大量的实验，这不仅使我们能够评估工具的质量，而且还可以评估基准的质量。
英文摘要：
Over the last few years, much progress has been made in the theory and practice of solving quantified Boolean formulas (QBF). Novel solvers have been presented that either successfully enhance established techniques or implement novel solving paradigms. Powerful preprocessors have been realized that tune the encoding of a formula to make it easier to solve. Frameworks for certification and solution extraction emerged that allow for a detailed interpretation of a QBF solver's results, and new types of QBF encodings were presented for various application problems. To capture these developments the QBF Gallery was established in 2013. The QBF Gallery aims at providing a forum to assess QBF tools and to collect new, expressive benchmarks that allow for documenting the status quo and that indicate promising research directions. These benchmarks became the basis for the experiments conducted in the context of the QBF Gallery 2013 and follow-up evaluations. In this paper, we report on the setup of the QBF Gallery. To this end, we conducted numerous experiments which allowed us not only to assess the quality of the tools, but also the quality of the benchmarks.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
