1回答
将公式转换为cnf python
、、、、
我想将公式转换为CNF。有没有库可以做到这一点？这是我的代码。我创建了许多函数来将任何(a或b)转换为CNF格式。
但如果有许多命题，这将很难(a > b) & (c & d)或不(F)。
浏览 13提问于2018-12-16得票数 3
回答已采纳
是否可以将SMT-LIBv2格式的包含设置逻辑QF_AUFBV的输入文件转换为CNF？如果是这样的话，我该如何使用Z3命令行功能来完成这项工作呢？更新:我还需要将变量从SMT-LIBv2实例映射到CNF DIMACS文件作为注释。使用Z3可以吗？
浏览 0提问于2015-09-08得票数 1
给定CNF中的Z3公式，可以使用Z3Py将其转换为列表表示吗？我想这样做是为了更容易地访问和操作文字。如果Python是一种函数式语言，我可能会做类似的事情 match fm with match fm with
| Or(P,Q) -> clause2list(P) + clause2list(Q
浏览 4提问于2016-06-07得票数 0
回答已采纳
1回答
有没有办法使用z3将公式转换为CNF (使用Tseitsin风格的编码)？我正在寻找类似simplify命令的东西，但要保证返回的公式是CNF。
浏览 0提问于2012-06-12得票数 4
回答已采纳
1回答
结合范式的书写条件
、、、
合合范式(CNF)是命题公式的一种标准化表示法，它规定每一个公式都应写成一个断点连词。每个布尔公式都可以转换为CNF。例如：在CNF中有如下表示：用CNF编写条件词是编程的最佳实践吗？
浏览 7提问于2016-04-01得票数 2
回答已采纳
DNF SAT是多项式时间，CNF SAT是NP完全的.如果我有一个布尔骨架已经在DNF中的一阶公式，z3会意识到这一点吗?还是它会盲目地将公式转换为CNF，由CDCL来求解？
浏览 2提问于2014-06-15得票数 1
回答已采纳
这就是我的问题:我不知道如何将∃m : m ∈ N转换为CNF公式。我只是理解公式∃x(A(x)vB(X))。
浏览 29提问于2020-12-14得票数 0
在急切的SMT求解器中，SMT公式被编码为可等量化的布尔公式，该公式被馈送到SAT求解器。通常，对于QF_UF公式，未解释的函数通过Ackermann约化或Bryant约化来约简，然后用等值图方法构造可等量化的布尔公式。因此，我想知道是否有可能调用现有的SMT求解器来获得给定QF_UF公式的可等量化的布尔公式，而不会破坏求解器的低级实现。例如，Z3有一些策略来转换输入问题(如tseitin-cnf和elim-term-ite)，是否有这样的转换策略？
浏览 32提问于2017-07-13得票数 1
对于更大的公式，似乎存在性能问题，这就是为什么我想查看picosat，看看它是否是一个更快的替代方案。我现有的python代码用z3语法生成一个命题公式：from pycosat import solve, itersolve
#1sols = list(itersolve(clauses, vars=nvars))print sols您推荐什么简单的解决
浏览 4提问于2013-10-23得票数 5
1回答
我知道将公式转换为CNF的4条规则，但我不太确定如何将它们应用到这个公式((x )^ to ) ->w中。
有人能帮我一把解释一下吗？谢谢!
浏览 6提问于2015-07-21得票数 0
回答已采纳
为此，我有使用CNF文件的工具。我想转换Minizinc文件(mzn或Flatzinc格式)，并将其转换为CNF。 我了解到Picat能够在加载约束后“转储”CNF文件。我修改了模块fzn_picat_sat.pi以“转储”CNF文件。所以，我所做的就是使用mzn2fzn将迷你文件转换为Flatzin型文件，然后尝试使用我的(稍微) fzn_picat_sat.pi的modified version将其转换为
浏览 18提问于2020-08-19得票数 5
回答已采纳
1回答
无限制表格至限制表格(CNF)
、、、、
我需要把不受限制的命题公式转换成CNF，然后转换成3-SAT。我知道把公式转换成连接范式的重写规则。实际上，我试图证明，不受限制的公式可以转换为受限形式，两者的解决方案是相同的。因此，我写任何不受限制的命题公式，把它转换成CNF，然后再转换成3-SAT(手工)，这样我就可以显示类似的结果。因此，我需要USAT-org和USAT-转换，其中org是不受限制的公式，在3-CNF中转换为SMT语法(SMT-LIB2 2文件
浏览 9提问于2021-12-05得票数 0
2回答
我正在使用Python，我想模拟C/C++强制转换对整数值的影响。例如，如果我有8位的无符号数字234，我想要一个公式将其转换为-22 (有符号转换)，并使用另一个函数将-22转换为234 (无符号转换)。 我知道numpy已经有了这样的函数，但我想避免它。
浏览 25提问于2020-04-14得票数 1
回答已采纳
我正在使用CNF4.0中的以下代码片段将公式转换为z3。simplify true tseitin-cnf)(goals ;)
我假设goal后面的每个表达式都是CNF的一个子句，也就是说
浏览 2提问于2012-06-19得票数 4
回答已采纳
我从表1中生成表2
采用以下公式：如何将1转换为true，将0转换为false，并设置一个筛选器仅显示true在相同公式中的行？
浏览 15提问于2021-12-08得票数 0
回答已采纳
1回答
是否有任何方法将DNF公式转换为ILP约束？例如，假设我有以下公式：如何把它写成ILP？我知道它可以被转换成相等的CNF表达式，然后转化为ILP，但在子句/变量的大小上可以是指数型的。
浏览 2提问于2016-03-07得票数 0
回答已采纳
云服务器
ICP备案
实时音视频
对象存储
即时通信 IM
腾讯云开发者
Copyright © 2013 - 2026 Tencent Cloud. All Rights Reserved. 腾讯云 版权所有
深圳市腾讯计算机系统有限公司 ICP备案/许可证号：粤B2-20090059 
粤公网安备44030502008569号
腾讯云计算（北京）有限责任公司 京ICP证150476号 | 京ICP备11018762号