问题标签 [conjunctive-normal-form]

我想以析取范式（DNF）压缩正命题公式。

我暂时只假设没有否定文字的简单 DNF。逆过程，解压可以很容易地定义。对于仅由合取和析取组成的公式，以下重写规则将生成 DNF：

下面是一个解压的例子：

现在我想知道是否有一些算法可以从 DNF 生成单个公式。我已经研究过二元决策图。我对这些的问题是它们不能在途中结合所有的析取。

例如，使用共享的二元决策图算法，在打印过程中仍会显示类似的分支和/或引入新的介词变量，这两件事都是不希望的：

结果应该是一个公式，不再是 DNF，它比仅使用析取和合取的二元决策图算法以及原始 DNF 中已经找到的介词变量更紧凑。这是所需压缩的示例：

你会怎么做？首选 Prolog 实现。

再见

我有一个想要评估的逻辑表达式。表达式可以嵌套，由 T (True) 或 F (False) 和括号组成。括号“（”表示“逻辑或”。两个术语 TF 并排（或任何其他两个并排的组合）应为 ANDED（逻辑与）。

例如，表达式：

我需要一个算法来解决这个问题。我想首先将表达式转换为析取或合取范式，然后我可以轻松地评估表达式。但是，我找不到使表达式标准化的算法。有什么建议么？谢谢你。

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

编辑：我误解了部分问题。在给定的逻辑表达式中，AND/OR 运算符与每个括号“(”交替出现。如果我们要用树来表示表达式，那么 AND/OR 运算符取决于子树的深度级别。但是，它是最初考虑到最深层次的树是与树。我的任务是可能通过构建树来评估给定的表达式。感谢下面的答案澄清了问题的正确要求。

我已经编写了一些代码来根据此处描述的标准从存储 cnf 的文件中加载 cnf 。

该文件是：

我想将它加载到 [[1, -3][2,3,-1]]

我编写的代码有效，但对我来说似乎很难看。我很想对此有一些反馈。（我是 python 新手）。

谢谢 ！

一个给定的例子，两个问题，两个想法：

1）在自然语言中是什么意思？

有at(opic)，当as(tudent)在a(rtificial intelligence)中了解到t(opic)并且没有分心，这个s(tudent)通过a(i)中的考试

2）它的CNF是什么？

你怎么看？

我正在使用 Z3 解决可满足性问题，包括数百个 XOR 子句，每个子句有 22 个输入。为了以 DIMACS 形式编码 XOR 子句，我使用了 Tseitin 编码。我的转换将 XOR 分解为更小的 CNF 子句，每个子句最多五个字面值。到目前为止，Z3 无法设计 SAT 解决方案。

我可以/应该做些什么来改进我的编码？

我看过高斯消元法，但这可能没有帮助，因为 XOR 表达式没有相同的输入变量。

假设您有一个 CNF 公式，其中一些变量标记为特殊。
有没有办法让 SAT Solver（比如 minisat）找到一个解决方案，最大化分配给 true 的特殊变量的数量？

我必须构建一个函数来确定我是否有以这种方式构建的格式良好的公式的合取：

cong ::= '(' and wff wff ...')'

假设我有确定公式是否为 wff 的代码。该函数必须首先检查列表的第一个元素是否是'and ，然后递归地检查其余的子列表是否是 wff。请注意，这 p也是一个 wff，因此它不一定是子列表。

例子 ：(and (or a b v) (and a b d) m n)

这是我尝试过的对我不起作用的方法：

我正在尝试寻找解决问题的实用方法（例如，在工程方面），其中我有一堆未知值：

和一个表达式二叉树（在内存中），最终返回一个布尔值，例如

我拥有的布尔运算符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 似乎也非常低效（以天真的方式进行，我会实现它）并且容易出错。更不用说尝试将所有整数数学编码为布尔表达式。而且我还没有找到为像我这样的人设计的好资源

我会很感激任何反馈，即使它就像“大声笑，你是个白痴——看看 X”或“是的，你的想法是正确的。享受吧！”

我有一个类似字符串的字符串

并将其转换为输出此字符串的 CNF，例如

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

我需要制作一个结构 TreeNode 来保持价值吗？

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

I'm trying to do CNF operator in Java and I have an error with equality.

Firstly, I did most of the software but I didn't do totally.

My codes are here :

The problem is the equality.

The program should check the variables is true or false.

For instance :

this program does like bellow:

give a number for p : 1(user will give a number one (true) or zero(false))
give a number for q : 0
give a number for s : 1
give a number for t : 0
give a number for k : 0
(if the variable use more than one, program will ask once)

If we look at these variables, we can see that (1 or 0 or 1 or 0 or 0) and (1 or 0) It will return true but I can't do this. I can't understand how to do it.

Best wishes.