我正在尝试分析Trivium中的相移故障分析，并遇到了一个非线性方程组来求解。我读过关于卫星求解器和高斯消除的文章，但不幸的是，我在互联网上找到的文章都没有展示如何处理具有大量变量的非线性方程组(这里trivium给出了288个变量(。所以我现在几乎被困在如何解决这些变量上。
您可以将问题表示为布尔门网络(网表(，并使用bc2cnf将其转换为CNF。您可以指示bc2cnf以XCNF格式输出XOR子句，这是一种扩展的CNF格式，其中"x"子句表示XOR子句。
像cryptominisat这样的SAT求解器能够读取XCNF和/或检测包含的XOR门并执行高斯消除。据报道，Cryptominisat已被多次用于攻击Trivium流密码。
我建议看看SMT求解器，例如Z3。 使用 SMT，您可以自然地表达布尔方程和不等式，而不是将所有内容都分解为 SAT 实例。 网上有大量文档可以帮助您入门。