Large Scale Ashenhurst Decomposition via SAT Solving and Craig Interpolation
Date Issued
2009
Date
2009
Author(s)
Lin, Hsuan-Po
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.
Subjects
Boolean function
functional decomposition
SAT solving
Craig interpolation
functional dependency
Type
thesis
File(s)![Thumbnail Image]()
Loading...
Name
ntu-98-R96943076-1.pdf
Size
23.32 KB
Format
Adobe PDF
Checksum
(MD5):77af5f29c9b7bff080ea0259690bd083