- android - 多次调用 OnPrimaryClipChangedListener
- android - 无法更新 RecyclerView 中的 TextView 字段
- android.database.CursorIndexOutOfBoundsException : Index 0 requested, 光标大小为 0
- android - 使用 AppCompat 时,我们是否需要明确指定其 UI 组件(Spinner、EditText)颜色
我试图理解为什么求解器在此代码中找不到解决方案
R.<x,y,z,w> = BooleanPolynomialRing()
S = PolynomialSequence([x*y+z,x+y])
sol = S.solve(); sol
[]
对我来说,解决方案是 x=1;y=1 和 z=1,还是我错了?
最佳答案
这个返回值的解释(以及如何得到一个更令人满意的返回值)可以通过仔细阅读我们正在使用的 solve
方法的文档找到,但我同意你的观点,这个返回值值(value)令人费解。
要访问该方法的文档,请输入 S.solve?
,要访问源代码,请输入 S.solve??
。这还将显示定义此方法的文件,然后您可以在您的系统上或在 Sage source code at GitHub 上在线阅读此文件。 .
作为引用,我使用的是 Sage 6.3。删除没有发挥作用的 w
,并通过编写 Sequence
而不给解决方案命名来稍微简化,您的示例将变为:
sage: R.<x,y,z> = BooleanPolynomialRing()
sage: S = Sequence([x * y + z, x + y])
sage: S.solve()
[]
我们确实感到惊讶,因为 (0,0,0) 和 (1,1,1) 是两个明显的解。
sage: obvious_0 = {x: 0, y: 0, z: 0}
sage: obvious_1 = {x: 1, y: 1, z: 1}
sage: S.subs(obvious_0)
[0, 0]
sage: S.subs(obvious_1)
[0, 0]
这是因为此solve
方法有一个可选参数eliminate_linear_variables
,默认设置为True
,这会删除变量的所有线性出现代入方程。在我们的示例中,这只是删除了所有方程。
此 solve
方法的另一个可能令人惊讶的功能是,如果多项式序列为空,则它返回一个空列表:
sage: S = S[0:]
sage: S.solve()
(然而人们可能会认为任何东西都是空方程列表的解)。
要获得多项式序列的解:
sage: S.solve(eliminate_linear_variables=False)
[{z: 0, y: 0, x: 0}]
这里我们只有一个解决方案。这是因为 solve
方法的另一个可选参数 n
表示最多返回 n
个解决方案,默认设置为 1。将其设置为Infinity
以获得所有解决方案。
sage: S.solve(n=Infinity,eliminate_linear_variables=False)
[{z: 0, y: 0, x: 0}, {z: 1, y: 1, x: 1}]
关于python - SAT 求解器 SAGE,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/25264382/
这两个 NP 完全问题之间到底有什么区别?在我看来,他们都在询问是否可以满足 bool 公式(即输出 1),但一个是在电路的上下文中,另一个只是一个公式。但是,不能从 bool 电路中写出 bool
有谁知道一个好的程序可以将每个子句具有任意数量变量的 CNF 文件转换为每个子句恰好有 3 个变量的 CNF 文件 (3-CNF)?我在计算机科学书籍中看到过这种算法,但无法在任何地方找到实现,如果其
我一直在阅读 this文章尝试并解释了 max 2 sat 问题本质上是一个 3-sat 问题并且是 NP-hard。 然而,如果你看到这篇文章,我无法理解为什么,满足ci后,10个子句中有7个是满意
看完strategies guide Z3 和 this answer利奥,我预计(check-sat)和 (check-sat-using smt)是等价的。然而,当针对我们的测试套件(230 个
我有兴趣了解已知为多项式(或更现实地说,O(N^2))的 bool 可满足性问题的特殊情况。这些案例还应该有有效的算法来实际生成所有令人满意的实例,其中高效我的意思是需要 O(N #SAT) 来生成所
SMT2 标准规定,调用 get-value 仅在调用 check-sat 之后才合法,并且仅当 check-sat 返回“sat”或“unknown”时才合法。 下面是一个 unsat 问题的简单示
我正在翻阅以前的试卷,并且遇到了这个让我感到困惑的问题。 问题: Convert the Not-All-Equal 2-SAT problem given by the clauses {x1, x
在 go 语言中 spec他们在其中一个示例中使用了三个点: days := [...]string{"Sat", "Sun"} // len(days) == 2 如果省略这三个点有什么不同吗?
我真的很困惑为什么2-CNF SAT在P,而3-CNF SAT在NPC。我读过 CLRS,我了解他们如何证明 3-CNF SAT 在 NPC 中。我不能使用从 SAT 到 2-CNF-SAT 的相同还
当使用 MiniSat 作为 C++ 库时,每个新变量都可以创建为决策变量或非决策变量。 我对此的粗略理解是,当求解器在分支期间决定接下来使用哪个变量时,不考虑非决策变量。然而,在我的项目中,当非决策
我从模板生成问题,由于问题的性质,我不得不依赖量词。现在,求解器只能找到非常简单(可满足)问题的实例。在许多情况下,寻找“unsat”是可行的。查找“sat”很少奏效。 问题在于,即使是像定义两个不相
我正在尝试构建一个简单的 Prolog SAT 求解器。我的想法是用户应该使用 Prolog 列表输入要在 CNF(联合范式)中求解的 bool 公式,例如(A 或 B)和(B 或 C)应显示为 sa
SAT 的最小翻译向量是否在所有情况下都始终正确和精确?我通过迭代所有可能的轴并检查每个轴上的重叠来计算它,然后继续跟踪哪个轴具有最短的重叠并将其用作穿透向量。 如您所见,最小平移向量的某些计算并不总
Boolean Satisfiabiity problem是检查 bool 表达式的可满足性的概括。现在 bool 表达式是由多项式的非负性算法生成的。例如,多项式可以是 和 有一些间隔,例如 其中
问题 我正在研究 SAT 优化问题的一个特殊子集。对于那些不熟悉 SAT 和相关主题的人,这里是 related Wikipedia article . TRUE=(a OR b OR c OR d)
我正在试验 F#,并希望在我使用 Or-Tools 的地方进行一些约束编程。我以前将该包与 Python 一起使用,但我无法让它与 F# 一起使用。 我遵循 C# 示例:https://develop
在调度问题中。我想按工作天数分配假期。现在我有一个使用多个 bool 标志的有效解决方案,但它的扩展性不是很好。 from ortools.sat.python import cp_model fro
我写了一个我认为是 quite interesting question 的答案,但不幸的是,在我发布之前,该问题已被作者删除。我在这里重新发布问题的摘要和我的答案,以防其他人有用。 假设我有一个 S
在汽车行业,当您购买汽车时,您有数千种不同的组件可供选择。并非每个组件都是可组合的,因此对于每辆汽车,都存在许多用命题逻辑表达的规则。就我而言,每辆车都有 2000 到 4000 条规则。 它们看起来
我在大学系使用一台 Cent0S 机器。请注意,我没有权限使用我作为 root 使用的系统。我下载了 minisat+zip file 我解压了zip。根据我运行的安装文件 make rx 但我有以下
我是一名优秀的程序员,十分优秀!