Что касается SAT Solvers и cnf-файлов

Question

Я пытался использовать 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 для атаки и дешифрования, мне действительно нужна помощь, как использовать это с спутниковым решателем и перевести в формат файла CNF. Я искал по всему интернету, но нигде не дано четкого метода. Любая помощь будет оценена. Если вам нужна дополнительная информация, пожалуйста, не стесняйтесь спрашивать. Мне нужно поместить вышеуказанные уравнения в файл cnf.

Поскольку используемые уравнения довольно сложны (их больше), некоторые ссылки или примеры для файлов cnf и их работа будут потрясающими.

Answer 1

Эта спецификация формата CNF может помочь вам:

http://people.sc.fsu.edu/~jburkardt/pdf/dimacs_cnf.pdf

На этой странице есть ссылки на образцы файлов:

http://people.sc.fsu.edu/~jburkardt/data/cnf/cnf.html