减少0-1背包问题.SAT问题的答案

Question

是否有办法将0-1背包问题化为合范数形式的SAT问题?

Answer 1

您总是可以计算出实现加法器和比较器所需的数字电路，然后将其结果转换为合取范式。你可以把电路变成CNF形式，而不需要把它们指数地展开，方法是用中间变量来表示一小段电路的输出。

电路的每个节点等于a=f(b, c)，其中a为输出，b和c为输入，f为简单函数，如&或|。您可以创建一个只有当a确实是f(b, c)的结果时才为真的CNF函数，而且它不能太笨拙，因为它是一个只有三个变量的函数。

你可以将任何电路改写成大量形式为a=f(b, c)的项，你所要做的就是用它们的CNF版本把它们都放在一起。假设您想求解输出是否为真，那么您只需将输出变量作为大与的最终组成部分。