logic - 解决命题逻辑规则集中的特定组合（SAT Solver）

Question

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

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

Answer 1

我知道的最好的方法是使用“假设下的增量求解”技术。它的动机与您遇到的相同问题：多个 SAT 实例（CNF 公式）具有一些共同的子公式。C形式上，您在 CNF 中有一些核心布尔公式。你有一组假设{A_i}, i=1..n，A_iCNF 中的布尔公式也在哪里。

在步骤 0 中，您向求解器提供您的核心公式C。它试图解决它，告诉你一个结果并保存它的状态（我们把这个状态称为core-state）。如果公式C是可满足的，则在i您向求解器提供假设的步骤中，它会从core-stateA_i继续执行。实际上，它试图解决一个公式，但不是从一开始就解决。C ∧ A_i

您可以轻松找到一堆与该主题相关的论文，其中包含大量信息。此外，您可以查看您最喜欢的 SAT-solver 是否支持此技术。