logic - 求解命题逻辑规则集中的特定组合(SAT Solver)

Question

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

它们看起来像这样:

A → B ∨ C ∨ D

C → ¬F

F ∧ G → D

...

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

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

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

(A) ∧ (B)

(A) ∧ (C ∨ F)

(B ∨ G)

...

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

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

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

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

Answer 1

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

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

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