基於 Max-SAT 求解器的二元體表達式簡化工具

Abstract

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