SAT/CNF优化

Question

问题

我正在研究SAT优化问题的一个特殊子集.对于那些不熟悉SAT和相关主题的人,这里是相关的维基百科文章.

TRUE=(a OR b OR c OR d) AND (a OR f) AND ...

没有NOTs,它是联合正常形式.这很容易解决.但是,我正在尝试最小化真正的赋值数,以使整个语句成立.我找不到解决这个问题的方法.

可能的解决方案

我提出了以下解决方法:

1. 转换为有向图并搜索最小生成树,仅跨越顶点子集.有Edmond的算法,但它给出了完整图形的MST而不是顶点的子集.
   • 也许有一个版本的Edmond算法可以解决顶点子集的问题？
   • 也许有一种方法可以用原始问题构建一个可以用其他算法解决的图形？
2. 使用SAT求解器,LIP求解器或穷举搜索.我对这些解决方案不感兴趣,因为我正在尝试将此问题用作讲义材料.

题

你有什么想法/意见吗？你能想出其他可行的方法吗？

Answer 1

这个问题也是NP-Hard.

人们可以从击球组中看到东部减少:

碰集问题:给定套S1,S2,...,Sn和一批k:选择了设定S的大小k,这样,每Si有一个元素s中S,使得s在Si.[备选定义:每个之间的交叉Si和S不为空.

减少:
对于一个(S1,...,Sn,k)命中集的实例,构造你的问题的实例:所有元素在(S'1 AND S'2 And ... S'n,k)哪里,用OR.S'i中的这些元素是公式中的变量.S'iSi

证明:
碰集- >这样的问题:如果有设置,hittins的一个实例,S然后通过把所有S的与真实的元素,计算公式是满意k的元素,因为对于每一个S'i有一些变量v是在S和Si,因此也在S'i.
这个问题 - >命中集:S使用所有分配为真的元素构建[ 与命中集相同的想法 - >这个问题].

既然你正在为此寻找优化问题,它也是NP-Hard,如果你正在寻找一个精确的解决方案 - 你应该尝试指数算法