2

因此，我必须将我的一位同事设计的一些方程转换为 cnf 文件格式，以便与一些开源 sat 求解器一起使用。

方程是：

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

我将不胜感激有关如何将这些转换为 cnf 文件格式的任何信息，包括任何参考链接。也将不胜感激有关以 cnf 文件格式指定上述约束的一些帮助。

4

1 回答 1

2

这里有一个建议：

  1. 将数学运算（GF(16) 中的加法、乘法等）编码为电路。如果你学过数字逻辑设计课程，你就会知道如何去做。如果没有，那就有点难了。如果您需要更多信息，请告诉我您的背景，我会尽力提出具体建议。
  2. 使用Tseitin 变换将电路转换为 CNF。

PS。似乎您正在尝试使用 SAT 求解器进行加密。AFAIK 这不适用于像MiniSat这样的标准求解器。不确定CryptoMiniSat是否会更好，但请记住，这些类型的问题传统上对于 SAT 求解器来说很难。

于 2014-03-03T02:13:11.097 回答