首页
学习
活动
专区
圈层
工具
发布
首页
学习
活动
专区
圈层
工具
MCP广场
社区首页 >问答首页 >如何将非线性异或方程组转化为CNF

如何将非线性异或方程组转化为CNF
EN

Stack Overflow用户
提问于 2018-06-25 06:52:30
回答 2查看 394关注 0票数 1

我试图分析相移故障分析的琐事,并遇到了一个非线性方程组来解决。我读过关于卫星求解器和高斯消除的文章,但不幸的是,我在互联网上发现的任何一篇文章都没有说明如何处理一个含有大量变量的非线性方程组(在这里,trivium给出了288个变量)。所以我现在很难解决这些变量的问题。

EN

回答 2

Stack Overflow用户

回答已采纳

发布于 2018-06-25 22:27:56

您可以将您的问题表示为布尔门网络--一个netlist --并使用bc2cnf将其转换为CNF。您可以指示bc2cnfXCNF格式输出XOR子句,这是一种扩展的CNF格式,带有表示XOR子句的"x“子句。

隐形虫这样的卫星解算器能够读取XCNF和/或检测包含的XOR门并执行高斯消除。密码体制( Cryptominisat 据报 )已被多次用于攻击Trivium流密码。

票数 1
EN

Stack Overflow用户

发布于 2018-07-19 02:45:30

我建议看一看SMT解算器,例如Z3。使用SMT,你可以用自然的方式来表达布尔方程和不等式,而不是把一切都解释到SAT实例中。网上有大量的文档可以让你开始工作。

票数 0
EN
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接:

https://stackoverflow.com/questions/51017769

复制
相关文章

相似问题

领券
问题归档专栏文章快讯文章归档关键词归档开发者手册归档开发者手册 Section 归档