布尔公式的简化，没有否定，只是和/或

Question

我想预处理布尔公式，以便 a 和（a 或 b）和 c

变得只是 a 和 c

从来没有任何否定，所以这应该是一个简单的问题，但没有什么真正明显的想法出现在脑海中（除了折叠“与”、“或”、重复、排序）。我是否遗漏了一些完全明显的东西？

Answer 1

我在 CSTheory.stackexchange 上有一个相关问题，这里给出了否定的答案。

您所描述的问题是 coNP-hard 的。因此，除非 P=NP，否则您将找不到有效的算法来做到这一点。

转换为CNF或DNF会导致某些公式呈指数级膨胀。

Answer 2

从你的例子来看，一般来说你不太清楚你想要什么。

看来你想用吸收定律来尽可能简化公式：

A ∨ (A ∧ B) = A 

A ∧ (A ∨ B) = A 

在您的示例中，您只需应用第二吸收定律一次。

Answer 3

A(A+B)C

AAC+ABC

交流+ABC

A1C + ABC

A(1+B)C

A(1)C

交流

这就是您要找的吗？

Answer 4

使用K-map。

基本上，您将创建一个公式可能结果的内存图表。 解析它，并以这样的方式存储它：给所有变量提供任意输入，您可以获得结果。 然后创建一个 N 维数组（其中 N 是变量的数量）并尝试每种组合，并将结果存储在数组中。

完成此操作后，请按照上述文章中的步骤提出简化的表达式。

请注意，这适用于包含所有类型布尔运算符的表达式，包括 not。

Answer 5

考虑转换为CNF或DNF。

简化“底层”很容易——只需删除重复项即可。 简化下一个级别几乎同样容易——删除子集或超集。

Answer 6

这是我在开发 SymPy 时从 Oscar Benjamin 那里学到的一个小例程，它将参数列表从 cnf 转换为 dnf，反之亦然。

def cnfdnf(eqs):
    """Change cnf args set to dnf (or vice versa). For And(x, Or(x,z)) pass
    [{x}, {x,z}]
    """
    if not eqs:
        return [set()]
    elif len(eqs) == 1:
        return [{f} for f in eqs[0]]
    else:
        assert all(type(i) is set for i in eqs)
        f = list(eqs[0])[0]
        eqs_f_zero = [_ for _ in eqs if f not in _]
        dnf_f = cnfdnf(eqs_f_zero)
        if {f} in eqs:
            dnf = [s | {f} for s in dnf_f]
        else:
            f_free_eqs = [_ - {f} for _ in eqs]
            eqs_f_nonzero = list(filter(None, f_free_eqs))
            dnf_no_f = cnfdnf(eqs_f_nonzero)
            dnf = dnf_no_f + [s | {f} for s in dnf_f if s not in dnf_no_f]
        return dnf

如果存在完全独立于其他集合的集合，则可以通过将每个笛卡尔积添加到每个从属参数中来单独处理它们，例如'a'、'ab'、'bc' 彼此依赖，而 'de' 和 'f' 则不然。因此，3 个依赖项的每个结果将变成另外两个包含“df”或“ef”的结果。但如果你想保持相同的形式，你可以再次运行

cnfdnf

，这只会将独立参数返回到开始时的状态。但正如 @wnoise 指出的那样，这样做相当于删除超集。因此，我不会提供一个例程，而是展示如何在 cnf 和 dnf 之间快速切换，同时注意独立参数。

def cnf_dnf(eqs):
    """simplify a cnf or dnf form"""
    from itertools import product as cartes
    eqs = [set(i) for i in eqs]
    indep = []
    for i in range(len(eqs)):
        for j in range(len(eqs)):
            if i != j and any(x in eqs[i] for x in eqs[j]):
                # it is dependent
                break
        else:
            indep.append(i)
    if indep:
        new = cnfdnf([eqs[i] for i in range(len(eqs)) if i not in indep])
        rv = []
        for i in cartes(*[eqs[i] for i in indep]):
            rv.extend( [n|set(i) for n in new] )
        return rv
    else:
        return reform(eqs)

>>> [''.join(i) for i in cnf_dnf(['a','ab','bf','c','de'])]
['cabd', 'cadf', 'cabe', 'cafe']
>>> cnf_dnf(_)  # back to simplified original form
[{'d', 'e'}, {'b', 'f'}, {'a'}, {'c'}]

注意我们所做的就是删除超集“ab”。因此，如果这就是我们想要做的全部（并且不想从一种形式更改为另一种形式），那么有一个很好的例程可以做到这一点here。