问题标签 [sat]

我正在编写一个 SAT 求解器，并开始实施 DPLL 算法。我了解该算法及其工作原理，我还实现了它的一个变体，但困扰我的是接下来的事情。

这是什么意思，这Φ是一组一致的文字？我理解不一致意味着假，这意味着一致意味着不假。true那么，如果当前的分配没有证伪问题，为什么我们可以返回呢？

我实现我的 SAT 求解器的方式是，每当遇到使所有子句都为真的赋值时，我返回那个赋值，算法就完成了。但是由于对于给定的赋值，所有子句都必须为真才能成为问题的解决方案，我不明白，true如果赋值刚好满足问题，怎么能返回（我假设我弄错了在这里，但是既然如果Φ是一致的，那么就意味着它不是假的，但它仍然可以是不可判定的？）。

有没有办法提取 Z3 中的布尔/命题骨架以获得可满足的公式？

谢谢，

赫里希

我对命题逻辑和布尔表达式这个话题很陌生。所以这就是我需要帮助的原因。这是我的问题：

在汽车行业，当您购买汽车时，您有数千种不同的组件可供选择。并非每个组件都是可组合的，因此对于每辆汽车，都存在许多用命题逻辑表达的规则。就我而言，每辆车都有 2000 到 4000 条规则。

它们看起来像这样：

1. A → B ∨ C ∨ D
2. C → ¬F
3. F∧G→D
4. ...

其中“∧”=“和”/“∨”=“或”/“¬”=“非”/“→”=“蕴涵”。

变量 A、B、C、... 链接到物料清单中的组件。我拥有的数据由成对的组件及其链接变量组成。

例子：

1. 组件_1，组件_2：（A）∧（B）
2. 组件_1，组件_3：（A）∧（C∨F）
3. 组件_3，组件_5：（B∨G）
4. ...

现在，我的问题是如何解决这个问题。具体来说，我想知道组件的每种组合是否可以根据上述规则进行。

1. 哪些工具、软件和算法可以解决这类问题？
2. 有说明性的例子吗？
3. 如何实现自动化，以便检查列表中的每个组合？
4. 一般来说，我应该在谷歌中搜索什么来加深我对这个主题的了解？

非常感谢您的帮助！奥拉夫

我从这里（第 8、9 页）阅读了关于 NP 硬度的信息，在注释中，作者将 3-SAT 形式的问题简化为可用于解决最大独立集问题的图形。

在示例中，作者将以下 3-SAT 问题转换为图。3-SAT问题是：

生成的等效图是：

作者指出，两个节点通过一条边连接，如果：

1. 它们对应于同一子句中的文字
2. 它们对应于一个变量及其倒数。

我很难理解作者是如何提出这些规则的。

• 为什么我们需要在变量和它的逆变量之间画边？
• 假设有两个子句，子句 1 有 (a,b,~c)，子句 2 有 (~a,b,c) 来连接子句 1 和子句 2，为什么我们必须连接 a 和 ~a？为什么我们不能将 a (clause 1) 与 c (clause 2) 连接起来呢？

我正在努力进行以下 XOR 子句转换：

给出了这个 XOR 子句：

翻译成CNF，就是：

这很清楚。

但为什么(x1 ⊕ ¬x2 ⊕ x3) = (x1 ⊕ x2 ⊕ x3 ⊕ 1)呢？<-这被称为“标准形式”的 XOR 子句

为什么是(x1 ⊕ x2 ⊕ x3 ⊕ 1) <=> x1 ⊕ x2 ⊕ x3 = 0？

我不明白...

这是我得到的论文中的另一句话：“如果所有文字都出现在正相，则异或子句是标准形式。”

SAT 或 SMT 求解器是否已用于 AI 视频游戏？他们解决了哪些任务？我能找到的几乎所有东西都与谜题有关。

在汽车行业，当您购买汽车时，您有数千种不同的组件可供选择。并非每个组件都是可组合的，因此对于每辆汽车，都存在许多用命题逻辑表达的规则。就我而言，每辆车都有 2000 到 4000 条规则。

它们看起来像这样：

1. A → B ∨ C ∨ D
2. C → ¬F
3. F∧G→D
4. ...

其中“∧”=“和”/“∨”=“或”/“¬”=“非”/“→”=“蕴涵”。

使用“limboole”工具（http://fmv.jku.at/limboole/），我能够将命题逻辑表达式转换为合取范式（CNF）。如果我必须使用 SAT 求解器，则需要这样做。

现在，我想检查规则集中特定组件的可构建性可行性。例如，对于以下每个表达式或组合，我想检查它们在规则集中是否可行。

1. (A) ∧ (B)
2. (A) ∧ (C ∨ F)
3. (B∨G)
4. ...

我的问题是如何解决这个问题。我之前问过类似的问题（解决命题逻辑的工具/布尔表达式（SAT Solver？）），但焦点不同，现在我又被困住了。或者我只是不明白。

一种选择是使用规则集的 ALLSAT 方法计算所有解决方案。然后我可以检查每个组合是否是任何解决方案的一部分。如果是，我可以得出这种特定组合是可行的。

另一种选择是，我将组合添加到规则集中，然后运行普通的 SAT 求解器。但是我必须为我要检查的每个表达式都这样做。

您认为解决此问题的最优雅或更简单的方法是什么？

我尝试解决SAT 问题，特别是 3-SAT。我的数据集来自SATLIB，我使用Neuroph创建神经网络。在我的数据集中，一个短语的子句表示如下：

其中0 - 子句结尾，{1,2,3} - 变量，“-”（减号） - 否定。也就是这等于：

我的问题是不知道如何表示这个像神经网络的输入。基于这个答案，我将选择我需要的正确输入节点。

PS：我不知道它是否重要，但NN输出必须是“可以满足短语吗？”的答案。

我正在尝试使用名为：MAX_HS 的 max-sat 求解器开始。

该文档只是一个自述文件，内容不多，但很清楚您必须做什么： https ://github.com/fbacchus/MaxHS

我已经从 IBM 安装了 CPLEX 库并按照文档中的说明配置了文件，但是当我编译时出现错误，这是我的终端日志：

真的不知道什么会导致错误，因为该库是官方许可的 IBM cplex 库，唯一的设置是为 IBM 库分配正确路径的设置。我想我已经正确完成了这一步，因为当路径错误并且没有找到 IBM 库时，我又遇到了另一个错误。

有任何想法吗？

谢谢！

我正在尝试使用 SAT 求解器 (sat4j) 实现扫雷求解器，并且我对它们的工作原理有一个简单的了解。但我不知道的一件事是如何表示x+y+Z+....=2地雷，因为 SAT 求解器使用布尔输入。如下表所示：

你可以写a+b+c+f+g+i+j+k = 2和c+d+e+g+h+k+l+m= 3。