减少布尔表达式答案

【问题标题】：Reducing a boolean expression减少布尔表达式
【发布时间】：2012-03-17 16:22:36
【问题描述】：

我有一个表情，假设，

a = 1 && (b = 1 || b != 0 ) && (c >= 35 || d != 5) && (c >= 38 || d = 6)

我希望它减少到，

a = 1 && b != 0 && (c >= 38 || d = 6)

有人有什么建议吗？指向任何算法的指针？

Nota Bene： 我相信卡诺图或 Quine-McCluskey 不是这里的选择。因为这些方法不处理灰色情况。我的意思是，表达只能减少到像 A 或 A' 或什么都没有，或者说是黑色或白色或无色的情况。但是这里我有灰色阴影，你们可以看到。

解决方案：我已经在 Clojure 中为此编写了程序。我使用包含函数作为值的地图的地图。这很方便，只需几个组合的一些规则，你就很好。感谢您提供有用的答案。

【问题讨论】：

多项式时间内可以减少多少是有限制的。例如，如果您始终可以将任何合取范式表达式简化为最简单的形式，那么您将解决开放 3SAT 问题。
@mbeckish：这对我来说听起来很可怕。实际上，直到你们把我引向正确的方向，我才知道这些事情。我想到的不仅仅是 3SAT，还有 nSAT 问题。现在，这一切听起来都是不可能的。
不要害怕解决 NP 难题。对于他们中的大多数人来说，困难的部分将在问题空间的一个相对较小的区域内，处于不可行问题和简单问题之间的相变中。如果解决 NP 难题总是不可能的，我就会失业。这在很大程度上取决于您希望算法扩展多远。

标签： language-agnostic boolean-expression reduction boolean-operations constraint-programming

【解决方案1】：

我认为你应该能够通过使用Constraint Handling Rules 来实现你想要的。您需要编写简化 OR 和 AND 表达式的规则。

主要的困难是约束蕴涵检查，它告诉您可以丢弃哪些部分。例如， (c >= 35 || d != 5) && (c >= 38 || d = 6) 简化为 (c >= 38 || d = 6) 因为前者由后者蕴涵，即后者更具体。不过，对于 OR 表达式，您需要选择更通用的部分。

Google 找到了paper on an extension of CHR with entailment check for user-defined constraints。我对 CHR 了解的不够多，无法告诉您是否需要这样的扩展。

【讨论】：

在简要阅读了约束编程，然后是约束逻辑编程（mgibsonbr 在另一篇文章中指出），然后是约束满足问题，然后是约束处理规则，然后是约束优化，我相信我的问题在于约束优化，我也相信任何回溯算法都会有用。我特别关注 B&B 和 Bucket Elimination，后者不是回溯算法。我的方向正确吗？
@AdeelAnsari：是的，你可以把它看作是一种优化问题，如果你以子句的数量作为衡量标准，你想找到最短的表示。通常，在解决 COP 问题时，B&B 是一个不错的选择，但只有在您可以计算出最终结果中子句数量的一些下限时才会有所帮助，否则它就是完整的搜索。使用 CLP 时将包括回溯。 CHR 旨在成为“承诺选择”，即没有回溯，但 CLP 之上的 CHR 实现实际上确实有回溯（例如在 ECLiPSe 中）。消除桶是否有帮助，我不知道。
@AdeelAnsari：顺便说一句，您是在寻找一个完全通用的解决方案，还是在为特定用例开发解决方案？如果是后者，您需要处理多少个变量和多大的域？
在程序函数中将其作为if-clause，或在sql-select 语句中作为where-clause。在这种情况下，我正试图减少约束，如果有些约束需要其他约束的话。我不认为，我可以修复变量的大小。

【解决方案2】：

我相信这些事情在constraint logic programming 中经常发生。不幸的是，我没有足够的经验来提供更准确的细节，但这应该是一个很好的起点。

一般原则很简单：未绑定的变量可以有任何值；当您针对不等式对其进行测试时，它的一组可能值受到一个或多个间隔的限制。当/如果这些间隔收敛到一个点时，该变量将绑定到该值。如果，OTOH，对于间隔中的每个值，这些不等式中的任何一个都被认为是无法解决的，那么就会发生[编程]逻辑故障。

另请参阅this，了解如何在实践中使用 swi-prolog 完成此操作的示例。希望您能找到底层算法的链接或参考，这样您就可以在您选择的平台上重现它们（甚至可以找到现成的库）。

更新：我尝试使用 swi-prolog 和 clpfd 重现您的示例，但没有得到我预期的结果，只有接近的结果。这是我的代码：

?- [library(clpfd)].
simplify(A,B,C,D) :-
    A #= 1 ,
    (B #= 1 ; B #\= 0 ) ,
    (C #>= 35 ; D #\= 5) ,
    (C #>= 38 ; D #= 6).

我的结果，关于回溯（为了便于阅读而插入换行符）：

10 ?- simplify(A,B,C,D).

A = 1,
B = 1,
C in 38..sup ;

A = 1,
B = 1,
D = 6,
C in 35..sup ;

A = 1,
B = 1,
C in 38..sup,
D in inf..4\/6..sup ;

A = 1,
B = 1,
D = 6 ;

A = 1,
B in inf.. -1\/1..sup,
C in 38..sup ;

A = 1,
D = 6,
B in inf.. -1\/1..sup,
C in 35..sup ;

A = 1,
B in inf.. -1\/1..sup,
C in 38..sup,
D in inf..4\/6..sup ;

A = 1,
D = 6,
B in inf.. -1\/1..sup.

11 ?-

因此，该程序产生了 8 个结果，其中您感兴趣的 2 个结果（第 5 个和第 8 个）：

A = 1,
B in inf.. -1\/1..sup,
C in 38..sup ;

A = 1,
D = 6,
B in inf.. -1\/1..sup.

另一个是多余的，也许可以使用简单、可自动化的逻辑规则来消除：

1st or 5th ==> 5th          [B == 1  or B != 0 --> B != 0]
2nd or 4th ==> 4th          [C >= 35 or True   --> True  ]
3rd or 1st ==> 1st ==> 5th  [D != 5  or True   --> True  ]
4th or 8th ==> 8th          [B == 1  or B != 0 --> B != 0]
6th or 8th ==> 8th          [C >= 35 or True   --> True  ]
7th or 3rd ==> 3rd ==> 5th  [B == 1  or B != 0 --> B != 0]

我知道要成为通用解决方案还有很长的路要走，但正如我所说，希望这是一个开始......

附：我使用“常规” AND 和 OR（, 和 ;），因为 clpfd 的（#/\ 和 #\/）给出了一个非常奇怪的结果，我无法理解自己......也许更有经验的人可以投点灯吧……

【讨论】：

谢谢，朋友。你真好。我正在研究它，并试图消化。