我有一个庞大的线性实数约束集需要解决，并且我正在逐步地将它们提供给求解器。Z3似乎总是在一段时间后被卡住。Z3是否会在内部改变其解决约束的策略，例如放弃单纯形算法并尝试其他算法，等等。或者我必须显式地指示Z3这样做？我正在使用Z3py。
浏览 1提问于2016-07-21得票数 0
回答已采纳
1回答
然而，对于真实的案例，它可以消除。(当i和k都是实数时)对于整数来说，消除量词是不是更难？我知道在量词消除后，这些约束被简化为线性约束。
我认为z3在检查可满足性之
浏览 1提问于2012-05-04得票数 5
回答已采纳
1回答
因此，我正在尝试使用z3解决一个调度问题。我有一组需要完成的工作和一组能够完成这些工作的资源。约束本身并不复杂，但我向求解器抛出的约束的数量有数千个，而且可能会增加10倍。
因此，我遇到的一个问题是，Z3似乎不能确定它如何尝试解决相同的问题(但在不同的运行期间)。然后我经常做的是终止当前的运行并重新启动，然后它
浏览 16提问于2018-08-31得票数 2
1回答
我们遇到了性能问题，我认为这是Z3中处理非线性算术的部分。这里有一个简单的具体的Boogie示例，当使用Z3 (版本4.1)验证时，需要很长时间(大约3分钟)才能完成。、整数变量的范围假设以及(未知)整数值的乘法引起的。最后的断言应该是不可证明的。Z3似乎有办法实例化许多术语，而不是很快失败，因为它的内存消耗相当快地增长到大约300MB，在这一点上它放弃了。我想知
浏览 2提问于2012-09-20得票数 5
回答已采纳
1回答
我想在z3py中断言“某些东西不能存在”的约束。我试着用“不存在((.)”。下面是一个简单的例子。我想为a和b找到一个赋值，这样这样的c就不存在了。from z3 import *
a = Int('a')c = Int('c')
s.add(Not(Exists(c,And(c>0,c<5,a*b+c==10))))
print s.check()
浏览 2提问于2015-07-12得票数 0
回答已采纳
我知道带乘法的整数理论通常是不可判定的。然而，在某些情况下，Z3确实会返回一个模型。我很好奇这是怎么做到的。这与reals上的非线性算术的新决策程序有关吗？Z3为乘法查询返回模型的特定实例(例如，有限模下的整数等)是否已被识别？任何帮助都是非常感谢的。
浏览 3提问于2012-12-16得票数 33
回答已采纳
1回答
我有两个使用reals的SMT2-Lib脚本，它们在道德上是等价的。唯一的区别是，一个也使用位向量，而另一个不使用。下面是同时使用实数和位向量的版本：(set-option :produce-models true) (let ((s10 (ite (>= s9 s3) #b1 #b0)))(get-model)
浏览 2提问于2012-10-17得票数 4
回答已采纳
如果这个问题措辞不当，我很抱歉，但我试图使用z3 (在python中有语言绑定)来求解一些非线性方程，但不幸的是，qfnra-nlsat和通用求解程序都无法解决以下系统，除非给出了a、b和c：我是CSP的新手，所涉及的理论背景，抱歉，如果这是一个愚蠢的问题，但我想知道这种非线性是超出(经验上)可由z3解决，还是我没有正确地使用它？谢谢!不过，如果我在下面再加上一个约束，那就是一个后
浏览 2提问于2016-01-29得票数 0
我在Python-API中使用Z3。我正在设置一组相当大的线性算术约束。如果我不使用任何push/pop，一切都可以正常工作。但是当我只是插入一个在s.check()之前的某个地方，s.check()会无休止地运行。只有在不使用pop的情况下使用push才能正常工作。是否有任何已知的问题
浏览 3提问于2013-06-18得票数 2
4回答
我有一个很大的布尔公式要解，由于密文的原因，我必须在这里粘贴一个图像：另外，我已经有了一个函数area来测量4个整数的维数：area(c,d,e,f)=|c−d|×|e−f|
我想做的不仅仅是计算公式是否可满足:我正在寻找一个最优的6元组(a,b,c,d,e,f)，它使大公式TRUE和area(c,d,e,f)大于或等于任何其他也满足该公式的6元组的维度。换句话说，找到大公式的Max(area(c,d,e,f)) subj
浏览 0提问于2011-12-14得票数 1
回答已采纳
1回答
我想要创建一个约束，以确保一个真正的值被量化为一些滴答值。TICK = 0.5solve(x % TICK == 0)还有别的解决办法吗？
浏览 0提问于2021-11-04得票数 1
回答已采纳
1回答
我正在尝试解决包含数千个变量的公式。这些公式的主要部分是线性的，从我的角度来看，z3正在以令人难以置信的速度消化它们。然而，很少有约束会引入一些非线性。然后，计算时间从几分钟增长到经过几天的计算后无法得到解决方案。
我认为尝试使用位向量会很有趣，但对于那些在此过程中失去一些精度的非线性约束，但
浏览 2提问于2015-07-09得票数 1
我正在修改一个使用Z3 (特别是Python )来解决位向量约束的工具。我需要使用一个特定的外部SAT解决程序，而不是内部的Z3解决程序，所以我首先使用的是这个策略。Then('simplify', 'bit-blast', 'tseitin-cnf')
之后，我可以相对轻松地将子句转储到DIMACS文件中。问题是将结果<
浏览 5提问于2015-06-18得票数 5
回答已采纳
1回答
Z3:复数？
、、、、
我一直在搜索z3是否支持复数，并发现了以下内容：他提供了编码(我的意思是，我们可以在机器上测试)，在那里我们可以求解方程x^2+2=0。*I
sat结果是有意义的，因为这个方程在模拟复数理论(作为代
浏览 7提问于2021-11-16得票数 1
回答已采纳
declare-var n Int)(assert (not (= b (^ a (+ n 1)))))它几乎是瞬间返回未知的。
浏览 1提问于2016-04-23得票数 1
回答已采纳
2回答
Z3或Z3Py中的假设
、、、
有没有一种方法可以在Z3 (我使用的是Z3Py库)中表达假设，这样引擎就不会检查它们的有效性，而是像定理证明一样将它们作为基本理论？用Z3Py编码，如下所示：assumption1 = ForAll(t，f1(t) = f2(t))。当前代码的问题是我的断言集非常大，并且我使用量词(我试图证明实时系统的可满足性)。如果
浏览 27提问于2016-03-23得票数 2
1回答
我注意到python的没有正确地报告涉及我正在处理的指数问题的可满足性。具体来说，它报告说，在我知道有效答案的情况下，没有找到任何解决办法--除非我增加了有效“告诉它答案”的约束。在下面的代码中，我要求它找到q和m这样的q^m == 100。当然，有了约束0 <= q < 100，您就有了q=10, m=2。但是使用下面的代码，它报告了“找不到解决方案”(raise Z3Exceptio
浏览 2提问于2020-07-16得票数 0
回答已采纳
1回答
我正在努力学习Z3，下面的例子使我感到困惑：a = Int("a")print(solve(2**a <= b))我希望它返回"a = 1，b= 2“，但它却返回”未能解决“。为何不能解决呢？
用Z3中的幂和对数进行计算是可能的吗？例如，如何找到数字(日志基
浏览 4提问于2021-12-09得票数 2
回答已采纳
2回答
理想情况下，我会想做在Modelica中可以做的事情，写出方程并让求解者来处理它。经过一些研究，我发现的解决者似乎做了我想做的事情。我想出了这个(这看起来是我想要优化的</e
浏览 12提问于2016-06-03得票数 8
回答已采纳
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
云直播
对象存储
腾讯会议活动推荐
腾讯云开发者
