利用虛擬布林規劃求解多值函式之對稱性布林編碼

Pseudo-Boolean Constraint Formulation of Symmetry Boolean Encoding for Multi-Valued Function

李孟彥(Meng-Yen Li)

指導教授 ： 江介宏

國立臺灣大學/電機資訊學院/電子工程學研究所/碩士(2011年)

https://doi.org/10.6342/NTU.2011.02361

摘要

在高階設計中，變數通常以多值符號的形式展現。多值邏輯於位元等級的實作被稱做編碼，選擇適當編碼是困難而具有挑戰性的問題。先前研究文獻顯示出預見所選編碼在經由強力邏輯最佳化後的效果是非常困難地。

　就我們目前所知，選擇具有特殊函式性質的編碼，除了最小化面積以外，是從未被研究過的課題。由於對稱性是最被廣泛研究應用的函式性質，我們希望能把這項性質穿引入編碼來實作多值函式。對稱布林函式在多種領域有其豐富應用。在密碼學中，對稱布林函式擁有特殊密碼參數。而在實體設計中，對稱布林函式更容易被最佳化。這些也被應用於在基於二元決策圖的合成的錯誤可測性之中。

　此論文中我們定義與研究所謂地對稱性編碼問題，這是一個試圖在實現多值函式時同時最大化編碼完函式的對稱數目的問題。我們提出一套系統化的方法將對稱性編碼問題透過虛擬布林規劃建立數學模型。透過已有的規劃最佳化軟體如IBM
ILOG CPLEX Optimizer(TM)，我們可以運算且產出對稱性編碼問題的解。除了
全對稱函式外，這套方法也可以用於部分對稱函式上。

　實驗結果顯示經由虛擬布林規劃求解，對稱性編碼與樸直編碼(直接以其二進位表示法編碼)相比所產生的編碼後函式，確實在大部分所測電路中擁有更多的對稱數量。對少於六個輸入，至多六十四多值的小型電路而言這套方法有著良好結果。但可擴展性不佳是個關鍵弱點。另外這套方法不適用於多輸出變數的電路。我們希望後續研究能克服這些弱點。

關鍵字

對稱性 ； 編碼 ； 虛擬布林規劃

並列摘要

In high level designs, variables are often represented
in the form of symbolic multi-values. The realization of
multi-valued logic in bit level is called encoding and
selecting the appropriate encoding would be a challenging
and difficult problem. Prior literatures showed that it is
hard to foresee the effect of chosen encoding after powerful
logic optimization.

To the best of our knowledge, choosing encoding biased
for some special functional property is never studied
before except minimizing area. Since symmetry is the most studied and applied functional property, we would like
weave this property into encoding when implement
multi-valued function. Symmetric Boolean functions have
many useful applications in various aspects. In cryptography, they have special cryptographic parameters.
It is easier to optimize symmetric functions in physical
design domain. They also applied in fault testability in
BDD based synthesis.

In this work, we define and study the Symmetry Encoding
Problem (SEP) as a problem to maximize the symmetries of
encoded function when realizing multi-valued function. We
also propose a systematic method to model the SEP into Pseudo-Boolean Constraint (PBC). Using existing constraint
optimizer like IBM ILOG CPLEX Optimizer(TM) we can solve
and generate the solution of SEP. Besides totally symmetric
function, the method can also target for partially
symmetric function.

Experiments show that by PBC solving, the symmetric
encoding generated will encode multi-valued function with
more symmetries in a large portion of test cases while
compared with naive encoding (encode multi-value in binary
representation directly). This method has promising result
for small size circuits, which has less than 6 of inputs
after encoding (up to 64 multi-values). However it has critical weaknesses, i.e. scalability. This method is also
not available for multiple outputs. We would like overcome
these weaknesses in future work.

並列關鍵字

symmetry ； encoding ； Pseudo-Boolean Constraint

參考文獻

[29] Donald Chai and Andreas Kuehlmann. A Fast Pseudo-Boolean Constraint Solver. In Proceedings of Design Automation Conference, pages 830, 2003.

[22] Chih-Wei (Jim) Chang, Ming-Fu Hsiao, Bo Hu, Kai Wang, Malgorzata Marek-Sadowska, Chung-Kuan Cheng, and Sao-Jie Chen. Fast Postplacement Optimization Using Functional Symmetries. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Volume 23, Issue 1, pages 102, 2004.

[26] Kuo-Hua Wang, Chung-Ming Chan, and Jung-Chang Liu. Simulation and SAT-Based Boolean Matching for Large Boolean Networks. In Proceedings of the Asia and South Pacific Design Automation Conference, Volume 2, pages 994, 2005.

[6] Jie-Hong Jiang, Yunjian Jiang, and Robert K. Brayton. An Implicit Method for Multi-Valued Network Encoding. In the Notes of the International Workshop on Logic Synthesis (IWLS), Tahoe City, 2001.

[16] Giovanni De Micheli, Robert K. Brayton, and Alberto L. Sangiovanni-Vincentelli. Optimal State Assignment for Finite State Machines. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Volume 4, Issue 3, pages 269, 1985.