smt 相关问题

可满足性模数理论（SMT）是逻辑公式的决策问题，与经典的一阶逻辑中表达的背景理论的组合相等。

在 Z3 求解器中使用封闭世界假设求解约束

我正在使用Python中的Z3求解器解决约束满足问题，我需要解决以下形式的约束： ForAll([x, y], 暗示(And(情况(x), 情况(y)), And(动作(...

python z3 solver smt z3py

回答 1 投票 0

Z3 来解决一个难题（8 块瓷砖）吗？

我试图从以下描述中解决问题，这是我的代码：我的想法如下。空白空间表示为 1524。在每一步 s 中，一个方块都会移动到那个空的空间中......

smtp z3 smt z3py

回答 1 投票 0

在给定一组约束的情况下，cvc5 是否能够最小化或最大化表达式？

其他数学求解器，例如 z3 或 cplex，能够求解具有多个约束的数学模型，目的是最小化/最大化表达式，例如： a+b=10； 2<=b<=6

java mathematical-optimization solver smt cvc4

回答 1 投票 0

Z3-Python 中的泰勒展开式三角函数

我需要在 Z3 中设计一个余弦（和正弦）函数，但这通常很困难且无法确定（例如，请参阅如何在 Z3 Python 中使用内置三角函数？）。不过，我还好

z3 smt z3py

回答 1 投票 0

如何在 Z3 Python 中使用内置三角函数？

我想做一些类似的事情：Exists y。 0<=cos(y)<=1., which could return a model e.g., y:=50. Is this possible in Z3? I know SMT solvers overall are problematic for non-linear/trascende...

z3 smt z3py

回答 1 投票 0

rust z3 版本 >= v 0.10.0 ast.Bool:: 和函数

铁锈z3 当z3的版本为“v.0.4.0”时，我们可以使用Bool::and函数来表示两个bool变量AND的结果。但在版本 >=“v.0.10.0”中，它......

rust boolean z3 smt

回答 1 投票 0

自动构建析取

我必须自动构建析取/合取公式，我所知道的是我必须获取变量值的列表的长度，例如： x=Int('x') 列表= [0,1,2,3] 求解器=Sol...

z3 smt z3py

回答 1 投票 0

Z3：如何办理协会或会员资格？

我对解决 Z3 中的调度问题感兴趣，这需要以下内容：有多个类别：C1、C2、C3... 和多名学生：S1、S2、S3... 每个学生都需要恰好在一个

set z3 smt

回答 1 投票 0

使用 Z3 进行的简化并没有像预期的那样简化

在我的应用程序中，我想使用 Z3 求解器简化公式。我知道普通的简化策略不够强大，所以我使用 ctx-solver-simplify。然而，即使这样的策略也不能

z3 smt

回答 1 投票 0

如何使用 z3 库将经过优化的 SMT 模型转换为由 cvc4 等不同求解器识别的 .smt2 文件？

我想使用文件.smt2中的z3库转换用python编写的SMT模型，以获得可以从不同求解器（例如cvc4-solver）运行的文件。问题是我的模型...

optimization z3 smt cvc4 smt-lib

回答 2 投票 0

有从Python-Z3到Z3/smt2的解析器吗？

我正在使用Z3的Python API，因为方便，但有时我需要将Python结果转换为Z3/smt2的可读输入。例如，每当我执行量词消除时...

z3 smt z3py quantifiers

回答 1 投票 0

减少最大位向量大小的等价公式

是否有可能将 .smt2 公式转换为等效公式，以这样的方式重写它，即每个 (declare-const a (_ BitVec 256)) 将转换为一组 (declare-const a0 (_ BitVec .. .

z3 smt

回答 1 投票 0

Z3 Python Mod Int 问题

我想使用 Z3 打印小于 20 的素数。以下程序打印 2、3、5 和 7，但不打印 11、13、17 或 19。尽管 isPrime(11)、isPrime(13)、isPrime(17) 或 isPrime(...

python z3 smt sat

回答 1 投票 0

如果一个理论在存在片段中是可判定的，这是否意味着有一个（终止）方法来获得满意的证人？

我担心是否有算法（例如，在 SMT 求解器中实现）保证终止给出存在公式模型的任务；以同样的方式他们保证

z3 smt quantifiers first-order-logic

回答 0 投票 0

CVC5 表示“未知”给定编码为 TPTP 的归纳数据类型，尝试为构造函数找到模型

（编辑：请参阅下面的更短的失败示例！）下面的 TPTP 问题是我从精益 4 到 TPTP 的翻译产生的。归纳类型被翻译成一堆打字声明......

types smt sat

回答 0 投票 0

将 true 分配给除 one 之外的所有变量

我有一个变量列表，我想向 z3 求解器添加约束，例如所有变量都应该是 False，除了一个变量应该是 True .. a,b,c,d= Bool('a,b,c,d') s = 求解器() 所有变量=[...

z3 solver smt z3py sat

回答 1 投票 0

实数理论决策程序的实现

是否有实数一阶理论的实现？我知道柯林斯存在一种基于圆柱代数分解的技术，但我不知道任何定理证明者......

z3 smt theorem-proving cvc4

回答 1 投票 0

用z3py寻找集合中的最小元素数。

练习。找出Z的最小元素数，加起来是4285。其中Z = { w(i): w(n) - n^2 - n + 1, i = 1,2,...,30 }。我创建了一个解决方案： def f(t): return t ** 2 - t + 1 opt ...

python z3 solver smt z3py

回答 2 投票 0

Z3中浮点值的Sum()

我想写一些东西来求解一个可变数量的浮点变量给予预期的平均值。然而，当我试图运行我的代码时，我得到了这个异常。z3.z3types.Z3Exception:......。

python z3 smt

回答 1 投票 0

逐步减弱Maxsat的实力

我有一个关于MaxSat的想法，并且已经用MSU3实现了一个天真的Maxsat求解器，同时用minisat APIs实现了顺序编码，我想知道是否有办法加快这个求解器的速度。I ...

smt constraint-programming sat satisfiability sat-solvers

回答 1 投票 2

smt 相关问题

最新问题