I have nested lists of truth values representing SAT forumlas, like this:
[[[0, True, False], [0, True, False], [0, True, 1]], [[0, True, True], [2, True, True], [3, False, True]], [[1, False, False], [1, False, False], [3, False, True]]]
representing
([x0=0] + [x0=0] + [x0=1]) * ([x0=1] + [x1=1] + [-x2=1]) * ([-x3=0] + [-x3=0] + [-x2=1])
I would like to calculate the truth value of the whole formula. First step would be adding up the truth values of the literals in each clause.
like this:
clause_truth_value = None
for literal in clause:
# multiply polarity of literal with its value
# sum over all literals
clause_truth_value += literal[1]*literal[2]
if clause_truth_value
is True
after the summation, the clause is true as a whole.
But I am not getting what I expected:
True + True = 2
that's not as expected
True * True = 1
that's as expected
False + False = 0
that's as expected
False * False = 0
that's as expected
so... True is simply 1 and False is 0... that sucks, I expected the arithmetic operators to be overloaded for the boolean algebra. Is there an elegant way to do do boolean arithmetic with boolean variables?
See Question&Answers more detail:
os