SHF: Small: Mechanical Verification of QBF Results

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

• 批准号: 1618574
• 负责人: Marienus Heule
• 金额: $ 50万
• 依托单位: University of Texas at Austin
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2016
• 资助国家: 美国
• 起止时间: 2016-08-01 至 2020-02-29
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1618574&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解算器在科学和工业应用中迫切需要的。