Re: [sage-support] Question about SAT solver

2014-08-13 Thread Juan Grados
Understand thanks, 2014-08-12 11:20 GMT-03:00 Martin Albrecht : > This is a bug. In particular: > > sage: S.solve(eliminate_linear_variables=False) > [{w: 0, z: 0, y: 0, x: 0}] > > Does the trick. The bug is that eliminating linear variables already solves > the problem and the logic in solve()

Re: [sage-support] Question about SAT solver

2014-08-12 Thread Martin Albrecht
This is a bug. In particular: sage: S.solve(eliminate_linear_variables=False) [{w: 0, z: 0, y: 0, x: 0}] Does the trick. The bug is that eliminating linear variables already solves the problem and the logic in solve() doesn't handle this case. Please open a ticket and CC me. On Tuesday 12 Aug

[sage-support] Question about SAT solver

2014-08-12 Thread Juan Grados
Dears members, I'm trying to understand why the solver not found solution in this code R. = 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? thanks -- -