如何解决求解Horn公式的贪婪算法
这是我几天来一直试图理解并最终解决的作业问题。到目前为止，我还没有成功。因此，感谢您提供任何指导，帮助您理解或解决问题。
您在
m个布尔变量上获得了一组n约束 {x 1 ，x 2 ，...，x n }。约束有两种类型：
，x i ！= x j
等式约束：x i = x j ，对于某些i != j
不等式约束：对于某些i != j设计一个有效的贪婪算法， 一组平等和不平等约束条件确定是否 是否可能同时满足所有约束。
如果它 有可能满足所有约束，您的算法应该 输出满足所有条件的变量的赋值 约束。
到目前为止，我发现这个问题与布尔可满足性（SAT）问题有关。我尝试过先将所有变量设置为false，然后通过反例证明它不能一次满足所有约束。
我对约束满意问题（CSP）和 Horn SAT感到困惑。我阅读了有关这些问题的某些文章以获得解决方案，这使我感到困惑。我的逻辑是创建一棵树并应用DFS检查是否满足约束条件，而Horn SAT解决方案使我获得了数学证明。
任何帮助都值得赞赏，因为这是我的学习阶段，我无法一次掌握所有知识。 ：）
解决方法
（非正式）分类：
首先，这不是布尔SAT问题，因为这是NP完全的。您的老师通过请求有效的方法（即最多是多项式时间）来 始终 解决问题，从而暗示这不是NP完全的。
建模（思考）问题：
解决这个问题的一种方法是使用图形，其中不等式代表一种边，而等式代表另一种边：
以图形方式思考此问题使我意识到，这有点像图形着色问题：我们可以将所有节点设置为?（未设置），然后选择任何节点设置为true，然后从该节点进行广度优先搜索以设置所有连接节点（将它们设置为true或false），并检查是否存在任何矛盾。如果我们为图的连接组件完成此操作而没有发现矛盾，那么我们可以忽略该部分中的所有节点并随机设置另一个节点的值，依此类推。如果执行此操作，直到不剩下任何连接组件，并且仍然没有矛盾，那么我们以代表合法解决方案的方式来设置图表。
解决方案：
由于确切存在n个元素，我们可以为equalities创建一个关联的“存储桶”数组，并为inequalities创建一个关联的数组（每个“ bucket”可以包含一个数组）等于，但是如果我们想要[复杂度保持不变]，我们甚至可以得到比这更高的效率。
您可以想象equalities的数组数组：
这将表示：
0 == 1
1 == 2
3 == 4
请注意，这是一个不规则矩阵，需要2*m空间。我们对inequality矩阵执行相同的操作。此外，设置这两个数组（的数组）会占用O(m + n)的空间和时间复杂度。
现在，如果存在解，{x 0 ，x 1 ，x 2 ，x 3 }，则{！x 0 、! x 1 、! x 2 、! x 3 }为也是解决方案。证明：
（x i == x j ）iff（！x i ==！x j ）
因此，如果我们随机设置元素之一，则不会影响我们的解决方案。让我们将x i 设置为true，将其他设置为? [在数字上，我们将处理三个值：0（false），{{ 1}}（真）和1（未设置）]。
我们将这个数组称为2（即使尚未完成）。
现在，我们可以使用递归来考虑设置值的所有后果：
（下面的代码是伪代码，因为发问者没有指定语言。我将其设置为solution风格，但只是为了使其通用并使用漂亮的格式设置颜色。 ）
c++由于bool Set (int i,bool val) // i is the index
{
if (solution[i] != '?')
return (solution[i] == val);
solution[i] == val;
for (int j = 0; j < equalities[i].size(); j += 1)
{
bool success = Set(equalities[i][j],val);
if (!success)
return false; // Contradiction found
}
for (int j = 0; j < inequalities[i].size(); j += 1)
{
bool success = Set(inequalities[i][j],!val);
if (!success)
return false; // Contradiction found
}
return true; // No contradiction found
}
void Solve ()
{
for (int i = 0; i < solution.size(); i += 1)
solution[i] == '?';
for (int i = 0; i < solution.size(); i += 1)
{
if (solution[i] != '?')
continue; // value has already been set/checked
bool success = Set(i,true);
if (!success)
{
print "No solution";
return;
}
]
print "At least one solution exists. Here is a solution:";
print solution;
}
函数中的第一个if条件，该函数只能执行Set次（在if语句之外）。 n函数只能在传递第一个Set语句时进行调用，该语句执行if次，每个节点值1次。每当n函数进入函数主体时（在Set语句之后），它所做的工作与与相应节点关联的边数成正比。 if函数最多可以Solve次调用Set函数。因此，该函数可以调用的次数为n，对应于求解过程中完成的工作量。
这里的一个技巧是认识到O(m+n)函数将需要调用Solve函数Set次，其中C是图形的已连接组件数。请注意，每个连接的组件彼此独立，因此适用相同的规则：我们可以合理地选择其元素之一的值，然后考虑后果。
最快的解决方案仍然需要读取所有约束C，并在可能的情况下需要输出解决方案O(m)；因此，不可能获得比O(n)更好的时间复杂度的解决方案。上面是具有O(m+n)时间和空间复杂度的贪婪算法。
有可能获得更好的空间复杂度（同时保持O(m+n)时间复杂度），甚至可能是O(m+n)，但我不确定。
关于霍恩公式，我很尴尬地承认我对它们一无所知，但是这个答案直接回答了作业中对您的要求。
,让我们以约束x1 = x2和x2！= x3的示例110
请记住，因为我们仅获得了约束，所以算法也可以同时满足约束，最终生成001作为输出
一种解决方法是
有两个列表，每个约束类型一个，
每个列表包含一对i，j索引。
根据i索引对列表进行排序。
现在，在等式约束中每对均检查不等式中是否没有与其冲突的约束。
如果这样做，那么您可以立即退出
否则，您必须检查相等约束列表中是否有更多对具有其中之一。
然后您可以为其分配一个或零，最终您将能够生成完整的输出
版权声明：本文内容由互联网用户自发贡献，该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容， 请发送邮件至 dio@foxmail.com 举报，一经查实，本站将立刻删除。
