标签: conjunctive-normal-form

所以我在Visual Studio 2010中编写了一个查询(我的意思是我打开了服务器资源管理器,右键单击了服务器并选择了New Query).查询包括条件

A AND B AND C AND D AND E AND F AND (G OR H)

这是联合正常形式(CNF).当我运行查询(附加到MSSQL Server 2008)时,它将文本更改为

A AND B AND C AND D AND E AND F AND G OR
A AND B AND C AND D AND E AND F AND H

这是析取正常形式(DNF).

从我在网上找到的小东西看来,似乎DNF允许SQL分别运行连接并在最后联合它们.

然而,对于像这样的事情,有这么多重复的条件,DNF实际上是否优于CNF？如果没有,我如何强制优化器按原样处理条件？如果是这样,我应该在我的应用程序代码中以CNF格式编写查询,因为它更短更整洁或以DNF形式,因为它为优化器节省了时间？

我有一个逻辑表达式,我想评估.表达式可以嵌套,由T(True)或F(False)和括号组成.括号"("表示"逻辑或".彼此旁边的两个术语TF(或彼此旁边的任何其他两个组合)应该是ANDED(逻辑与).

例如,表达式:

((TFT)T) = true

我需要一个算法来解决这个问题.我想到首先将表达式转换为析取或连接的正规形式,然后我可以轻松地评估表达式.但是,我找不到一个规范化表达式的算法.有什么建议？谢谢.

问题陈述可以在这里找到:https: //icpcarchive.ecs.baylor.edu/index.php？option = com_onlinejudge&Itemid = 2&category = 378&page = show_problem&issueble = 2967

编辑:我误解了部分问题.在给定的逻辑表达式中,AND/OR运算符与每个括号"(")交替.如果我们要通过树表示表达式,则AND/OR运算符取决于子树的深度级别.但是,它是最初认为最深层的树是AND树.我的任务是通过构建树来评估给定的表达式.感谢下面的答案,澄清了问题的正确要求.

我有一个像字符串的字符串

     s="(=> P (OR (AND A (NOT B)) (AND B (NOT A))))";

并将其转换为该字符串的CNF，例如

（或（非P）（或AB））（或（非P）（或（非B）（非A）））

我需要构造一个TreeTree来保留值吗？

     struct TreeNode {
            string val;         // The data in this node.
            TreeNode *left;   // Pointer to the left subtree.
            TreeNode *right;  // Pointer to the right subtree.
            //TreeNode *farther;//should I use farther or not in convert to CNF?
      };

如何使它成为合取范式的CNF？请提供一些算法细节。从我的角度来看，也许使用递归函数可以更好地解决此问题，但是我仍然想不出如何使用递归。或者您有解决此问题的其他建议？

当试图在计算机上解决逻辑问题时，通常首先将它们转换为 CNF，因为最好的求解算法都希望 CNF 作为输入。

对于命题逻辑，这种转换的教科书规则很简单，但如果按原样应用它们，结果是非常罕见的情况之一，即程序遇到双指数资源消耗而没有专门为此而构建：

a <=> (b <=> (c <=> ...))

使用 N 个变量，生成 2^2^N 个子句，在等价到 AND/OR 的转换中一个指数爆发，另一个在 OR 到 AND 的分布中。

解决这个问题的方法是重命名子项。如果我们将上面的内容重写为类似

r <=> (c <=> ...)
a <=> (b <=> r)

其中r是一个被定义为等于子项的新符号 - 通常，我们可能需要 O(N) 这样的符号 - 可以避免指数爆炸。

不幸的是，当我们尝试将其扩展到一阶逻辑时，这会遇到问题。使用 TPTP 表示法，其中?表示“存在”且变量以大写字母开头，请考虑

a <=> ?[X]:p(X)

诚然，这种情况很简单，实际上不需要重命名子项，但有必要使用一个简单的情况来说明，因此假设我们使用的算法只是自动重命名等价运算符的参数；这一点可以推广到更复杂的情况。

如果我们尝试上述技巧并重命名?子项，我们会得到

r <=> ?[X]:p(X)

存在变量被转换为 Skolem 符号，因此最终为

r <=> p(s)

然后原始公式扩展为

(~a | r) & (a | ~r)

其构造相当于

(~a | p(s)) & (a …

我正在使用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表达式示例:

O0 = (B0&!B1&!B2&B3) | (!B0&B1&B2&B3) | (!B0&!B1&B2&B3) | (B1&!B3) | (!B0 &!B2&!B3);

O1 = (B0&B1&!B2&B3) | (B0&!B1&B2&!B3) | (B0&B1&B2&!B3) | (!B0&!B1&B2&!B3) | (!B0&!B1&!B2&B3) | (!B0&!B1&B2&B3) | (!B0&!B2&!B3);

O2 = (B0&!B1&!B2&B3) | (B0&!B1&B2&!B3) | (B0&B1&B2&B3) | (!B0&B1&!B3) | (!B0&!B2&B3) | (!B0&!B1&B2&B3);

O3 = (!B0&B1&!B2&!B3) | (B0&B1&B2&B3) | (!B0&B1&B2&B3) | (B0&B1&B2&!B3) | (B0&!B1&!B2) | (!B0&!B1&B2&!B3) | (!B0&!B1&!B2&B3);

所以,这是一个实际的问题; 按优先顺序排列:

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

您是否知道任何可以理解(或可以教授)各种门类型的布尔逻辑最小化工具,而不仅仅是为PAL制作CNF？

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

如果你不知道它的算法,你知道或者可以想到任何有用的启发式方法吗？

(并且,以防万一你建议它 - 测试显示GCC和ICC(或者,我敢打赌,现有的任何其他C编译器)都不够聪明,不能从CNF表达式为我做特定于处理器的最小化 - 这真的很不错,但是检查两个-O3 -S的输出显示它们甚至无法捕捉到可以使用XOR的情况.

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

vx(t).
vx(f).
vy(t).
vy(f).
vz(t).
vz(f).

x(X) :- X=t; \+ X=f.
y(Y) :- Y=t; \+ Y=f.
z(Z) :- Z=t; \+ Z=f.
nx(X) :- X=f; \+ X=t.
ny(Y) :- Y=f; \+ Y=t.
nz(Z) :- Z=f; \+ Z=t.

cnf :-
   (nx(X); y(Y); nz(Z)),
   (x(X); ny(Y); z(Z)),
   (x(X); y(Y); z(Z)),
   (nx(X); ny(Y); z(Z)),
   write(X), write(Y), write(Z).

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

我正在尝试寻找解决问题的实用方法(例如在工程方面的努力),其中我有一堆未知值:

val a: Int32 = ???
val c: Int32 = ???
val d: Bool = ???

和表达式二进制树(在内存中),最终返回一个布尔值,例如

((a > 4) || (b == (c+2))) && (a < b) && ((2*d)) || e

我有的布尔运算符and or xor not和32位整数有比较的东西,以及加法,乘法,除法(注意:这些必须尊重32位溢出!)以及一些按位的东西(移位,按位&,| ^).但是,我不一定需要支持所有这些操作[参见:LOL_NO_IDEA]

我想得到三个答案中的一个:

• ES_POSSIBLE [我不需要知道如何,只是被告知它有可能存在的方式]
• 不可能[无论我的变量保持什么值,这个方程永远不会是真的]
• LOL_NO_IDEA [如果问题太复杂或耗时,这是可以接受的]

我正在解决的问题都不是太大或太复杂,而且条款太多(最多的是大约数百个).并且有大量的LOL_NO_IDEA可以.然而,我正在解决数以百万计的这些问题,因此不断的成本将会刺痛(例如转换为文本格式,并唤起外部解算器)

因为我是用scala做的,所以使用SAT4J看起来非常吸引人.虽然,文档很糟糕(特别是像我这样的人,他们只关注这个SAT世界几天)

但我目前的想法是,首先将每个Int32变为32个布尔值.这样我可以通过将它作为嵌套布尔表达式来表达像(a <b)这样的关系(比较msb,如果它们是eq,那么下一个等等)

然后当我有一个布尔变量和布尔表达式的大表达式树时 - 然后遍历它,同时逐步建立一个:http: //en.wikipedia.org/wiki/Conjunctive_normal_form

然后将其喂入SAT4J.

然而,所有这些看起来都非常具有挑战性 - 甚至构建CNF似乎效率很低(以天真的方式做,我实现它)并且容易出错.更不用说尝试将所有整数数学编码为布尔表达式.而且我无法为像我这样的人找到好的资源,一个想要使用SAT解决问题的工程师主要是一个黑盒子

我很感激任何反馈,即使它像"哈哈,你的白痴 - 看看X"或"是的,你的想法是正确的.享受!"

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

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

是否有任何自动cnf文件转换器,以便我可以直接给坐在求解器？

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