Horn-satisfiability or Horn-SAT is the problem of deciding whether a satisfying assignment exists for a Horn formula, a conjunction of clauses each with at most one positive literal (also known as Horn clauses). It is a well-known P-complete problem, which implies that unless P = NC, it is a hard problem to parallelize. In this paper, we empirically show that, under a known simple random model for generating the Horn formula, the ratio of hard-to-parallelize instances (closer to the worst-case behavior) is infinitesimally small. We show that the depth of a parallel algorithm for Horn-SAT is polylogarithmic on average, for almost all instances, while keeping the work linear. This challenges theoreticians and programmers to look beyond worst-case analysis and come up with practical algorithms coupled with respective performance guarantees.

翻译：Horn可满足性（Horn-SAT）是判断是否存在满足赋值的Horn公式（每个子句至多包含一个正文字的子句合取，亦称为Horn子句）的决策问题。这是一个著名的P完全问题，这意味着除非P = NC，否则它难以并行化。本文通过实验证明：在一种已知的简单随机模型生成的Horn公式中，难并行化实例（接近最坏情况行为）的比例极小。我们证明，对于几乎所有实例，Horn-SAT并行算法的深度平均为多对数级，同时保持线性工作量。这一结论挑战理论家和程序员超越最坏情况分析，提出兼具性能保证的实用算法。