ASKSAGE: Sage Q&A Forum - RSS feedhttps://ask.sagemath.org/questions/Q&A Forum for SageenCopyright Sage, 2010. Some rights reserved under creative commons license.Mon, 04 Nov 2013 04:56:50 +0100SAT Solverhttps://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 22:44:00 +0100https://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>
https://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.
Mon, 04 Nov 2013 04:56:50 +0100https://ask.sagemath.org/question/10664/sat-solver/?answer=15651#post-id-15651