python - SAT 求解器 SAGE

Question

我试图理解为什么求解器在此代码中找不到解决方案

R.<x,y,z,w> = BooleanPolynomialRing()
S = PolynomialSequence([x*y+z,x+y])
sol = S.solve(); sol
[]

对我来说，解决方案是 x=1;y=1 和 z=1，还是我错了？

Answer 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}]