SAT Solver output

SAT Solver output

asked 2013-11-01 02:21:06 +0100

pp
49 ●1 ●1 ●10

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?

answered 2013-11-01 05:52:47 +0100

tmonteil
27413 ●31 ●204 ●517 http://wiki.sagemath.o...

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?

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:

edit flag offensive delete link

Comments

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

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

add a comment

Your Answer

Please start posting anonymously - your entry will be published after you log in or create a new account.

1 Answer

Comments

Your Answer

Question Tools

Stats

Related questions

SAT Solver output edit

1 Answer

Comments