SAT solver SAGE

Question

I'm trying to understand why the solver not found solution in this code

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

For me the solution is x=1;y=1 and z=1, or I'm wrong?

Answer 1

The explanation for this return value (and how to get a more satisfying one) can be found by carefully reading the documentation for the solve method we are using, but I agree with you that this return value is puzzling.

To access the documentation for the method, type S.solve?, and to access the source code, type S.solve??. This will also reveal the file where this method is defined, and you can then read this file on your system or online on the Sage source code at GitHub.

For reference, I work with Sage 6.3. Removing w which played no role, and slightly simplifying by writing Sequence and not giving the solution a name, your example becomes:

sage: R.<x,y,z> = BooleanPolynomialRing()
sage: S = Sequence([x * y + z, x + y])
sage: S.solve()
[]

We are indeed surprised, since (0,0,0) and (1,1,1) are two obvious solutions.

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]

This is because this solve method has an optional parameter eliminate_linear_variables, set to True by default, which removes all linear occurrences of the variables into the equations. In our example, this just removes all the equations.

And another maybe surprising feature of this solve method is that if the polynomial sequence is empty, it returns an empty list:

sage: S = S[0:]
sage: S.solve()

(whereas one might argue that anything is a solution for an empty list of equations).

To get a solution for the polynomial sequence:

sage: S.solve(eliminate_linear_variables=False)
[{z: 0, y: 0, x: 0}]

Here we get only one solution. This is because another optional parameter of the solve method, n, indicates to return at most n solutions, with a default set to one. Set it to Infinity to get all solutions.

sage: S.solve(n=Infinity,eliminate_linear_variables=False)
[{z: 0, y: 0, x: 0}, {z: 1, y: 1, x: 1}]