我一直在尝试使用 Cryptominisat（类似的东西）来制定对 Piccolo 的攻击，这是一种类似于 AES 的轻量级分组密码。
方程是这样的：
Z= z1|z2|...|z16, 1<= i<=16
那么，ui= (1+z(4i-3)) ^ (1+ z(4i-2)) ^ (1+z(4i-1)) ^ (1+ z(4i)), 1<=i <=4
那么，(1+u1) V (1+u2) V (1+u3) V (1+u4) =1；ui + uj=1, i<=i<=j<=4
我需要一些关于下一步的帮助。我已经准备好用于攻击和解密的 CNF 方程，我真的需要关于如何将其与 sat 求解器一起使用并将其放入 CNF 文件格式的帮助。我一直在寻找整个互联网，但在任何地方都没有明确的方法。任何帮助，将不胜感激。如果需要更多信息，请随时询问。我需要把上面的方程放在一个 cnf 文件中。
由于涉及的方程式非常复杂（还有更多），因此 cnf 文件及其工作的一些参考或示例会很棒。