1回答
我正在试验优化使用Z3来证明一阶理论的事实.目前，我在Python中指定了一阶理论，将量词放在那里，并将所有子句连同证明目标的否定一起发送给Z3。我有以下的想法，我希望能优化结果:我只想把理论中的公式发送给Z3，这些公式与证明目标相关。我不打算详细讨论这个概念，但我认为直觉很简单:我的理论是公式的结合，我只想发送可能影响证明目标的真值的连词。我的问题是:这能导致效率的提高吗，还是Z3已经使用了类似的方法？我想不会，因为我不认为Z3总是假设最后的断言是证
浏览 4提问于2012-12-21得票数 1
回答已采纳
1回答
一个非常类似的问题已经被问到了，但是我找不到以下问题的答案。使用所有量词都可以很容易地表示线性最大化问题：像上面这样的查询可以提交给z3。因此，我想问一问，当z3看到一个LP问题时，它是否聪明到能够识别一个LP问题，它是否会应用一种单纯形方法来消除所有量词？
浏览 3提问于2014-06-12得票数 0
回答已采纳
1回答
我不习惯使用Z3的优化特性，我通常只做证明；这就是为什么我几乎确定错误是我的…… 现在，我在python中的check-sat语句上使用了一个循环，并迭代地添加了一个约束(r > result)。(define-fun j () Int; (define-fun r () Int; (define-fun t () Int;) $ z3--version
Z3 version 4.8.7 - 64 bit
浏览 47提问于2021-10-13得票数 0
2回答
Z3优化的超时
、、、、
如何为z3优化器设置超时，以便在时间耗尽时为您提供最知名的解决方案？from z3 import *# Hard Problemprint(s.model())
后续问题，你能把z3设置为随机爬山，还是它总是执行一个完整的搜索
浏览 5提问于2020-03-25得票数 3
回答已采纳
1回答
我试图使用z3py作为优化求解器，最大限度地提高从一张纸上切出的长方体的体积。python提供了优化()对象，但使用它似乎不可靠，给出的解决方案显然是不准确的。from z3 import *w = Real("w")v = Real("v")width = 63.6
浏览 0提问于2019-06-27得票数 4
回答已采纳
4回答
我想知道SMT求解器是否可以帮助解决这个问题。我了解到Z3支持quantifiers，并且能够判断布尔表达式是否可满足。但问题是，Z3是否可以帮助找到函数area的最优解。
有谁知道吗？任何关于SMT求解器，Z3或其他算法的评论将不胜感激…
浏览 0提问于2011-12-14得票数 1
回答已采纳
我想我在某处读到过，Z3有一些选项可以返回具有“最小”值的模型，例如给定如下内容Z3会返回2。我可以发誓我最近看到了一些关于这个的引用，但我现在找不到了。有人能证实这一点吗？
浏览 0提问于2014-11-14得票数 1
我想用Z3来优化一组方程。这里的问题是，我的方程是非线性的，但最重要的是，它们确实有三角函数。在z3中有没有办法解决这个问题呢？我正在使用z3py应用编程接口。
浏览 4提问于2018-07-20得票数 2
优化不应该也能找到解决方案吗？(显然，在这个场景中只有一个)from z3 import *
vy0, y0 = Reals("vy0 y0") # initial velocity, initial position
浏览 0提问于2018-05-13得票数 1
回答已采纳
我正在尝试从商业求解器转移到Z3来解决大整数可满足性问题。我们的商业求解器花了1353秒来解决这个大问题。我们的商业求解器实际上是一个优化器，这是一个混合整数优化问题。该问题转化为一个具有5,093,121个变量，9901个约束，63,450,472个零，5,093,120个整数的整数问题，并在4690次迭代中得到解决。然而，这是一个简单的应用程序测试问题，所以我希望将其转移到Z3上，并抛弃商业优化
浏览 20提问于2019-11-30得票数 1
回答已采纳
我正在尝试使用z3 smt求解器将值分配给受约束的变量。除了硬约束，我还有一些软约束(例如a != c)。我希望能够使用assert指定硬约束，并将软约束指定为soft-assert，如果我使用(check-sat)解决问题，则可以做到这一点。
浏览 20提问于2019-12-03得票数 3
回答已采纳
我使用GHC版本8.0.2和堆栈版本1.5和SBV版本7.3，我使用Z3作为我的解决程序，它是在MacOS上运行的4.5.1 64位版本。
调用sat和prove按预期工作。有什么想法吗？谢谢!
浏览 1提问于2017-09-20得票数 1
回答已采纳
1回答
定理证明工具z3花了很多时间来解决一个公式，我相信它应该能够很容易地处理。为了更好地理解这一点，并可能优化我对z3的输入，我想看看z3在求解过程中生成的内部约束。从命令行使用z3时，如何打印z3为其后端求解器生成的公式？
浏览 1提问于2012-10-28得票数 7
回答已采纳
1回答
我正在尝试优化从我的模型中生成的z3 python输入。我能够在15k约束的模型上运行它(200个状态)，然后z3停止在合理的时间内完成(<10分钟)。是否有一种方法来优化从我的模型生成的约束？
浏览 3提问于2013-01-08得票数 3
以以下问题为例:有三个连续点A、B和C，其中A和C分别固定为0和200。确定B的位置，B - A >= 10，C - B >= 15，以及我们的优化目标是minimize(C - B)。这个问题的解决方案应该是B = C - 15 = 200 - 15 = 185。
未跟踪代码在下面给出了正确的解决方案。问题来了。::implies(ctx.bool_const("t0"), ctx.int_const("A") == 0), 1);，“强制”优化器达到
浏览 0提问于2020-08-14得票数 2
回答已采纳
1回答
我使用Z3来解决线性优化问题，但随着变量和约束的增加，求解时间变得难以承受。未来，变量数量约为35940个，约束条件可能超过十万个。有没有办法提高速度？from z3 import *cost=Int('cost')
set_option(max_args=1000000
浏览 4提问于2019-08-19得票数 1
在使用z3优化求解器时，需要模型的边界，特别是约束条件复杂。我可以在Z3 python api中找到函数upper和lower，但不能用于Java api。您能举一些例子来说明如何在Z3 java api中获取模型边界吗？
浏览 26提问于2020-08-16得票数 0
回答已采纳
我在z3 shell和java api中都尝试了相同的假设。declare-const x (_ BitVec 32))
(check-sat)在z3外壳中，解决方案是:x=9，但在z3应用程序接口中，解决方案是:x= 0x80000000在我的应用程序中，我更喜欢外壳结果。但通常Z3会给我一些非常大的值，看起来像是随机值。
浏览 0提问于2016-11-08得票数 1
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
腾讯会议
云直播活动推荐
腾讯云开发者
