algorithm - 算法：如何找到 SAT 的解数？

Question

假设变量数 N 和子句数 K 相等。找到一种算法，该算法返回满足子句的不同方式的数量。

我读到SAT与独立集有关。

Answer 1

N带变量的函数有一个带行的真值表。2^N每一行对应一个最小项，它可以是解决方案，也可以不是解决方案。

带有N变量的子句恰好排除了其中一个作为解决方案的一部分的最小项。那是由子句的所有倒置变量组成的最小术语。

只要K条款都不同，

解决方案的数量是 2^N - K

---

例子：

带变量的K=3子句：N=3

 A or  B or  C
!A or  B or  C
 A or  B or !C

三个输入的真值表：

A  B  C  output
0  0  0  0         //  excluded by A or B or C
0  0  1  0         //  excluded by A or B or !C
0  1  0  1
0  1  1  1
1  0  0  0         //  excluded by !A or B or C     
1  0  1  1
1  1  0  1
1  1  1  1

可能的八个术语中有五个仍然正确。因此，该示例有 2^3 - 3 = 5 个解决方案。