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

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

關鍵字

布林函式；函式拆解；可滿足性求解法；克雷格內插法；函式相依性

並列摘要

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.

並列關鍵字

Boolean function ； functional decomposition ； SAT solving ； Craig interpolation ； functional dependency

參考文獻

[16] C.-C. Lee, J.-H. R. Jiang, C.-Y. Huang, and A. Mishchenko. Scalable exploration

[12] J.-H. R. Jiang, J.-Y. Jou, and J.-D. Huang. Compatible class encoding in hyperfunction

[3] J. Cong and Y.-Y. Hwang. Boolean matching for LUT-based logic blocks with

[1] R. L. Ashenhurst. The decomposition of switching functions. Computation Lab,

tions on Computer-Aided Design of Integrated Circuits, 20(9):1077-1090, 2001.

國際替代計量

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

主題瀏覽