通常如何组合和优化谓词？答案

【问题标题】：How to combine and optimize a predicate, generally?通常如何组合和优化谓词？
【发布时间】：2009-09-21 15:36:14
【问题描述】：

我正在做一些复杂事件处理系统的工作。它支持使用查询语言根据这些记录的成员过滤记录集。该语言支持任意成员的逻辑、算术和用户定义运算符。

以下是支持的查询示例：

( MemberA > MemberB ) && 
( @in MemberC { "str1", "str2" } ) &&
( com.foo.Bar.myPred( MemberD, MemberE ) )

我的问题是我想将查询组合成一个超级查询，然后我想优化该超级查询以消除冗余、重言式和矛盾。例如我要拍

A > 0

并结合

A > 1

这很简单：

A > 0 || A > 1

但后来我想优化它，使其减少到

A > 0

如果有任何 URL 或书籍讨论这个一般性主题，我将不胜感激。

【问题讨论】：

【解决方案1】：

书籍？我认为有几个；并且很可能您应该查找该领域的文章。

您可能会看到SMT solvers，它可以与您的查询域一起使用。你用你的表达语言的数学化定义，你支持的关系的状态公理来喂他们。然后，例如，他们可以推理（是的，两个相等的连词）一个谓词是否暗示另一个谓词是重言式。

请注意，此任务的自动化解决方案含糊不清，有时超出了图灵机（即计算机）的理论能力。您的问题不会有唯一且正确的解决方案。

【讨论】：

谢谢帕维尔。我的感觉是，完全最优的解决方案将是棘手的，但应该可以在有限的时间段内进行一些合理的优化。 SMT 看起来很有趣，感谢您指出，但我无法从您的回答中理解这句话：“然后，他们可以，例如，推理（是的，两个相等的连词）一个谓词是否暗示另一个是重言式”，你能澄清一下吗？
@Bill：澄清。在您的示例中，您要丢弃谓词A > 1，因为它是由A > 0 暗示的。 IE。在A>1 为真的所有情况下，A>0 也为真（这称为“暗示”）。鉴于您的 SMT 求解器已上传正式的算术公理，因此可以推断公式 ( A > 0 ) implies ( A > 1) 是重言式。在这个推理之后，你可以从你的表达中撤回A>0。但这只是 SMT 求解器的众多应用之一，我只是因为您在问题中使用了它而对其进行了概述。