(3.238.7.202) 您好!臺灣時間:2021/02/26 14:51
字體大小: 字級放大   字級縮小   預設字形  
回查詢結果

詳目顯示:::

我願授權國圖
: 
twitterline
研究生:陳韋翰
研究生(外文):Wei-Han Chen
論文名稱:基於 Max-SAT 求解器的二元體表達式簡化工具
論文名稱(外文):A Simplification Tool for Expressions over Binary Fields Using Max-SAT Solver
指導教授:鄭振牟鄭振牟引用關係
指導教授(外文):Chen-Mou Chen
口試委員:楊柏因陳君明
口試委員(外文):Bo-Yin YangJiun-Ming Chen
口試日期:2014-06-14
學位類別:碩士
校院名稱:國立臺灣大學
系所名稱:電子工程學研究所
學門:工程學門
學類:電資工程學類
論文種類:學術論文
論文出版年:2014
畢業學年度:102
語文別:英文
論文頁數:26
中文關鍵詞:二元體表達式簡化Max-SAT最佳化編譯器
外文關鍵詞:expression simplificationMax-SAToptimizationcompiler
相關次數:
  • 被引用被引用:0
  • 點閱點閱:195
  • 評分評分:系統版面圖檔系統版面圖檔系統版面圖檔系統版面圖檔系統版面圖檔
  • 下載下載:0
  • 收藏至我的研究室書目清單書目收藏:1
在密碼學領域的演算法實作中,程式的效能是實作時的重要考量,為了提高效
能,設計者無法使用現有的高階程式語言實作所有的演算法,而需要在關鍵運算
上使用低階語言(如組合語言)來描述,使程式整體的效能達到目標。
我們的目標是將二元體中的表達式自動地轉換為低階語言程式碼,而且此程式
碼的效能比直接簡單的轉換方式來的好。
在此研究中,我們將二元體表達式的簡化問題轉換為 Max-SAT 問題,並使用
現有的Max-SAT 求解器求解;我們的實驗結果顯示,我們可以在合理的時間內把
表達式簡化為原本的 50% ;而根據所給予的關係式數量,我們可以在運算時間和
程式的優化程度之間作取捨。


Efficiency is an important consideration in cryptosystem algorithms implementation. Therefore, a designer has to implement critical part of algorithms in low level languages such as assembly language.

Our goal is to automate this human work. The designer can describe critical part of algorithms in high level languages and we convert that into a simplified representation in low level languages.

In this work we convert the problem of simplifying binary field expressions into instances of Max-SAT problems, and solve them by an existing Max-SAT solver. It turns out that we can achieve up to 50% improvements. And there is a trade-off between time and quality depend on how many relations are allowed to use in simplification.



1 Introduction 1
1.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.2 Our Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.3 Roadmap . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
2 Finite Field Multiplication 4
2.1 Preliminary . . . . . . . . . . . . . . . . . . . 4
2.2 Karatsuba Algorithm . . . . . . . . . . . . . . 5
2.3 Multiplication Using Fast Fourier Transform . 6
2.4 Other Ways . . . . . . . . . . . . . . . . . . 6
3 Max-SAT 7
3.1 Problem Definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
3.2 Max-SAT Solver . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
4 Related Works 9
4.1 High-Level Synthesis . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
4.2 Common Subexpression Elimination . . . . . . . . . . . . . . . . . . 9
5 Our Work 13
5.1 Problem Specification . . . . . . . . . . . . . . . . . . . . 13
5.2 Reducing to Max-SAT . . . . . . . . . . . . . . . . . . . . . 14
5.2.1 An Example . . . . . . . . . . . . . . . . . . . . . . . . . 15
5.3 Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
5.3.1 Expanding XOR Clauses . . . . . . . . . . . . . . . . . . 17
5.3.2 Total Number of Clauses . . . . . . . . . . . . . . . . . 18
5.4 Working with Compiler . . . . . . . . . . . . . . . . . . . . 19
6 Results 20
6.1 Result Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
7 Conclusion 24
7.1 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
Bibliography 25


[Bod07]
Marco Bodrato. Towards optimal toom-cook multiplication for univari-
ate and multivariate polynomials in characteristic 2 and 0. In Arith-
metic of Finite Fields, pages 116–133. Springer, 2007.
[Can89]
David G Cantor. On arithmetical algorithms over finite fields. Journal
of Combinatorial Theory, Series A, 50(2):285–300, 1989.
[CGPR+ 09] Maciej Ciesielski, Daniel Gomez-Prado, Qian Ren, J&;#233;r&;#233;mie Guillot, and
Emmanuel Boutillon. Optimization of data-flow computations using
canonical ted representation. Computer-Aided Design of Integrated Cir-
cuits and Systems, IEEE Transactions on, 28(9):1321–1333, 2009.
[CKA06]
Maciej Ciesielski, Priyank Kalla, and Serkan Askar. Taylor expansion
diagrams: A canonical representation for verification of data flow de-
signs. Computers, IEEE Transactions on, 55(9):1188–1201, 2006.
[Com]
Compiler optimations.
http://www.compileroptimizations.com/
index.html.
[Ger99]
Sabih H Gerez. Algorithms for VLSI design automation, volume 8.
Wiley Chichester, England, 1999.
[KO63]
Anatolii Karatsuba and Yu Ofman. Multiplication of multidigit num-
bers on automata. In Soviet physics doklady, volume 7, page 595, 1963.
25
[KZFH12]
Miyuki Koshimura, Tong Zhang, Hiroshi Fujita, and Ryuzo Hasegawa.
Qmaxsat: A partial max-sat solver system description. Journal on
Satisfiability, Boolean Modeling and Computation, 8:95–100, 2012.
[MAX10] Max-sat 2010. http://maxsat.ia.udl.cat:81/10, 2010.
[MAX11] Max-sat 2011. http://maxsat.ia.udl.cat:81/11, 2011.
[MAX12] Max-sat 2012. http://maxsat.ia.udl.cat:81/12, 2012.
[PIC] Figure of xor gate. https://asicdigitaldesign.files.wordpress.
com/2007/05/high-z_solution_02.png.
[PSD+ 99]
Robert Pasko, Patrick Schaumont, Veerle Derudder, Serge Vernalde,
and Daniela Durackova. A new algorithm for elimination of common
subexpressions. Computer-Aided Design of Integrated Circuits and Sys-
tems, IEEE Transactions on, 18(1):58–68, 1999.
[Soo] Mate Soos. Sat-solver “cryptominisat”, version 2.9. 0 (january 20, 2011).
[SS71] Doz Dr A Sch&;#246;nhage and Volker Strassen. Schnelle multiplikation
grosser zahlen. Computing, 7(3-4):281–292, 1971.
[Wik14a]
Wikipedia. Boolean satisfiability problem — wikipedia, the free ency-
clopedia, 2014. [Online; accessed 1-June-2014].
[Wik14b]
Wikipedia. Conjunctive normal form — wikipedia, the free encyclope-
dia, 2014. [Online; accessed 1-June-2014].
[Wik14c]
Wikipedia. Convolution theorem — wikipedia, the free encyclopedia,
2014. [Online; accessed 5-June-2014].
[Wik14d]
Wikipedia. Maximum satisfiability problem — wikipedia, the free en-
cyclopedia, 2014. [Online; accessed 1-June-2014].


QRCODE
 
 
 
 
 
                                                                                                                                                                                                                                                                                                                                                                                                               
第一頁 上一頁 下一頁 最後一頁 top
無相關期刊
 
系統版面圖檔 系統版面圖檔