Преобразование уравнений в cnf для использования спутниковых решателей

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

Mix-столбцы:

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) и т. Д.) Как схемы. Если вы прошли курс по дизайну цифровой логики, вы будете знать, как это сделать. Если нет, это будет немного сложно. Если вам нужна дополнительная информация, скажите мне, каково ваше прошлое, и я постараюсь внести конкретные предложения.
2. Используйте преобразование Цейтин, чтобы преобразовать схему в CNF.

PS. Похоже, что вы пытаетесь сделать крипто, используя SAT решатель. AFAIK, это не очень хорошо работает со стандартными решателями, такими как MiniSat. Не уверен, что CryptoMiniSat будет лучше, но было бы хорошо иметь в виду, что эти типы проблем традиционно были трудными для решателей SAT.