From the documentation of sage.sat.boolean_polynomials.solve (here), it is not clear how to use it. Can anyone cite me any detailed example?
Say, I need to solve (in a Boolean ring)
(x1 + x2 * x3 = x2)*(x2 = x3) .
Can we do it?
Regards.
You can do:
sage: from sage.sat.boolean_polynomials import solve as solve_sat
sage: B.<x1,x2,x3> = BooleanPolynomialRing() ; B
Boolean PolynomialRing in x1, x2, x3
sage: f = (x1 + x2 * x3 - x2)*(x2 - x3) ; f
x1*x2 + x1*x3 + x2*x3 + x2
l = solve_sat([f], n=infinity) ; l
[{x3: 0, x2: 0, x1: 0},
{x3: 1, x2: 1, x1: 1},
{x3: 0, x2: 0, x1: 1},
{x3: 1, x2: 1, x1: 0},
{x3: 1, x2: 0, x1: 0},
{x3: 0, x2: 1, x1: 1}]
It is possible that you will have to install the cryptominisat package first.
Asked: 2013-11-03 22:44:00 +0100
Seen: 373 times
Last updated: Nov 04 '13
Copyright Sage, 2010. Some rights reserved under creative commons license. Content on this site is licensed under a Creative Commons Attribution Share Alike 3.0 license.