我有嵌套的真值列表,代表着像这样的SAT公式:
[[[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]]]
代表
([x0=0] + [x0=0] + [x0=1]) * ([x0=1] + [x1=1] + [-x2=1]) * ([-x3=0] + [-x3=0] + [-x2=1])
我希望能够计算整个公式的真值。第一步是将每个子句中文字的真值相加。
例如:
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]
如果在总和之后
clause_truth_value
为True
,则整个子句为真。
但我没有得到我期望的结果:
True + True = 2
,这不是我期望的结果
True * True = 1
,这是我期望的结果
False + False = 0
,这是我期望的结果
False * False = 0
,这是我期望的结果
所以... True只是1,而False是0... 这很糟糕,我希望布尔代数可以重载算术运算符。是否有一种优雅的方式使用布尔变量进行布尔算术?
|
和&
,而不是+
和*
。 - lejlotand=
那样的+=
。所以... - lo tolmencrex = x or y
代替x += y
。 - recursivex &= y
和x |= y
。但它们不是懒惰的。 - Veedrac