SHF: Small: Mechanical Verification of QBF Results

许多重要的工业应用，如验证和综合问题，可以有效地解决可满足性（SAT）求解器。 然而，这种方法涉及到将原始问题转换为SAT，通常会导致生成数十到数千个几乎相同的子问题副本。 量化布尔公式（QBF）的形式主义提供了一个方便的框架，以compensate翻译许多这些有趣的问题。例如，软件验证和硬件综合问题可以转换为QBF，同时避免生成这些几乎相同的副本。 因此，QBF为计算机科学中的关键问题提供了一个紧凑的表示，但QBF的表现力是有代价的：很难验证这些求解器产生的结果。 解决这个问题的现有方法都有缺点。 流行的方法涉及昂贵的验证算法，并限制了所使用的技术。 最近的一项技术进步，被称为子句证明，可以解决大多数问题。 然而，有效地检查子句证明是复杂的，因此信任一个复杂程序（QBF求解器）的结果取决于另一个复杂程序（检查器）的正确性。 为了提高对QBF求解器结果的信心，需要一个经过机械验证的检查器。 本研究为QBF求解器的科学和工业应用开发了一个统一、完整和可信的QBF求解框架。

Many important industrial applications, such as verification and synthesis problems, can be efficiently solved by satisfiability (SAT) solvers. However, this approach involves translating the original problem into SAT that typically results in generating dozens to thousands of nearly identical copies of subproblems. The quantified Boolean formula (QBF) formalism provides a convenient framework to compactly translate many of these interesting problems. For example, software verification and hardware synthesis problems can be translated into QBF, while avoiding generating these nearly identical copies. Hence, QBF facilities a compact representation of crucial problems in computer science.The expressiveness of QBF comes at a price: it is hard validate the results produced by these solvers. The existing approaches for addressing this problem all have disadvantages. Prevalent approaches involve costly validation algorithms and limit the used techniques. A recent technological advancement, known as clausal proofs, takes care of most problems. However, efficiently checking clausal proofs is complicated, thus trusting the results of one complex program (a QBF solver) depends on the correctness of another complex program (the checker). To boost confidence in the results of QBF solvers, a mechanically-verified checker is required. This research develops a uniform, complete, and trustworthy framework for QBF solving which is urgently needed for the scientific and industrial application of QBF solvers.