1

我正在尝试使用SAT Solver来解决组合问题。

在此处输入图像描述

这涉及以下步骤：

  1. 将问题编码为一组布尔表达式。
  2. 将表达式的连词翻译成CNF/DIMACS
    （使用自制工具bc2cnf、bool2cnf或Limboole）
  3. 求解CNF
    （使用 SAT 求解器，如Cryptominisat、Plingeling、Clasp或Z3）
  4. 将解决方案（假设为“SAT”结果）转换回问题域

这适用于我的小样本。但对于更具挑战性的问题，SAT 求解器需要数小时甚至数天才能得出 SAT/UNSAT 结论。我尝试调整我的编码以获得解决方案。但是我在编码上投入的精力越多，我就越不能确定我的编码实际上是正确的（即“可满足性等效”）。

从布尔表达式到 CNF 的步骤相当复杂，在可管理数量的子句和变量方面是有效的。等待 SAT 求解器的时间很长并且不确定时间是否花在正确的轨道上是很痛苦的。

布尔表达式可能是错误的。因此，我想验证 CNF 实际上代表了原始问题，而不仅仅是布尔表达式。

我的问题：

我如何验证给定的编码是原始布尔表达式的有效表示？

从文献中，我知道了一些问题的解决方案，我可以将其转化为变量分配，以获得对我的编码过程的信任。但是由于Tseitin encoding，我的 CNF 中的大多数变量都是辅助（切换）变量。如果没有Tseitin encoding，我的 CNF 将太大而无法解决。因此，我不能简单地检查已知解决方案是否满足每个 CNF 子句。

我曾尝试使用cnf2aig将 CNF 转换回布尔表达式，但该工具仍处于起步阶段。在不切换变量的情况下，可以直接根据主要问题变量的布尔表达式检查分配。

有一些关于“CNF 到电路”方法的出版物，但没有一个提供可用的工具。

是否有任何最佳实践来完成这样的检查？

4

1 回答 1

1

所以你要问的是：

给定一个布尔表达式 B 和一个 CNF C，有没有办法判断它们是否可满足？

或者换句话说：

是否存在满足 B 但不满足 C 或满足 C 但不满足 B 的模型？如果不存在这样的模型，那么两者都是等值的。

我对该问题的解决方案如下：

  1. 我会使用已知良好的软件（例如，您未优化的代码或第三方工具）从布尔表达式生成已知良好的 CNF D。

  2. 使用 Tseitin 从 C 生成 !B 的 CNF，DIe 将 C 的 CNF 解释为和的乘积（析取的结合）并反转整个表达式。让我们将生成的 CNF C' 称为 C 的倒数，将 D' 称为 D 的倒数。

    因此，满足 C 的模型不会满足 C'，反之亦然。D 和 D' 类似。

  3. 使用 SAT 求解器找到满足 C 和 D' 的模型。这样的模型将满足 C 但不满足 B。

  4. 使用 SAT 求解器找到满足 C' 和 D 的模型。这样的模型将满足 B 但不满足 C。

  5. 如果步骤 3. 和 4. 都没有产生模型（未满足），那么您已经证明 B 和 C 是可等满足的。

步骤 3. 和 4. 很简单。只需创建一个包含来自两个 CNF 的所有子句的大 CNF。来自 B 的所有变量必须在两个 CNF 中使用相同的文字进行编码，并且辅助变量必须从单独的池中分配。

根据您的问题，求解步骤 3. 和 4. 在计算上可能非常昂贵。因此，这种方法可能只有在您可以将问题拆分为可以相互独立验证的较小块时才可行。

我希望这会有所帮助。您说过您正在尝试确保您的优化是正确的，因此您应该有一个已知良好的实现。否则，您可以使用我编写的库作为外部参考：

https://github.com/cliffordwolf/yosys/tree/master/libs/ezsat

这个库生成的CNF效率不是很高！但它是很好的测试..

于 2014-01-17T17:32:40.803 回答