扩展基于 LINQ 的规范模式以实现包容答案

【问题标题】：Extending LINQ-based Specification Pattern to implement subsumption扩展基于 LINQ 的规范模式以实现包容
【发布时间】：2012-12-04 23:12:24
【问题描述】：

复合规范模式有很多基于 LINQ 的实现。我还没有见过使用 Subsumption 的。

是否有任何此类示例已被记录（博客等）或作为开源发布？我有一个想法和概念证明，通过让 ExpressionVisitor 将每个规范转换为规范逻辑形式 (CNF/DNF) 来实现这一点，但我担心这过于复杂。有没有更好的办法？

【问题讨论】：

你的意思是 Linq 中的条件 where 子句吗？

标签： linq boolean-logic boolean-expression linq-expressions specification-pattern

【解决方案1】：

我担心这过于复杂。有没有更好的办法？

简短的回答是“不，没有”¹

长答案：“过于复杂”抓住了问题的本质：它是 NP 难的。这是一个简短的非正式证明，它依赖于 satisfiability problem is NP-complete:

假设您有两个布尔公式，A 和 B
对于A 和B 所依赖的所有变量赋值，您需要测试A 是否隐含B，或等价于¬A | B。换句话说，您需要证明F = ¬A | B 是一个重言式。
假设重言式测试可以在多项式时间内执行
考虑¬F，F 的倒数。 F 是可满足的当且仅当¬F 不是一个重言式
使用假设多项式算法测试 ¬F 是否是重言式
“是 F 可满足”的答案与“是 ¬F 重言式”的答案相反
因此，多项式重言式检查器的存在意味着可满足性问题存在于P 和P=NP。

当然，问题是 NP-hard 的事实并不意味着对于实际情况没有解决方案：事实上，您转换为规范形式的方法可能会在许多实际情况下产生良好的结果。然而，缺乏已知的“好”算法通常会阻碍实际解决方案的积极开发²。

¹ 带有强制性的“除非P=NP”免责声明。

² 除非有一个“相当好的”解决方案，如果你允许“假阴性”，那么你的问题很可能就是这种情况。

【讨论】：

+1，问题：您是在形式逻辑意义上使用重言式，还是在 CS 中有类似但不同的限定定义？我的理解是，一个命题是重言式的，如果它可以从空的 SC 句子集中推导出来。这不能充分描述我要证明的内容，因为我也有一个广泛的知识库/数据库可以从中派生。另一方面，这个问题很困难，但之前已经有效地解决了。现在，我正在研究 Prolog、Euler 和 Microsoft Solver Foundation。
@smartcaveman 我在形式逻辑意义上使用重言式：为了证明表达式A 包含B，您需要证明A => B 始终为真，即可以是源自空的前提集。我提到它的唯一原因是解决可满足性问题，众所周知，它是 NP 完全的。注意只有A => B必须是重言式；单独的表达式A 和B 可以，并且在所有非平凡的情况下，将基于非空的前提集。该集合越大，越难证明B 被A 包含。
所以我对如何更实际地解决这个问题有了另一个想法——仍在解决这个问题。我可以为每个谓词创建一个对立平方模型，并要求我的所有谓词都采用三段论形式，而不是纯粹的重写。这似乎可以减轻复杂性，b/c 内容将被规范化而不是正式的表示 - 因为我的域是一个业务应用程序，我认为它可能足够有表现力。有什么想法吗？
@smartcaveman 更改表示不会改变问题的基本难度。即使您将所有内容归一化为 3-CNF，您仍然处于 NP 空间中。本质上，您正在构建一阶定理证明器 - 这并不容易，除非您显着限制您的谓词。如果您的应用程序可以容忍，在少数极端情况下允许误报可能是另一种权衡。
您能否详细说明您的想法：允许极端情况出现误报，或者将我链接到讨论这种变化的地方？