Satispy can use constans

[crptcusco]

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]

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

[crptcusco]

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.