将方程转换为 cnf，以便使用 sat 求解器

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

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

Answer 1

这里有一个建议:

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

PS。您似乎正在尝试使用 SAT 求解器进行加密。 AFAIK 这对于像 MiniSat 这样的标准求解器来说效果不太好。 。不确定是否 CryptoMiniSat会更好，但最好记住，这些类型的问题历来对于 SAT 求解者来说都是困难的。