解决命题逻辑规则集中的特定组合(SAT求解器)

Question

在汽车行业，当你购买一辆汽车时，你有上千种不同的零部件可供选择。并不是每个组件都是可组合的，因此对于每个car，都有许多用命题逻辑表示的规则。在我的例子中，每辆车都有2000到4000条规则。

它们看起来是这样的：

1. →B∨C∨D
2. C→f
3. F∧G→D
4. ..。

其中"∧“=”和“/ "∨”=“或”/“=”不是“/ "→”=“含意”。

使用工具"limboole“(http://fmv.jku.at/limboole/)，我能够将命题逻辑表达式转换为联合范式。这是必要的，以防我不得不使用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中有一些核心布尔公式C。你有一组假设，{A_i}, i=1..n，其中A_i也是CNF中的布尔公式。

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

你可以很容易地找到一堆与这个主题相关的论文，在那里你可以找到很多信息。此外，您也可以检查您最喜欢的SAT-解决方案，以支持这项技术.