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.

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.