姜咏江

逻辑电路基本上都是与、或、非门电路搭建起来的。电路运行中如何检测每个器件的好坏？实际上可以通过SAT表达式求出的解来进行验证。我这里举一个维基百科上的实际例子来说明这个问题的解决办法。

在https://en.wikipedia.org/wiki/Tseytin_transformation网页可以找到图1这个逻辑电路。它通过Tseytin变换可以得到下面的SAT-CNF。

图1   逻辑电路

SAT-CNF=(g₁+x₁)(g₁’+x₁’)(g₂’+g₁)(g₂’+x₂)(x₂’+g₂+g₁’)(g₃+x₂)(g₃’+x₂’)(g₄’+x₁)(g₄’+g₃)(g₃’+g₄+x₁’)(g₅+x₂)(g₅’+x₂’)(g₆’+g₅)(g₆’+x₃)(x₃’+g₆+g₅’)(g₇+g₂’)(g₇+g₄’)(g₂+g₇’+g₄)(g₈+g₆’)(g₈+g₇’)(g₆+g₈’+g₇).  

用1表示变量文字x，用0表示变量文字x’，那么这个SAT-CNF就可以用表1表示出来。不仅如此，我们可以利用子句标志消去法，求出g点随着x端输入的变化应该出现的正确值。变量x和g的那些值是SAT 的满足解，就说明电路器件完好，整个电路合格。由于集成电路基本门电路数量庞大，人工检测基本上是不可能的。用自动检测设备进行，就要求出SAT-CNF=1 的满足解，也许需要求出全部解。自动检测设备的核心就是计算机。用计算机求SAT解，就是著名的世界公开难题.

表1  SAT-CNF 的二进制表示

在我的博文http://blog.sciencenet.cn/blog-340399-1009397.html有一个验证小程序，可以让你方便地求出这个SAT-CNF=1的全部解。

如果手工操作也很容易，只要你先备一个11位二进制表，然后对照表1，删去那些包含表1子句的那些二进制数，并将最后剩下的那些二进制数求反码，得到的都是这个SAT-CNF=1的解。

这个例子的全部解为：

10100111111

10000111011

01111000011

01011000011

00110101101

不信，你就自己验证一下吧。