Simplification of Quantified Boolean Formula Certificates

• Main Authors: Shuo-Ren Lin, 林碩紝
• Other Authors: Jie-Hong Jiang
• Format: Others
• Language: en_US
• Published: 2013
• Online Access: http://ndltd.ncl.edu.tw/handle/27458066247791628128

碩士 === 國立臺灣大學 === 電子工程學研究所 === 101 === 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.