1

我正在尝试用琐碎的方式分析相移故障分析，并遇到了一个非线性方程组来求解。我读过关于 sat-solvers 和 Gaussian 消元的文章，但不幸的是，我在互联网上找到的文章都没有显示如何处理具有大量变量的非线性方程组（这里 trivium 给出了 288 个变量）。所以我现在几乎被困在如何解决这些变量上。

4

2 回答 2

1

您可以将您的问题表达为布尔门网络 - 一个网表 - 并使用bc2cnf将其转换为 CNF。您可以指示bc2cnf以格式输出XOR子句XCNF，这是一种扩展CNF格式，其中“x”子句表示XOR子句。

像cryptominisat这样的SAT 求解器能够读取XCNF和/或检测包含的XOR门并执行高斯消除。据报道， Cryptominisat已被多次用于攻击Trivium流密码。

于 2018-06-25T22:27:56.763 回答
0

我建议看一下 SMT 求解器，例如 Z3。使用 SMT，您可以以自然的方式表达布尔方程和不等式，而不是将所有内容都分解为 SAT 实例。有大量在线文档可以帮助您入门。

于 2018-07-19T02:45:30.030 回答