利用決策過程產生內插邏輯之演算法：一個嶄新的布林電路重新合成技術

Abstract

布林電路操作是一個被廣泛地使用在電路設計自動化領域中之重要技術。為了釐清及整合此方面之技術，本論文探究了兩項重要的電路重寫技巧，其一為多餘物增加與拔除，其二為函數重組成。我們從這兩項電路重寫技巧的問題定義開始做比較，進而去分析各自理論之異同，最後再深入討論其演算法上之差異與優缺點。我們從此整合性的分析與比較之中，獲得了幾項關於電路改寫技術之重要啟發：第一、多餘物增加與拔除和函數重組成皆是在探索和推導奎格內插之行為。第二、新的奎格內插產生演算法可以被嵌入於可滿足性解法器中，而不須記錄不滿足解析圖；此新的演算法提昇了奎格內插電路產生過程之可控制性，演算法的彈性與電路最佳化的能力。第三、我們的演算法整合電路重寫分析比較後之優缺點，進而提出一創新之客製化奎格內插器。從實驗結果而論，本論文所提出之創新奎格內插產生演算法具有多項優點，包含使用更少的記憶體及產生更小的奎格內插電路等等。

Boolean circuit manipulation is one of the most important techniques generally used in the design automation. To extend it for future design paradigms, we study two of the most important Boolean circuit rewriting techniques, redundancy addition and removal (RAR) and functional decomposition, and explore the possibility of unifying these two techniques on a unified Boolean circuit optimization platform. From problem formulation, theoretical analysis, to the comparison of pros and cons in the related algorithms, such unification exploration enlights us several interesting observations and conclusions in the technique of circuit rewriting. The first is a claim that constraint deduction in RAR is a mechanism equivalent to perform constraint solving and explore Craig interpolation. The second is a novel algorithm that embeds the Craig interpolant generation in SAT solving without constructing resolution graph and thus serves as a white-box technique to increase the controllability, flexibility, and capability in optimization. The third is an integrated algorithm, a framework for circuit resubstitution with the novel interplant constructing algorithm. The experimental results show that our algorithm has the advantages over the prior interpolant generation techniques in both memory usage and interpolation circuit size.