Ask Your Question

SAT Solver output

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

pp gravatar image

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 flag offensive close merge delete

1 Answer

Sort by ยป oldest newest most voted

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

tmonteil gravatar image

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]

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

* 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").


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 more


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

pp gravatar imagepp ( 2013-11-03 23:21:52 +0200 )edit

Your Answer

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

Add Answer

Question Tools


Asked: 2013-11-01 02:21:06 +0200

Seen: 364 times

Last updated: Nov 01 '13