Revision history [back]
 | 1 | initial version |
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}]
| | 2 | No.2 Revision |
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.
