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. ...

我的问题是如何解决这个问题。我之前问过类似的问题(Tool to solve propositional logic / boolean expressions (SAT Solver?))，但焦点不同，现在我又陷入困境。或者我只是不明白。

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

另一种选择是，我将组合添加到规则集中，然后运行普通的 SAT 求解器。但我必须对每个我想检查的表达式执行此操作。

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

Answer 1

我所知道的最好的方法是使用“假设下的增量求解”技术。它的动机与您遇到的相同问题:多个 SAT 实例(CNF 公式)，它们具有一些常见的子公式。 形式上，CNF 中有一些核心 bool 公式 C。并且您有一组假设 {A_i}, i=1..n，其中 A_i 也是 CNF 中的 bool 公式。

在步骤 0 中，您向求解器提供核心公式 C。它尝试解决这个问题，向您说出结果并保存其状态(我们将此状态称为核心状态)。如果公式C可满足，则在步骤i中，您向求解器提供假设A_i，并且它会从核心继续执行状态。实际上，它试图求解公式C ∧ A_i，但不是从一开始就求解。

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