Как преобразовать систему нелинейных уравнений XOR в CNF

Question

Я пытаюсь проанализировать анализ фазовых сдвигов в тривиуме и наткнулся на систему нелинейных уравнений для решения. Я читал о спутниковых решателях и исключении Гаусса, но, к сожалению, ни одна из статей, которые я нашел в Интернете, не показывает, как справляться с нелинейной системой уравнений с большим числом переменных (здесь тривиум дает 288 переменных). Так что теперь я застрял в том, как решить эти переменные.

Answer 1

Я бы порекомендовал взглянуть на SMT решатель, например. Z3. С помощью SMT вы можете выразить булевы уравнения и неравенства естественным образом, вместо того, чтобы обрабатывать все до экземпляра SAT. В Интернете достаточно документации, чтобы начать работу.

Answer 2

Вы можете выразить свою проблему как сеть логических элементов - список цепей - и использовать bc2cnf , чтобы перевести ее в CNF.Вы можете указать bc2cnf выводить XOR предложения в формате XCNF, расширенный формат CNF с предложениями "x", обозначающими XOR предложения.

SAT-решатели, такие как cryptominisat способны читать XCNF и / или обнаруживать содержащиеся XOR вентили и выполнять устранение по Гауссу.Cryptominisat по сообщениям использовался несколько раз для атаки на Trivium потоковый шифр.