使用座標解算器將等式轉換爲cnf

Question

因此，我必須將一些由我的同事設計的方程轉換爲cnf文件格式，以便與一些開源座標解算器一起使用。

的公式爲：

S盒：

y1= 1+x1+x2+x4+x1x2 

y2= 1+x1+x2+x3+x3x2 

y3= 1+x1+x4+x1x2+x1x3+x2x3+x3x4+x1x2x3 

y4= x1+x2+x3+x1x3+x1x4+x2x4+x3x4+x1x2x3+x2x3x4 

混合柱：

Y1= 2.X1+3.X2+1.X3+1.X4 

Y2= 1.X1+2.X2+3.X3+1.X4 

Y3= 1.X1+1.X2+2.X3+3.X4 

Y4= 3.X1+1.X2+1.X3+2.X4 

. denotes multiplication in GF(2^4) with x^4+x+1 being the irreducible polynomial. 

有關攻擊，

Z= z1|z2|...|z16, 1<= i<=16 

Then, ui= (1+z(4i-3))^(1+ z(4i-2))^(1+z(4i-1))^(1+ z(4i)), 1<=i<=4 

Then, (1+u1) V (1+u2) V (1+u3) V (1+u4) =1; ui + uj=1, i<=i<=j<=4 

我會很感激的任何有關如何轉換這些t的信息cnf文件格式，包括任何參考鏈接。還有一些關於如cnf文件格式指定約束的幫助也將被讚賞。

Answer 1

這裏是一個建議：

1. 編碼的數學運算（加法，乘法在GF（16）等）作爲電路。如果你已經完成了數字邏輯設計課程，你會知道如何做到這一點。如果不是，那會有點困難。如果您需要更多信息，請告訴我您的背景是什麼，我會嘗試提出具體建議。使用Tseitin transformation將電路轉換爲CNF。

PS。看起來你正在嘗試使用SAT求解器來進行加密。 AFAIK對於像MiniSat這樣的標準解算器來說效果不佳。不知道CryptoMiniSat會更好，但記住這些類型的問題傳統上很難解決SAT問題。