  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.
