算法:如何找到SAT的解决方案的数量

Question

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

我读到SAT与独立集有关。

Answer 1

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

一个包含N变量的子句只排除其中一个minterm作为解决方案的一部分。这是由子句的所有反转变量组成的minterm。

假设K子句都不同，

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

---

示例：

具有N=3变量的K=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个解决方案。