Please use this identifier to cite or link to this item:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/21736
Title: | 藉積項分配為量化布林公式解決與認證最小化 A Cube Distribution Approach to QBF Solving and Certificate Minimization |
Authors: | Li-Cheng Chen 陳立誠 |
Advisor: | 江介宏 |
Keyword: | 量化布林公式,認證,Skolem 函數,Herbrand函數,字句選擇, Quantified Boolean Formula,certificate,Skolem function,Herbrand Function,clause selection, |
Publication Year : | 2019 |
Degree: | 碩士 |
Abstract: | 量化布林公式是一種泛用且簡明的方法,以表示許多計算機科學的問題,包括機器人規劃、硬體與軟體之合成與驗證等等。實際應用時,如何有效地解決此公式並提供認證至關重要。此篇論文中,我們提出「積項分配」,為量化布林公式之解決與認證提出新觀點。此方法為公式之解決提供了大量靈活性,並以隨意項將認證化簡。我們將此新方法,實作於先前「字句選擇」的量化布林公式求解架構之上。實驗結果展示了我們的方法在解決與認證大小上,都勝於具認證功能的其它現有方法。 Quantified Boolean Formulas (QBFs) are powerful expressions to naturally and concisely encode many decision problems in computer science, such as robotic planning, hardware/software synthesis and verification, among others. Their effective solving and certificate (in terms of model and countermodel) generation play crucial roles to enable practical applications. In this work, we give a new view on QBF solving and certificate generation by the cube distribution interpretation. It provides a largely increased flexibility for QBF reasoning and allows compact certificate derivation with don't cares. Through this interpretation, we develop a QBF solver based on the prior clause selection framework. Experimental results demonstrate the superiority of our solver in both solving performance and certificate size compared to other state-of-the-art solvers with certificate generation ability. |
URI: | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/21736 |
DOI: | 10.6342/NTU201900661 |
Fulltext Rights: | 未授權 |
Appears in Collections: | 電子工程學研究所 |
Files in This Item:
File | Size | Format | |
---|---|---|---|
ntu-108-1.pdf Restricted Access | 1.77 MB | Adobe PDF |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.