布尔公式编码 [英] Boolean formula encoding

问题描述

我想知道对

@(x1,x2,x3,x4) = (x1 OR x2 OR NOT(x3) OR x4) AND ((NOT)x2 OR x3) AND (x1 OR (NOT)x4)  

@是SAT的一个实例.我认为这是4位，因为可能的组合总数为2(power4).那是对的吗?我应该计算OR，NOT和AND来计算编码所需的位数吗?我搜索了很多，但找不到任何东西.

@ is an instance of SAT. I think it is 4 bits since total number of possible combinations are 2(power4). Is that correct? Should i count OR, NOT, AND to calculate number of bits needed for encoding? I searched a lot but couldn't find anything on this.

推荐答案

您始终可以在保留变量数的情况下将表达式转换为逻辑上等效的CNF.但是，在最坏的情况下，这会产生指数数量的子句，这对于大多数应用程序至少不切实际;-).因此，通常在SAT中使用其他编码，这些编码使用较少(多项式数)从句，但增加了(多项式)变量.通常使用 Tseitin转换来生成此编码.

You can always convert your expression into a logically equivalent CNF with preserving the number of variables. However, in the worst case this yields an exponential number of clauses, which is at least impractical for most applications ;-). Therefore usually other encodings are used in SAT that use fewer (polynomial number of) clauses but adds a (polynomial) number of variables. Usually a Tseitin Transformation is used to generate this encoding.

请注意，变量的数量并不一定是编码效果的量度.在某些情况下，可以通过添加冗余子句之类的技巧极大地加快SAT的速度.因此，当您想生成有效的编码时，应该查看CNF的结构，而不是变量或子句的数量.

Note that the number of variables is not necessarily a measure of how effective an encoding is. In some situations SAT can be sped up immensely by tricks like adding redundant clauses. So when you want to generate an effective encoding, you should look at the structure of your CNF rather than the number of variables or clauses.

Magnus Bjiirk于2009年7月25日发表的一篇不错的论文，其中包含很多有关SAT编码的有用参考，这是一篇很好的文章: http://jsat.ewi.tudelft.nl/addendum/Bjork_encoding.pdf

A nice paper that contains a lot of useful references to work regarding SAT encoding is "Successful SAT Encoding Techniques" by Magnus Bjiirk, 25th July 2009: http://jsat.ewi.tudelft.nl/addendum/Bjork_encoding.pdf‎

这篇关于布尔公式编码的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！