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的并行算法，在几乎所有实例上的平均深度为多对数级别，同时保持线性工作量。这一结果挑战理论家与程序员超越最坏情况分析，提出兼具实用性与性能保证的算法。