在密碼學領域的演算法實作中,程式的效能是實作時的重要考量,為了提高效
能,設計者無法使用現有的高階程式語言實作所有的演算法,而需要在關鍵運算
上使用低階語言(如組合語言)來描述,使程式整體的效能達到目標。
我們的目標是將二元體中的表達式自動地轉換為低階語言程式碼,而且此程式
碼的效能比直接簡單的轉換方式來的好。
在此研究中,我們將二元體表達式的簡化問題轉換為 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].