量化布林代數認證之化簡

Abstract

量化布林代數(QBF)的求值與確認在解決屬於PSPACE-complete複雜度的問題上是重要的議題，許多計算機科學領域的應用都能夠以QBF精簡的編碼，在這些應用中，QBF認證在提供必要的合成資訊上擔任重要的腳色。QBF認證主要有兩種型態，一是文法上的認證，包含了Q共識(Q-consensus)以及Q歸結(Q-resolution)，另一個則是語意上的認證，包含了Skolem函數以及Herbrand函數，而其中語意上的認證在合成應用上更是十分有用。近來，一個卓越的線性時間演算法—ResQu被提出用來將Q共識以及Q歸結轉換為Herbrand函數以及Skolem函數。此演算法可將由現在以Q-DPLL為基礎的QBF求解器所產生的文法認證轉換為語意認證，並藉此幫助合成相關的應用問題。不幸的是，這些由QBF求解器所產生的文法認證經常太過於複雜，也導致轉換出來的語意認證過大而不能被實際應用所使用，因此減低語意認證的大小對實際的應用來說具有十分重要的價值。此論文主要將使用提出四項在語意認證萃取上的彈性來對Skolem與Herbrand函數做最小化，我們利用布林減少的可延後性(reduction postponing)實作了一個最小化Skolem與Herbrand函數的程序以及一個支援簡化指令的不落地(on-the-fly)認證建立程序。以And-inverter graph(AIG)節點數觀點，實驗結果指出此最小化的程序可以有效率的減低QBF認證的大小，除此之外不落地簡化程序也可以有效率的減低在建立Skolem及Herbrand函數時的尖峰記憶體使用量(peak memory)，因而提高實際的計算能力。

The evaluation and validation of Quantified Boolean Formulas (QBFs) are important subjects in conquering application problems belonging to the PSPACE-complete complexity class. Many applications in computer science can be compactly encoded in term of QBFs. In certain applications, QBF certificates play an important role in providing essential information for synthesis. There are primarily two types of certificates: the syntactic type in the form of Q-resolution/Q-consensus proofs and the semantic type in the form of Herbrand/Skolem functions. The latter is particularly useful in synthesis applications. A recent advancement established a linear-time algorithm, called ResQu, that converts a Q-resolution/Q-consensus proof to a Herbrand function countermodel/Skolem function model. It allows the syntactic certificates generated by the modern Q-DPLL based solvers be transformed into semantic certificates, and thus enables synthesis applications. Unfortunately the syntactic Q-resolution/Q-consensus proofs generated by a QBF solver are often too complex to be practically used for real-world applications. Therefore reducing the circuit size of Herbrand/Skolem functions can be of important practical value to allow real-world applications. This thesis aims to reduce the certificate size by characterizing four kinds of flexibilities for Herbrand/Skolem function minimization. In particular we implement a certificate minimization procedure based on reduction postponing as well as an on-the-fly simplification procedure for certificate construction. Experimental results show that the reduction postponing procedure can effectively reduce the size of certificates in terms of and-inverter graph nodes. In addition, the on-the-fly simplification procedure can effectively reduce peak memory for Herbrand/Skolem function construction and thus extend computational scalability.