Ask Your Question
0

SAT Solver output

asked 2013-10-31 20:21:06 -0500

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
1

answered 2013-10-31 23:52:47 -0500

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]
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 more

Comments

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

pp gravatar imagepp ( 2013-11-03 16:21:52 -0500 )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

Stats

Asked: 2013-10-31 20:21:06 -0500

Seen: 145 times

Last updated: Oct 31 '13