问题标签 [conjunctive-normal-form]

我有一个库，我必须与之交互，它基本上充当数据源。检索数据时，我可以将特殊的“过滤器表达式”传递给该库，然后将其转换为 SQL WHERE 部分。这些表达非常有限。它们必须是合取范式。喜欢：

这对于编程来说当然不是很舒服。所以我想制作一个小包装器，它可以解析任意表达式并将它们转换为这种正常形式。喜欢：

会被翻译成类似的东西：

我可以使用Irony库将表达式解析为树。现在我需要对其进行规范化，但我不知道如何......哦，还有，这是扭曲：

• 最终表达式可能不包含NOT运算符。但是，我可以通过将运算符替换为逆运算符来反转各个项。所以，这没关系：
  
  (not A or not B) AND (not C or not D)
  
  但这不是：
  
  not (A or B) and not (C or D)
  
  
• 我想让表达式尽可能简单，因为它将被翻译成几乎相同的 SQL WHERE 语句，因此复杂的语句很可能会降低执行速度。

如果我有一个像这样的公式：

（FA = 全部 / E = 存在）

skolemisation 的规则说：

1. 如果 E 在 FA 之外，则替换为常数或
2. 如果 E 在 FA 内部，则用新函数替换包含 FA 外部的所有变量作为参数。

那么在这种情况下我该怎么办？我可以只删除 Exists 量词还是用常数替换它？

谢谢！

我正在使用Espresso 逻辑最小化器来生成一组布尔方程的最小化形式。然而，我希望在标准微处理器上实现这些，而不是为可编程阵列逻辑（这是 Espresso 通常用于）生成逻辑。问题是 Espresso 以合取范式产生输出，这对于 PAL 来说是完美的，但对于 x86 或 PPC 来说不是最佳的。

例如，Espresso 完全忽略 XOR - 在下面的 Espresso 输出中，子表达式(!B0&!B1&B2&!B3) | (!B0&!B1&!B2&B3)等价于(!B0&!B1&(B2^B3)). 这种替换确实增加了表达式的门深度/关键路径，但考虑到我正在查看具有足够数量的术语以完全饱和周围任何 CPU 的执行资源的表达式，折衷一些门深度来减少似乎是合理的指令总数。我还想扩展它以了解如何使用我感兴趣的某些处理器上可用的 ANDC 或 NOR 等指令。

我正在查看的 CNF 表达式示例：

因此，要使这成为一个实际问题；按优先顺序：

你知道 Espresso 的选项或扩展会产生我想要的那种表达吗？

您是否知道任何理解（或可以教授）各种门类型的布尔逻辑最小化工具，而不仅仅是为 PAL 生成 CNF？

您是否知道将上述 CNF 表达式转换为使用其他类型门的表达式的算法？

如果您不知道它的算法，您是否知道或可以想到任何有用的启发式方法？

（而且，以防万一你要建议它 - 测试表明 GCC 和 ICC（或者，我敢打赌，现有的任何其他 C 编译器）还不够聪明，无法从 CNF 表达式中为我执行特定于处理器的最小化- 这真的很好，但是检查 -O3 -S 的输出表明他们甚至无法捕捉到可以使用 XOR 的情况）。

我想将我的从句转换为合取范式。每次我运行我的程序时，条款都会改变，所以我想我需要在我的程序中内置一个工具来为我做这件事。有什么建议如何实施吗？我还发现了一些图书馆，例如：
Orbital library。我是逻辑编程的新手，我从未使用过它们，所以很难通过它们。我也试图找到一个例子来澄清事情，但没有任何结果。我正在用 java 语言构建我的程序。请帮忙...

提前致谢！

如果您将 3-cnf-sat 问题更改如下：
对于每个 c _i， c _i = -x _i1 OR -x _i2 OR x _i3意味着恰好有一个变量出现而没有否定。
您还可以为某些（或全部）x 赋予值（0 或 1）。
您应该能够在多项式时间内解决问题（找到满足问题或证明问题不可满足的 x 值）。

1. 解决这个问题的多项式运行时间算法是什么？
2. 证明它在多项式时间内运行。

提示：表明 c _i = -x _i1 OR -x _i2 OR x _i3等于 c = (x _i1 AND -x _i2 ) -> x _i3

我需要使用 sat 求解器来检查布尔表达式的可满足性..

我有这样的复杂布尔表达式

是否有任何自动 cnf 文件转换器，以便我可以直接将其提供给 sat 求解器？

我读了 cnf 格式文件.. 但是如何在 .cnf 文件中表达这个表达式？当括号内有连词以及如何表达 --> 和 <-> 时，我会感到困惑？请帮我

在学习 Prolog 时，我尝试编写一个解决 CNF 问题的程序（性能不是问题），所以我最终得到了以下代码来解决(!x||y||!z)&&(x||!y||z)&&(x||y||z)&&(!x||!y||z)：

有没有更简单、更直接的方法来使用这种声明性语言来解决 CNF？

所以我在 Visual Studio 2010 中编写了一个查询（我的意思是我打开了服务器资源管理器，右键单击服务器并选择了新查询）。查询包含条件

这是合取范式（CNF）。当我运行查询（附加到 MSSQL Server 2008）时，它将文本更改为

这是析取范式（DNF）。

从我在网上找到的一点点来看，似乎 DNF 允许 SQL 单独运行连接词并在最后合并它们。

但是，对于这样的事情，有这么多重复的条件，DNF 真的比 CNF 更有优势吗？如果不是，我如何强制优化器按原样接受条件？如果是这样，我应该在我的应用程序代码中以 CNF 形式编写查询，因为它更短更整洁，还是以 DNF 形式编写，因为它可以节省优化器的时间？

我正在努力使用MiniSat来解决约束满足问题。在一阶逻辑中，问题很容易用一些离散域变量和一些谓词来表示。

但是，MiniSat 以及我迄今为止看到的其他 CSP 求解器都希望他们以 CNF 形式输入。所以我正在寻找一种“预处理器”，它将一阶逻辑表达式转换为 CNF。

有什么想法吗？

布尔函数可以用析取范式 (DNF) 或合取范式 (CNF) 表示。谁能解释为什么这些表格有用？