问题标签 [conjunctive-normal-form]

I am using Dr Racket to check if an expression passed is in Conjunctive normal form.

The code checks if the expression is in Negative normal form first.

is-nnf checks recursively whether the expression is in negative normal form.

I am trying to write a similar expression named is-cnf to recursively check if an expression is in conjunctive normal form.

is-constant -> checks if the expression is a constant (Eg #t, #f)

is-variable -> checks if the expression is a variable (Eg 'a, 'x)

is-not -> checks if the first element of the list is a 'not ( Eg. '(not x))

is-or -> checks if the first element of the list is a 'not ( Eg. '(or x y))

is-and -> checks if the first element of the list is a 'not ( Eg. '(and x y))

我目前正在尝试使用 SAT 求解器来解决难题“Kuromasu”，该求解器采用常见的 DIMACS 格式，即作为连接范式 (CNF) 的输入。

在 Kuromasu 中，您有一个带有 mxn 单元的矩形板。一个细胞要么是黑色的，要么是白色的。游戏的目标是决定哪个单元格是哪种颜色。一些单元格包含一个数字。包含数字的单元格始终为白色。该数字告诉您应该从该单元格中看到多少个单元格，包括其自身。同一行和同一列中的所有白色单元格都是可见的，直到第一个黑色单元格。

示例 5x4 网格，# 表示黑色单元格：

我需要制定这个约束，以 SAT 求解器理解的方式找到黑色区域的位置。我已经能够通过遍历编号单元格左侧、右侧、顶部、底部的所有单元格并检查将它们着色为黑色是否满足约束来为每个数字生成一个分离范式 (DNF) 版本。这给了我一份 DNF 中可能的黑细胞星座列表。我通过在每个单元格中引入一个变量来对游戏进行编码，如果为假，则为黑色，如果为真，则单元格为白色。以下是上述字段的所有变量（1 索引，因为 DIMACS 格式将假变量指定为负整数，将真变量指定为正对应）：

仅对于上面示例中的 2-number 约束，我将生成以下内容：

(-4 & -15) | (-3 & -10) (等式 1.)

这代表了可以遵循约束的两种方式。但是，要将其输入到 SAT-Solver，我需要将 (Eq 1.) 转换为 CNF。我实现了一个（简单的）转换器，它可以工作，但由于转换为 CNF的复杂性，它确实很慢且内存密集。对于有超过 4 种方式来实现它们的约束，这样做是不可行的。

如何以可以直接提供给 Solver 的方式制定约束？可能吗？这个问题我想了好久，还是搞不明白。

谢谢！

子句范式中的逻辑语句的元素称为文字。

例如，给定子句{a, !b}

字面量是a, !b。

但是假设你想获得元素的集合，不管它们是否被否定。

'无符号文字'（？）是a, b.

什么是比“无符号文字”更好/更标准的术语？我想有人可以说“变量”，但在它们可能是常数或本身就是复杂术语的情况下，这似乎不协调。

我正在用 C 语言实现一个 MAX-3SAT 求解器。显然，有很多关于联合范式的布尔公式的文献。我打算以以下格式存储它们：

这是一个变量 ID 数组的数组，其中变量为负表示否定（就像在标准 DIMACS CNF 格式中一样）。

这是我的问题：我应该了解 3SAT 的任何“聪明”数据结构吗？也许可以提高求解算法性能的结构？

我在处理布尔逻辑公式时看到的大多数事情都是首先将其转换为 CNF 或 DNF 形式。维基百科说它“在自动定理证明中很有用”，但仅此而已。

想知道为什么需要执行这一步，在哪个算法中利用了它的哪个方面等等。如果不知道更多，似乎一些标准算法会利用这个特性，那么所有后续论文都会有将其声明为一项要求。但也许没有必要。

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

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

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

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

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

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

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

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

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

然后原始公式扩展为

这在构造上相当于

但这是不正确的！假设我们没有进行重命名，只是按原样扩展原始公式，我们会得到

这与我们通过重命名获得的版本截然不同。

问题是等价需要每个论点的正面和负面版本，但是将否定应用于包含全称或存在量词的术语，会在结构上改变这些术语；您不能只将它们封装在定义中，然后将否定应用于定义的符号。

这样做的结果是，当你有等价并且参数可能包含这样的量词时，你实际上需要重复每个参数两次，一次用于正版本，一次用于负版本。这足以带回我们希望通过重命名来避免的存在性爆炸。据我所知，这个问题不是由特定算法的工作方式引起的，而是由任务的性质引起的。

所以我的问题：

给定一个可能包含等价和量词的任意嵌套的输入公式，是否有任何算法可以正确地将其转换为具有多项式而不是指数子句数的 CNF？

许多论文都在使用 SAT，但很少有人提到如何将附加项转换为 CNF。

由于 CNF 只允许 AND OR NOT 运算，因此很难描述加法运算。例如，

1. 将这些方程映射到布尔电路中。
2. 将 Tseitin 变换应用于电路并将其转换为 DIMACS 格式。

但是有什么方法可以读取结果吗？我确实认为如果所有变量都是我们自己定义的，则可以读取结果，因此有必要弄清楚如何将线性约束转换为 SAT 问题。

如果有3或4个变量，即x1+x2+x3 <3，我们可以用真值表来解决这个转换。另外，直接的方法是从1600个变量中选择29个（任何小于30的数字）为1，其他为0。但是有太多的可能性使得这个问题很难解决。

我使用过 STP，但它只能给出 1 个答案。随着变量和子句数量的增加，STP 的运行时间也越来越长。

所以我尝试用SAT来解决STP给出的cnf，它可以在几分钟内给出答案。但无法读取结果。

最后，我找到了一些论文，1. Encoding Linear Constraints with Implication Chains to CNF，2. SAT-Based Techniques for Integer Linear Constraints。这可能会有所帮助。

我正在做一个项目，我必须创建一个使用 SAT 求解器解决 N 皇后问题的程序。我已经将约束转换为联合范式，现在正在编写 DIMACS 文件的代码。然而，我有一个问题。我打算给用户 2 个选项：

第一个选项是让用户给出某些皇后的位置，然后让 SAT 求解器找到该特定设置的解决方案。

第二个选项是 SAT 求解器打印问题的所有解决方案。例如，对于 n=4，它将打印两个解决方案，对于 n=5，所有 10 个解决方案，依此类推

我的问题是第二个选项。有没有办法通过循环多次调用 SAT 求解器以找到所有解决方案？

关于合取范式中的公式，下列哪项是正确的？

A. 对于任何公式，都有一个真值分配，至少有一半的子句评估为真。

B. 对于任何公式，都有一个真值赋值，所有子句的计算结果都为真。

C. 有一个公式，对于每个真值赋值，至多四分之一的子句评估为真。

D. 以上都不是。

我的疑问：我知道合取范式是求和形式的乘积，但是这个问题让我很困惑，请用简单的语言解释一下。

SAT 求解器可用于解决旅行商问题，其中所选边之间的成本总和很重要。我了解到您随后要求求解器再次寻找较低的成本。该最大值如何以合取范式表示？