我一直在尝试使用Cryptominisat(类似的东西)来制定对Piccolo的攻击，Piccolo是一种轻量级分组密码，类似于AES。
方程是这样的:
Z = z1 | z2 |…|z16, 1<= 1<= 16
然后,ui = (1 + z(4我))^ (1 + z(4我2))^ (1 + z(4张))^ (1 + z(我)),1 & lt; = i<= 4
,(1+u1) V (1+u2) V (1+u3) V (1+u4) =1;
关于下一步我需要一些帮助。我已经准备好了攻击和解密的CNF方程，我真的需要帮助，如何使用sat求解器并将其放入CNF文件格式。我一直在网上找，但没有明确的方法给出任何地方。任何帮助都会很感激。如果需要更多的信息，请随时问我。我需要把上面的方程式放在一个cnf文件中。
由于所涉及的方程相当复杂(还有更多)，一些cnf文件的参考或示例及其工作将非常棒。
这个规范的CNF格式可能会对您有所帮助:
http://people.sc.fsu.edu/jburkardt/pdf/dimacs_cnf.pdf
本页有示例文件链接:
http://people.sc.fsu.edu/jburkardt/数据/cnf cnf.html