验证组合CNF SAT编码？ [英] Verify Combinatorial CNF SAT Encodings?

问题描述

我正在通过使用

（使用本土工具， bc2cnf ， bool2cnf 或 Limboole ）

解决 CNF

（使用SAT解析器，如 Cryptominisat ， Plingeling ，表带或 Z3 ）

将解决方案（假设SAT结果）转换回问题域

这在我的小样本的情况。但是对于更具挑战性的问题，SAT解决者需要几个小时甚至几天才能进入SAT / UNSAT结论。我尝试调整我的编码以获得解决方案。但是我把编码越多，我的编码实际上是正确的（即可满足性等效）就越不确定。

布尔表达式的步骤对于可管理数量的条款和变量而言，CNF相当复杂，从而是有效的。等待SAT求解器的年龄是痛苦的，而不是确定时间花在正确的轨道上。

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

我的问题

编码是原始布尔表达式的有效表示？

从文献中，我已经知道了一些可以转换为变量赋值的问题的解决方案信任我的编码过程。但是由于 Tseitin编码，我的CNF中的大多数变量是辅助（切换）变量。没有 Tseitin编码，我的CNF将无法解决。因此，我不能简单地检查每个CNF条款是否由已知解决方案实现。

我试图使用 cnf2aig ，但该工具还处于起步阶段。没有切换变量，可以直观地检查对主要问题变量的布尔表达式的分类。

有几个关于CNF到电路方法的出版物，但是它们都没有提供可用的工具。

有没有最佳实践来完成这样的检查？

解决方案

所以你问的是：

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

或换句话说：

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

我的解决方案如下：

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




2. 使用Tseitin从C和DIe为！B生成CNF将C的CNF解释为总和（分离的结合）的乘积，并反转整个表达式。让我们把所得到的CNFs C'作为D的倒数与C的倒数相乘。

   
   
   

   所以满足C的模型不会满足C'，反之亦然。类似于D和D'。




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




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




5. 如果步骤3.和4.两者都不产生模型（不满足），那么你已经证明B和C是等同的。 p>

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

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

我希望有所帮助。你已经说过你正在努力确保你的优化是正确的，所以你应该有一个很好的实现。否则你可以使用我写的外部参考资料库：

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

CNF这个图书馆生成的效果不是很好！但是经过很好的测试..

I am trying to solve a combinatorial problem by using a SAT Solver.

This involves the following steps:

1. Encode the problem as set of boolean expressions.
2. Translate a conjunction of the expressions into CNF/DIMACS
   (using home grown tools, bc2cnf, bool2cnf or Limboole)
3. Solve the CNF
   (using SAT Solvers like Cryptominisat, Plingeling, Clasp or Z3)
4. Translate the solution (assuming a "SAT" result) back into the problem domain

This works in my case for small samples. But for more challenging ones, the SAT solver takes hours or even days without coming to a SAT/UNSAT conclusion. I try to tune my encoding to arrive at a solution. But the more effort I put in my encoding, the less certain I can be that my encoding is actually correct (i.e. "satisfiability equivalent").

The step from boolean expression to CNF is rather convoluted to be efficient in terms of a managable number of clauses and variables. It is painful to wait ages for the SAT solver and not be sure that the time is spent on the right track.

The boolean expression might be wrong. Therefore, I'd like to validate that the CNF actually represents the original problem not just the boolean expression.

My Question:

How could I verify that a given encoding is a valid representation of the original boolean expression?

From the literature, I have known solutions for some problems which I could translate into variable assignments to gain trust in my encoding process. But due to Tseitin encoding, most of the variables in my CNF are auxiliary (switching) variables. Without Tseitin encoding, my CNF would be far too big to be solvable. I therefore cannot simply check if every CNF clause is fulfilled by the known solution.

I have tried to translate the CNF back into boolean expressions using cnf2aig, but the tool is still in its infancy. Without switching variables, it is straightforward to check an assigment against boolean expressions of the primary problem variables.

There are a couple of publications about "CNF to circuit" approaches, but none of them provides a usable tool.

Is there any best practice to accomplish such a check?

解决方案

So what you are asking is:

Given a boolean expression B and a CNF C, is there a way to tell if they are equisatisfiable?

Or in other words:

Exists a model that satisfies B but not C, or that satisfies C but not B? If no such model exists then both are equisatisfiable.

My solution to that problem would be the following:

1. I'd use a known-good software (e.g. your unoptimized code or a third party tool) to generate a known-good CNF D from the boolean expression.

2. Use Tseitin to generate CNF for !B from C and D. I.e. interpret the CNF for C as a product of sums (conjunction of disjunction) and invert the whole expression. Lets call the resulting CNFs C' for the inverse of C and D' for the inverse of D.

   So a model that satisfies C would not satisfy C' and vice versa. Similar for D and D'.

3. Use a SAT solver to find a model that satisfies C and D'. Such a model would satisfy C but not B.

4. Use a SAT solver to find a model that satisfies C' and D. Such a model would satisfy B but not C.

5. If steps 3. and 4. both do not yield a model (unsat) then you have proven that B and C are equisatisfiable.

Steps 3. and 4. are easy. Just create one big CNF that contains all clauses from the two CNFs. All variables from B must be encoded with the same literal in both CNFs and the auxilary variables must be allocated from separate pools.

Depending on your problem, the solving steps 3. and 4. might be computationally quite expensive. So this approach might only be feasible if you can split up your problem into smaller chunks that can be verified independent from each other.

I hope that helps. You have said you are trying to make sure your optimizations are correct, so you should have a known-good implementation. Otherwise you could use a library I have written as an external reference:

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

The CNF generated by this library is not very efficient! But it is well tested..

这篇关于验证组合CNF SAT编码？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！