# SAT Solver output

I need to solve a SAT problem. I searched and found the manual here, 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?

edit retag close merge delete

Sort by ยป oldest newest most voted

There 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?


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:

more

Then why not use cms()[1:]? That will simplify the situation.

( 2013-11-03 23:21:52 +0100 )edit