search

netom / satispy

An interface to SAT solver tools (like minisat)
Other
58 stars 17 forks source link

Satispy can use constans #15

Open crptcusco opened 5 years ago

crptcusco commented 5 years ago

I use satispy to solve boolean functions, but I need some variables to have constant values 0 or 1, True or False. Can the library do that?

Arvind-777 commented 1 year ago

@crptcusco Hey did you find out anything about this? Would be grateful if you can share.

crptcusco commented 1 year ago

Yes, use a boolean property that can be used to set values. It is about placing the formula in CNF and we put the variable that we want to set by adding the variable to the formula with AND.

For example, to set the variable x5 , in the function

(x1 OR x5 OR -x2) AND (-x3 OR x4 OR x1)

If we want to set it positive, we can formulate it in CNF

(x1 OR x5 OR -x2) AND (-x3 OR x4 OR x1) AND x5

If we want the value in negative we put like this

(x1 OR x5 OR -x2) AND (-x3 OR x4 OR x1) AND -x5

So the SAT-Solver the only way to give a true answer is through the fixed value. This property works with Satispy.