ASKSAGE: Sage Q&A Forum - Individual question feedhttp://ask.sagemath.org/questions/Q&A Forum for SageenCopyright Sage, 2010. Some rights reserved under creative commons license.Sun, 03 Nov 2013 21:56:50 -0600SAT Solverhttp://ask.sagemath.org/question/10664/sat-solver/From the documentation of `sage.sat.boolean_polynomials.solve` ([here](http://www.sagemath.org/doc/reference/sat/sage/sat/boolean_polynomials.html)), it is not clear how to use it. Can anyone cite me any detailed example?
Say, I need to solve (in a Boolean ring)
<code> (x1 + x2 * x3 = x2)*(x2 = x3) </code>.
Can we do it?
Regards.Sun, 03 Nov 2013 15:44:00 -0600http://ask.sagemath.org/question/10664/sat-solver/Answer by tmonteil for <p>From the documentation of <code>sage.sat.boolean_polynomials.solve</code> (<a href="http://www.sagemath.org/doc/reference/sat/sage/sat/boolean_polynomials.html">here</a>), it is not clear how to use it. Can anyone cite me any detailed example?</p>
<p>Say, I need to solve (in a Boolean ring)
<code> (x1 + x2 * x3 = x2)*(x2 = x3) </code>.
Can we do it?</p>
<p>Regards.</p>
http://ask.sagemath.org/question/10664/sat-solver/?answer=15651#post-id-15651You 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.
Sun, 03 Nov 2013 21:56:50 -0600http://ask.sagemath.org/question/10664/sat-solver/?answer=15651#post-id-15651