利用可滿足性求解法與克雷格內插法之大尺度亞氏函式拆解

Abstract

函式拆解著眼於將一個布林函式拆解成一系列較小的子函式。在本篇論文裡面， 我們著重在亞氏函式拆解，這是一種因為他的簡易性而有許多實際應用的常見函 式拆解法。我們將函式拆解問題包裝成可滿足性求解問題，更進一步的採用克雷 格內插法以及函式相依性計算來找出相對應的子函式。在我們採用可滿足性求解 法為核心的研究中，輸入變數分組的過程可以被自動的處理，並且嵌入我們的函 式拆解演算法中。我們也可以自然的將我們的演算法延伸，應用在允許共用輸入 變數與多輸出變數的函式拆解問題上，這些問題在以往採用二元決策圖為核心資 料結構的演算法中都很難被解決。實驗結果顯示，我們提出的演算法可以有效的 處理輸入變數達到三百個之多的函式。

Functional decomposition aims at decomposing a Boolean function into a set of smaller sub-functions. In this thesis, we focus on Ashenhurst decomposition, which has practical applications due to its simplicity. We formulate the decomposition problem as SAT solving, and further apply Craig interpolation and functional dependency computation to derive composite functions. In our pure SAT-based solution, variable partitioning can be automated and integrated into the decomposition procedure. Also we can easily extend our method to non-disjoint and multiple-output decompositions which are hard to handle using BDD-based algorithms. Experimental results show the scalability of our proposed method, which can effectively decompose functions with up to 300 input variables.