在哪里可以找到将任意布尔表达式转换为合取或析取范式的方法？ [英] Where might I find a method to convert an arbitrary boolean expression into conjunctive or disjunctive normal form?

问题描述

我编写了一个小应用，该应用将表达式解析为抽象语法树。现在，我对表达式使用了一系列启发式方法，以确定如何最好地评估查询。不幸的是，有一些示例使查询计划变得非常糟糕。

I've written a little app that parses expressions into abstract syntax trees. Right now, I use a bunch of heuristics against the expression in order to decide how to best evaluate the query. Unfortunately, there are examples which make the query plan extremely bad.

我找到了一种方法，可证明地更好地猜测应该如何评估查询，但是我需要首先将我的表情放入CNF或DNF中，以便获得可证明的正确答案。我知道这可能会导致潜在的指数时间和空间，但是对于我的用户运行的典型查询来说，这不是问题。

I've found a way to provably make better guesses as to how queries should be evaluated, but I need to put my expression into CNF or DNF first in order to get provably correct answers. I know this could result in potentially exponential time and space, but for typical queries my users run this is not a problem.

现在，我转换为CNF或DNF为了简化复杂的表达方式，始终需要手动处理。 （嗯，也许不是一直都是，但是我确实知道如何使用例如德摩根定律，分配定律等。）但是，我不确定如何开始将其转换为可作为算法实现。我看过有关查询优化的论文，其中有几篇以首先把东西放到CNF中或首先把东西放到DNF中开头，他们似乎从不解释实现这一点的方法。

Now, converting to CNF or DNF is something I do by hand all the time in order to simplify complicated expressions. (Well, maybe not all the time, but I do know how that's done using e.g. demorgan's laws, distributive laws, etc.) However, I'm not sure how to begin translating that into a method that is implementable as an algorithm. I've looked at papers on query optimization, and several start with "well first we put things into CNF" or "first we put things into DNF", and they never seem to explain their method for accomplishing that.

我应该从哪里开始？

推荐答案

朴素的原始算法，用于无量词公式，是：

The naive vanilla algorithm, for quantifier-free formulae, is :

• 对于CNF，转换为否定范式，然后将AND分配到AND


• 用于DNF，转换为否定范式与De Morgan法则并在OR上进行AND分配

• for CNF, convert to negation normal form with De Morgan laws then distribute OR over AND
• for DNF, convert to negation normal form with De Morgan laws then distribute AND over OR

我不清楚您的公式是否量化。但是，即使不是，看来合取范式，它-在自动定理证明者世界中大致等同-从属正规形式 alter ego概述了一种可用的算法（如果您想使这种转换更加巧妙，请指向引用）。如果您还需要更多，请告诉我们更多有关您遇到困难的地方。

It's unclear to me if your formulae are quantified. But even if they aren't, it seems the end of the wikipedia articles on conjunctive normal form, and its - roughly equivalent in the automated theorm prover world - clausal normal form alter ego outline a usable algorithm (and point to references if you want to make this transformation a bit more clever). If you need more than that, please do tell us more about where you encounter a difficulty.

这篇关于在哪里可以找到将任意布尔表达式转换为合取或析取范式的方法？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！