验证组合CNF SAT编码？(Verify Combinatorial CNF SAT Encodi

我试图通过使用来解决一个组合问题SAT求解。

这包括以下步骤：

这适用于我的情况下，在小样本。但更具挑战性的，在SAT求解器需要几个小时甚至几天不来一个SAT / UNSAT结论。我试着调整我的编码，以达成解决办法。但更多的努力我把我的编码，少肯定我可以为我的编码实际上是正确的（即“可满足等价物”）。

从布尔表达式到CNF的步骤是颇为曲折是有效的条款和变量的可管理数量方面。这是痛苦的等待年龄的SAT求解器，而不是肯定的是，时间花费在正确的轨道上。

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

我的问题：

我怎么能验证一个给定的编码是原始布尔表达式的一个有效的代表性？

从文学，我已经知道了一些问题，我可以转化为变量赋值在我的编码过程中获得信任的解决方案。但由于Tseitin编码，大部分在我的CNF的变量是辅助（开关）变量。如果没有Tseitin编码，我CNF将远远太大，是可以解决的。因此，我不能简单地检查每一个CNF条款是由已知的解决方案满足。

我曾尝试到CNF转换回使用布尔表达式cnf2aig ，但该工具还处于起步阶段。无需切换变量，它是简单的所要检查的首要问题变量的布尔表达式的分配新建分配FY。

有“到电路CNF”办法一对夫妇约出版物的，但它们都没有提供一个可用的工具。

有没有办法实现这样的检查任何最佳做法？

所以，你问的是：

给定一个布尔表达式B和一个CNF C，有没有办法知道，如果他们是equisatisfiable？

或者换句话说：

存在满足B而不是C，或满足C，但不是B模式？如果没有这样的模式存在，那么两者都equisatisfiable。

我对这个问题的解决办法是以下几点：

我会使用已知良好的软件（例如，您的未经优化的代码或第三方工具），以从布尔表达式生成已知良好的CNF d。
使用Tseitin生成CNF从！C B和死解释为CNF C作为款项（析取的结合）的产品和反转整个表达式。让调用所得的CNF C“为C和d逆”为D的逆
因此，满足C将不能满足C”，反之亦然模型。为d和d类似”。
使用SAT求解器找到满足C和d”的典范。这种模式将满足C，但不是B.
使用SAT求解器找到满足C和D.这种模式将满足B，而非C.模型
如果步骤3和4都不会产生一个模型（不饱和度），那么你已经证明，B和C是equisatisfiable。

步骤3和4很容易。只要创建一个大的CNF包含来自两个碳纳米纤维的所有条款。所有的B变量必须在两者的CNF和辅助的变量相同的文字，必须从单独的池分配进行编码。

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

我希望帮助。你说你想确保你的优化是正确的，所以你应该有一个已知良好的实现。否则，你可以使用我已经写作为外部参考库：

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

这个库所产生的CNF是不是很有效！但它是很好的测试..