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 16:21:52 -0600SAT Solver outputhttp://ask.sagemath.org/question/10680/sat-solver-output/I need to solve a SAT problem. I searched and found the manual [here](http://www.sagemath.org/doc/reference/sat/), but can not figure out the output obtained:
sage: from sage.sat.solvers import CryptoMiniSat # optional - cryptominisat
sage: cms = CryptoMiniSat() # optional - cryptominisat
sage: cms.add_clause((1,2,-3)) # optional - cryptominisat
sage: cms() # optional - cryptominisat
(None, True, True, False)
There are 3 variables, then what does that `None` mean?Thu, 31 Oct 2013 20:21:06 -0500http://ask.sagemath.org/question/10680/sat-solver-output/Answer by tmonteil for <p>I need to solve a SAT problem. I searched and found the manual <a href="http://www.sagemath.org/doc/reference/sat/">here</a>, but can not figure out the output obtained:</p>
<pre><code>sage: from sage.sat.solvers import CryptoMiniSat # optional - cryptominisat
sage: cms = CryptoMiniSat() # optional - cryptominisat
sage: cms.add_clause((1,2,-3)) # optional - cryptominisat
sage: cms() # optional - cryptominisat
(None, True, True, False)
</code></pre>
<p>There are 3 variables, then what does that <code>None</code> mean?</p>
http://ask.sagemath.org/question/10680/sat-solver-output/?answer=15635#post-id-15635There is no `0` variable because there is no difference between `0` and `-0`. But python lists start with index `0`. If you want the value of the variable `2`, you will type:
sage: cms()[2]
True
Without the `None` at the beginning (standing for the value of the `0` variable that does not exist), you will get `False` (the value of the variable `3`).
There seems not be any on-line documentation, but you can actually read it from the sage command line, if you type:
sage: cms?
You will read
OUTPUT:
* If this instance is SAT: A tuple of length "nvars()+1" where the
"i"-th entry holds an assignment for the "i"-th variables (the
"0"-th entry is always "None").
and
First, we do not assume anything, note that the first entry is
"None" because there is not "0"-th variable:
Thu, 31 Oct 2013 23:52:47 -0500http://ask.sagemath.org/question/10680/sat-solver-output/?answer=15635#post-id-15635Comment by pp for <p>There is no <code>0</code> variable because there is no difference between <code>0</code> and <code>-0</code>. But python lists start with index <code>0</code>. If you want the value of the variable <code>2</code>, you will type:</p>
<pre><code>sage: cms()[2]
True
</code></pre>
<p>Without the <code>None</code> at the beginning (standing for the value of the <code>0</code> variable that does not exist), you will get <code>False</code> (the value of the variable <code>3</code>).</p>
<p>There seems not be any on-line documentation, but you can actually read it from the sage command line, if you type:</p>
<pre><code>sage: cms?
</code></pre>
<p>You will read</p>
<pre><code>OUTPUT:
* If this instance is SAT: A tuple of length "nvars()+1" where the
"i"-th entry holds an assignment for the "i"-th variables (the
"0"-th entry is always "None").
</code></pre>
<p>and</p>
<pre><code>First, we do not assume anything, note that the first entry is
"None" because there is not "0"-th variable:
</code></pre>
http://ask.sagemath.org/question/10680/sat-solver-output/?comment=16806#post-id-16806Then why not use `cms()[1:]`? That will simplify the situation.Sun, 03 Nov 2013 16:21:52 -0600http://ask.sagemath.org/question/10680/sat-solver-output/?comment=16806#post-id-16806