SHF: Small: Mechanical Verification of QBF Results

SHF：小型：QBF 结果的机械验证

• 批准号: 2010951
• 负责人: Marienus Heule
• 金额: $ 19.66万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-11-02 至 2021-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2010951&HistoricalAwards=false
• 关键词: SHF; Small; Mechanical; Verification; 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.

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