請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/21736
標題: | 藉積項分配為量化布林公式解決與認證最小化 A Cube Distribution Approach to QBF Solving and Certificate Minimization |
作者: | Li-Cheng Chen 陳立誠 |
指導教授: | 江介宏 |
關鍵字: | 量化布林公式,認證,Skolem 函數,Herbrand函數,字句選擇, Quantified Boolean Formula,certificate,Skolem function,Herbrand Function,clause selection, |
出版年 : | 2019 |
學位: | 碩士 |
摘要: | 量化布林公式是一種泛用且簡明的方法,以表示許多計算機科學的問題,包括機器人規劃、硬體與軟體之合成與驗證等等。實際應用時,如何有效地解決此公式並提供認證至關重要。此篇論文中,我們提出「積項分配」,為量化布林公式之解決與認證提出新觀點。此方法為公式之解決提供了大量靈活性,並以隨意項將認證化簡。我們將此新方法,實作於先前「字句選擇」的量化布林公式求解架構之上。實驗結果展示了我們的方法在解決與認證大小上,都勝於具認證功能的其它現有方法。 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 |
全文授權: | 未授權 |
顯示於系所單位: | 電子工程學研究所 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
ntu-108-1.pdf 目前未授權公開取用 | 1.77 MB | Adobe PDF |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。