验证组合CNF SAT编码？

Question

我试图用卫星解算器来解决一个组合问题。

​

这涉及以下步骤：

1. 将问题编码为布尔表达式集。
2. 将表达式的连词转换为CNF/DIMACS (使用国产工具，bc2cnf、bool2cnf或林伯勒)
3. 解CNF (使用隐孢子虫、平岭、卡环或Z3等SAT解决方案)
4. 将解决方案(假设"SAT“结果)转换回问题域

这在我的情况下适用于小样本。但对于更具挑战性的问题，SAT求解者需要数小时甚至几天才能得出SAT/UNSAT的结论。我试图调整我的编码，以得到一个解决方案。但是，我在编码中付出的努力越多，我就越不确定我的编码实际上是正确的(即“可满足性等效”)。

从布尔表达式到CNF的步骤对于一个可管理的子句和变量的数目来说是非常复杂的。等待SAT求解者等待很长时间，但不确定时间是否在正确的轨道上，这是痛苦的。

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

我的问题：

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

从文献中，我知道了一些问题的解决方案，我可以将这些问题转化为可变的赋值，以获得对我的编码过程的信任。但是由于将军澳编码的存在，我的CNF中的大部分变量都是辅助(开关)变量。如果没有将军澳编码，我的CNF就太大了，无法解决。因此，我不能简单地检查每个CNF条款是否都由已知的解决方案来执行。

我尝试使用cnf2aig将CNF转换回布尔表达式，但该工具仍处于初级阶段。在没有切换变量的情况下，很容易根据主要问题变量的布尔表达式检查辅助。

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

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

Answer 1

所以你要问的是：

给定一个布尔表达式B和CNF C，是否有一种方法可以判断它们是否相等？

换言之：

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

我对这个问题的解决办法如下：

1. 我会使用一个已知的好软件(例如，未优化的代码或第三方工具)从布尔表达式中生成一个已知的、良好的CNF。
2. 使用Tseitin从C和D生成CNF，即将C的CNF解释为和(分离的连词)的乘积，并反演整个表达式。让我们调用生成的CNFs C‘表示C的逆，D’表示D的逆。 因此，满足C的模型不满足C‘，反之亦然。D和D‘相似。
3. 使用SAT求解器来寻找满足C和D‘的模型。这样一个模型可以满足C，但不满足B。
4. 使用SAT求解器来寻找满足C‘和D的模型，这样的模型可以满足B，但不满足C。
5. 如果步骤3和步骤4都不能生成模型(unsat)，那么您已经证明了B和C是相等的。

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

根据您的问题，解决步骤3和步骤4在计算上可能相当昂贵。因此，这种方法可能是可行的，如果您可以将您的问题分成更小的块，这些块可以相互独立地进行验证。

我希望这能帮上忙。您已经说过您正在努力确保您的优化是正确的，因此您应该有一个已知的好的实现。否则，您可以使用我编写的库作为外部引用：

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

这个库生成的CNF不是很有效！但它经过了很好的测试..。