1回答
从Z3调用外部SAT求解器
z3、smt、sat
在我工作的公司，我们可以访问多个SAT Solver。我们想要分析每个SAT求解器如何影响Z3 SMT求解器的性能。
是否可以从Z3调用外部SAT求解器？如果不是，应该在哪里修改Z3以调用外部求解器？
浏览 9提问于2016-07-18得票数 1
1回答
我正在尝试用Z3解决一个带有12000+布尔变量的应用程序测试问题。我期望大多数变量在解决方案中的计算结果为false。有没有一种方法可以引导或提示Z3作为SAT求解器首先尝试“极性错误”？
浏览 0提问于2012-12-18得票数 7
回答已采纳
2回答
在Z3中使用不同的后端解算器
z3、z3py、sat-solvers、pysmt
我正在使用Z3 Python接口为我的实验创建公式。然后，我将该公式发送到Z3求解器。如果我没记错的话，Z3使用了自己的求解器！
如何在Z3py中使用不同的SAT/SMT求解器？我在CBMC (C bounded Checker)中使用的方法是:运行程序并生成一个中间DIMAC表示(在一个文件中)，然后使用该文件作为其他SAT求解器的输入。我可以在<em
浏览 2提问于2017-06-19得票数 3
1回答
Z3 SAT求解器的XOR子句
z3、xor、conjunctive-normal-form
我正在使用Z3来解决可满足性问题，包括数百个XOR子句，每个子句有22个输入。为了在DIMACS表单中编写XOR子句，我使用了Tseitin编码。到目前为止，Z3还不能设计出一个SAT解决方案。我研究过高斯消去法，但这可能没有帮助，因为XOR表达式没有相同的输入变量。
浏览 4提问于2013-01-20得票数 1
1回答
下面的Python片段演示了Z3的一种性能限制行为。如果没有push()调用，z3将在0.1s内检查公式。对于push() (没有额外的断言)，z3需要0.8s。import timef = z3.parse_smt2_file("smt-lib/QF_BV/RWS/Example_1.txt.smt2")
s = z3.Solver()
浏览 2提问于2014-10-17得票数 4
回答已采纳
1回答
关于Z3中增量式SAT的几个问题:它能被停用吗？里面用的是什么技术？
z3、z3py、theorem-proving、sat、satisfiability
我注意到，Z3在默认情况下执行增量式SAT求解(参见)：具体来说，每次使用s.add命令(在s是一个求解者)时，它意味着将该子句添加到s，但它不会忘记您以前学过的所有知识。第一个问题：非增量式SAT解决方案能在Z3中完成吗？那就是，以某种方式“停止”增量解决方案。这意味着什么？我们正在为每一个扩大的公式创建一个新的求解器？也就是说，一旦我们得到一个模型，我们就把被否定的模型附加到相同的求解器上。
虽然这是在“强迫”<
浏览 10提问于2022-01-13得票数 0
回答已采纳
1回答
将子句直接添加到z3解决程序
c++、c、z3、sat
我有一个美国国际集团(和-逆变图)，我不断修改，其可满足性，我需要检查的增量方式使用Z3。我可以生成美国国际集团的CNF代表，理想情况下，我希望直接将这些条款提供给求解者，并从我的代码中反复调用它。我是否可以通过C/C++ API直接向Z3解决程序添加子句(或AIG)？
浏览 2提问于2016-12-20得票数 0
回答已采纳
1回答
是否可以使用Z3，但不包括SAT？
z3、smt
Z3支持SMT-lib set-logic语句，以限制到特定的片段。例如，在使用(set-logic QF_LRA)的程序中，启用了无限定符的线性实数运算。如果启用了多个理论，对我来说，需要SAT是有意义的。然而，我不清楚是否有可能启用单个理论并保证SAT永远不会运行，从而将Z3纯粹简化为该单个理论的求解器。这将是有用的，例如，声称一个工具遵守给定理论的求解器的特定性能界限。
有没有办法在SMT-lib中或直接在Z3中做到这一点？或者
浏览 31提问于2021-03-03得票数 0
回答已采纳
2回答
查询:当Z3返回未知状态时，我们可以使用z3 Python获得部分模型吗？
python、z3、smt、z3py、z3-fixedpoint
是否有一种方法可以从z3获得部分模型，即使状态为unknown
x, y, z = Reals('x y
浏览 18提问于2020-09-02得票数 0
回答已采纳
1回答
除了Z3，还有其他支持弦理论的MAX解程序吗？
z3、smt
SMT求解器Z3引入了一个扩展()来支持优化目标的求解。我正在寻找其他SMT解决方案，支持软断言和弦理论。
我所知道的唯一支持软约束的SMT解决方案是SMT -鼠和SMT的巴塞罗那。
浏览 28提问于2022-03-20得票数 0
2回答
使用Z3从受限空间进行采样
z3、constraint-programming
我尝试过Z3，它似乎能够告诉我空间是否是非平凡的(即约束是否可满足)，但我看不到从空间中获取示例的方法，除非我正在最小化或最大化某些东西。
我是不是错过了什么，或者这不是Z3的用途？
浏览 2提问于2016-08-30得票数 4
回答已采纳
下面的SMT2实例可以被解决(它是UNSAT)，但是如果我使用qfnra求解器，结果是未知的。lv_n_8_1 (<= lv_n_1_1 10)) (= lv_n_1_1 NONDET_INT_32_1);(check-sat-using(then simplify sat qfnra))这一切为什么要发生？
浏览 2提问于2015-10-20得票数 1
回答已采纳
1回答
你好，我是Z3 SMT解决方案的新手。我知道您可以通过使用相关的API以编程方式调用Z3。但是，我想用Z3 SMT解决程序做以下事情：while ((check-sat) returns sat)最后，在求解公式后，如何让Z3将结果保存到一个输出文件中
浏览 3提问于2012-02-08得票数 0
回答已采纳
1回答
3-SAT和CNF之间的差异
algorithm、boolean、z3、sat
我试图用Z3定理求解器来解决SMT语法中的SAT问题，需要用CNF编写命题公式，并求出满意的值。我知道这些概念，但我不理解实现。你能给出用Z3定理证明器解决3-SAT问题的例子吗？谢谢
浏览 9提问于2021-12-05得票数 0
1回答
Z3卫星解算器的随机种子
z3、satisfiability
我使用Z3作为SAT solver来解决一个以CNF/DIMACS格式编码的棘手的可满足性问题。将输入随机化以增加找到解决方案的机会是否有意义：
对于Z3来说，排序/随机化对于我的示例来说并不是很有希望的，因为它可能没有代表性。我没有发现影响Z3的SAT模块的随机种子命令行参
浏览 4提问于2014-09-13得票数 1
回答已采纳
1回答
(assert (= c (ite b 1 0)))
结果是未知的。(assert (= b false))
Z3现在能够解决这个实例为什么Z3可以解决第二个实例，而不能解决第一个实例，即使第一个实例可以简化为第二个实例？在寻找问题的时候，我发现了一些非常奇怪的东西。a 0.0))
浏览 0提问于2015-10-18得票数 3
回答已采纳
非常有趣的是，是什么方法帮助Z3在smtcomp的QF_BV部分获得了第一名。
浏览 3提问于2011-09-01得票数 4
回答已采纳
我正在对UFBV查询运行Z3。当前查询包含2个调用check-sat。如果我把push 1放在check-sat后面，Z3会在30秒内完成查询。如果我根本不放置任何push 1，因此有两个调用check-sat，它们之间没有任何push 1，那么Z3在200秒内解决了它。有意思的。有没有什么特别的原因，或者只是巧合？
浏览 0提问于2012-02-03得票数 4
回答已采纳
1回答
Z3:提取存在模型值
z3、smt、theorem-proving
我正在使用Z3的QBVF求解器，想知道是否可以从存在断言中提取值。然后，我可以说：(get-model)sat在每种情况下，Z3都正确地抱怨没有这样的常量。显然，从对(check-sat)调用的响应中可以看出，Z3具有该信息。有没有办法通过get-value或其他机制自动访问存在值？
谢谢.
浏览 1提问于2011-08-25得票数 4
1回答
当使用z3获取该公式集的真值赋值时，是否存在某种方法来设置变量的优先级？我的意思是，如果优先级是a>b>c，那么在搜索过程中，z3首先假设a为真，如果a不可能为真，则假定b为真，依此类推。换句话说，如果z3给出了一个真值分配:不是上述优先级下的a，b，c，这意味着a不可能为真，因为与b相比，a是高优先级的。希望我能清楚地描述这个问题。
浏览 0提问于2013-01-09得票数 5
回答已采纳
云服务器
对象存储
ICP备案
云点播
语音识别
腾讯云开发者
Copyright © 2013 - 2026 Tencent Cloud. All Rights Reserved. 腾讯云 版权所有
深圳市腾讯计算机系统有限公司 ICP备案/许可证号：粤B2-20090059 
粤公网安备44030502008569号
腾讯云计算（北京）有限责任公司 京ICP证150476号 | 京ICP备11018762号