问题标签 [satisfiability]

在急切的 SMT 求解器中，SMT 公式被编码为可等满足的布尔公式，该公式被馈送到 SAT 求解器。通常，对于 QF_UF 公式，未解释的函数通过 Ackermann 归约或 Bryant 归约进行归约，然后通过等式图方法构造一个等值的布尔公式。

所以我想知道是否可以调用现有的 SMT 求解器来获得给定 QF_UF 公式的等值布尔公式，而无需破解求解器的低级实现。比如 Z3 有一些转换输入问题的策略（比如tseitin-cnfand elim-term-ite），有没有这样的转换策略？

我在 Z3 中经常使用最小化功能，我担心一些可伸缩性问题（当我最小化的变量数量增加时）。“最小化”的底​​层算法是什么，有没有一种通用的方法来加快速度？

我有布尔公式 A 和 B 并想检查“A -> B”（A 暗示 B）在多项式时间内是否为真。

对于完全通用的公式 A 和 B，这是 NP 完全的，因为““A -> B”为真”与“非 (A -> B)”不可满足。

我的目标是找到有用的限制，使多项式时间验证成为可能。我也有兴趣找到 O(n) 或 O(n log n) 限制（n 是某种长度 |A| 或 |B|）。我宁愿限制 B 而不是 A。

一般来说，我知道以下几类“更简单”的布尔公式：

• （可重命名）Horn 公式可以在线性时间内求解（它们是 CNF 形式，最多有一个正变量）。
• DNF 形式的所有公式都很容易检查
• 2-SAT 是 CNF 公式，每个子句最多 2 个变量，可在线性时间内求解。
• XOR-SAT 是具有 XOR 而不是 OR 的 CNF 公式。它们可以通过 O(n^3) 中的高斯消元法求解

主要问题是我有公式“A -> B”又名“（不是 A）或 B”，对于非平凡的 A/B，它很快就变成了非 CNF 和非 DNF。

如果我正确理解了 Tseytin 转换，那么我可以使用 O(|X|) = O(|Y|) 将任何公式 X 转换为 CNF Y，因此我可以假设 - 如果我愿意 - 我在 CNF 中有我的公式。

有一些唾手可得的果实：

• 如果 |B| 是恒定且小的，我可以枚举 B 的所有解决方案并检查它们是否产生真正的 A。
• 同样，如果 |A| 是常数且很小，我可以枚举 A 的所有解决方案并检查它们是否产生错误的 B

更有趣的是：

• 如果 B 在 DNF 中，那么我可以将 A 转换为 CNF，这将使“（不是 A）或 B”DNF 可以在线性时间内求解。
• 对于一般 B，如果 |B| 在 O(log |A|) 中，我可以将 B 转换为 DNF 并以这种方式解决

但是，我不确定如何使用其他更简单的类，或者是否可能。

由于分布性，CNF 中的 A 或 B 几乎肯定会在试图将“（不是 A）或 B”带回 CNF 时呈指数级增长——如果我没记错的话。

注意：我的用例可能比 B 公式更复杂/更长。

所以我的问题归结为：是否存在有用的布尔公式 A 和 B 类别，使得“A -> B”可以在多项式（最好是线性）时间内得到证明？- 除了我已经提到的 4 个案例。

编辑：对此有不同的看法：在以下类别之一中，A 和 B 在什么条件下是“A -> B”：

• 在 DNF
• 在 CNF 和 Horn 公式 (Horn-SAT) 中
• 在 CNF 和二元公式 (2-SAT) 中
• 在 CNF 和一个算术公式（XOR 的 CNF）中

我在编程方面相当新，所以我希望有人能够在这方面为我指出正确的方向。

我有一个约 2400 人的列表，每个人至少有 23 个条件中的一个（如果他们有条件，每个人的条件是 1，如果没有，则为 0）。

EG 如果 Jon 有条件 1、5 和 6，Jon 的输出将是 {1,0,0,0,1,1,0,0...}。

然后，我将获得一份列表，列出每种条件需要多少人。因此，如果条件 1 的期望人数是 10 人，而条件 2 的期望人数是 5 人，我想要 10 人有条件 1 和 5 人有条件 2（如果两个人都有，一个人可以计入条件 1 和条件 2） .

此外，我必须准确选择 30 人，并尽量接近所需的条件数量，严格限制单个条件必须至少有 3 人且不超过 10 人。

有没有办法可以做到这一点，如果可以，我将如何去做？我尝试过暴力破解，但是大量的组合使我无法获得解决方案。

编辑：这是一个包含 5 个人和 4 个条件的小示例：

Person 1: {1,0,0,1} Person 2: {0,1,1,1} Person 3: {0,0,0,1} Person 4: {1,0,0,0} Person 5: {1,0,0,1}

所需的条件数 {2,1,1,2}。这个想法是我需要选择 3 个人并尽可能接近所需的条件数量。在此示例中，将选择人员 1、2 和 4。我必须将这个想法扩展到具有 23 个条件并选择 30 人的 2400 人列表（尽管它应该能够扩展到任何列表大小和任意数量的条件）并且不知道是否有 30 个成员的组合这将导致完全匹配。

这有助于澄清事情吗？

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

在汽车行业，当您购买汽车时，您有数千种不同的组件可供选择。并非每个组件都是可组合的，因此对于每辆汽车，都存在许多用命题逻辑表达的规则。就我而言，每辆车都有 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. 一般来说，我应该在谷歌中搜索什么来加深我对这个主题的了解？

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

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

给出了这个 XOR 子句：

翻译成CNF，就是：

这很清楚。

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

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

我不明白...

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

这里有没有人理解代码并能够回答我的一些问题？

For info: to_examine是一个队列并保存最近分配的变量。 var显然是一个变量，将检查它是否会导致冲突、传播或什么都没有。

我不明白的是如何DPLL(var)在第 3 行返回一个子句，我认为 DPLL 只能返回 true 或 false。

以及 DPLL 算法如何/为什么只接受第 3 行中的单个变量？

这个伪代码的来源是 Mate Soos 2009 年的博士论文。

在汽车行业，当您购买汽车时，您有数千种不同的组件可供选择。并非每个组件都是可组合的，因此对于每辆汽车，都存在许多用命题逻辑表达的规则。就我而言，每辆车都有 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 求解器。但是我必须为我要检查的每个表达式都这样做。

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

所以我有一个 cnf，以及两个变量 K 和 C 的列表。在将 K 的变量发送到 sat-solver 之前，K 的变量作为单位子句（取反或不取决于布尔数组）添加到 cnf。当 sat-solver 返回一个模型时，我只关心 C 中也出现的变量，模型中的所有其他变量都被丢弃。

由于 cnf 将重复运行（将 K 中的不同变量设置为 true 或 false），因此值得花几个小时来简化 cnf 并删除不必要的变量（不必要的是任何不在 K 或 C 中的变量) 如果这意味着每次要解决它时都要减少几分钟。

我的问题是我是否可以使用此 pdf或此博客文章中描述的分辨率变量消除来消除一些变量，只要我不消除 K 或 C 中出现的任何变量。或者这是否会改变结果模型到 C 中的变量？

假设我有一个带有 N 个输入和 1 个输出的黑盒电路。

我想固定 M 个输入的值并找到电路可满足的其余输入 (NM) 的值。如果我手动修复verilog RTL中的M个输入，并将其转换为CNF（使用abc），这会产生正确的结果吗？这是解决这类问题的正确方法吗？