SAT/CNF 优化
问题
我正在研究 SAT 优化问题的一个特殊子集。对于那些不熟悉 SAT 和相关主题的人，请参阅以下相关维基百科文章。
TRUE=(a OR b OR c OR d) AND (a OR f) AND ...
没有 NOT，它是合取范式。这很容易解决。不过，我正在尝试最大限度地减少真实分配的数量以使整个陈述成立。我找不到解决该问题的方法。
可能的解决方案
我想出了以下方法来解决它：
- 转换为有向图并搜索最小生成树，仅跨越顶点的子集。有 Edmond 算法，但它给出的是完整图的 MST，而不是顶点的子集。
- 也许 Edmond 算法的某个版本可以解决顶点子集的问题？
- 也许有一种方法可以根据原始问题构建一个可以用其他算法解决的图表？
- 使用 SAT 求解器、LIP 求解器或穷举搜索。我对这些解决方案不感兴趣，因为我试图使用这个问题作为讲座材料。
问题
您有什么想法/意见吗？您能想出其他可行的方法吗？
Problem
I'm looking at a special subset of SAT optimization problem. For those not familiar with SAT and related topics, here's the related Wikipedia article.
TRUE=(a OR b OR c OR d) AND (a OR f) AND ...
There are no NOTs and it's in conjunctive normal form. This is easily solvable. However I'm trying to minimize the number of true assignments to make the whole statement true. I couldn't find a way to solve that problem.
Possible solutions
I came up with the following ways to solve it:
- Convert to a directed graph and search the minimum spanning tree, spanning only a subset of vertices. There's Edmond's algorithm but that gives a MST for the complete graph instead of a subset of the vertices.
- Maybe there's a version of Edmond's algorithm that solves the problem for a subset of the vertices?
- Maybe there's a way to construct a graph out of the original problem that's solvable with other algorithms?
- Use a SAT solver, a LIP solver or exhaustive search. I'm not interested in those solutions as I'm trying to use this problem as lecture material.
Question
Do you have any ideas/comments? Can you come up with other approaches that might work?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
这个问题也是NP-Hard。
人们可以从击球组显示东减少：
击球组问题：给定组< code>S1,S2,...,Sn 和数字
k：选择大小为k的集合S，这样对于每个Si那里是S中的元素s，使得s位于Si中。 [替代定义：每个Si和S之间的交集不为空]。减少：
对于命中集的实例
(S1,...,Sn,k)，构建问题的实例：(S'1 AND S'2 And ... S'n,k)，其中S'i是Si中的所有元素，使用 OR。 S'i 中的这些元素是公式中的变量。证明：
击球设置 ->这个问题：如果有一个hitins集合的实例，
S，那么通过将S的所有元素赋值为true，公式满足>k个元素，因为对于每个S'i都有一些变量v位于S和Si< /code> ，因此也在
S'i中。这个问题-> Hitting set：用所有赋值为真的元素构建
S[与Hitting Set相同的想法->这个问题]。由于您正在寻找为此的优化问题，因此它也是 NP-Hard，如果您正在寻找精确的解决方案 - 您应该尝试指数算法
This problem is NP-Hard as well.
One can show an east reduction from Hitting Set:
Hitting Set problem: Given sets
S1,S2,...,Snand a numberk: chose setSof sizek, such that for everySithere is an elementsinSsuch thatsis inSi. [alternative definition: the intersection between eachSiandSis not empty].Reduction:
for an instance
(S1,...,Sn,k)of hitting set, construct the instance of your problem:(S'1 AND S'2 And ... S'n,k)whereS'iis all elements inSi, with OR. These elements in S'i are variables in the formula.proof:
Hitting Set -> This problem: If there is an instance of hittins set,
Sthen by assigning all ofS's elements with true, the formula is satisfied withkelements, since for everyS'ithere is some variablevwhich is inSandSiand thus also inS'i.This problem -> Hitting set: build
Swith all elements whom assigment is true [same idea as Hitting Set->This problem].Since you are looking for the optimization problem for this, it is also NP-Hard, and if you are looking for an exact solution - you should try an exponential algorithm