2023/05/22 by Ananth Hari, Uzi Vishkin, Hari, Ananth +1
Computer Science · #Distributed #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Natural Language Processing Techniques #Parallel #and Cluster Computing (cs.DC)
paper · pdf · doi:10.48550/arxiv.2305.13539
openalex publication_date 2023/05/22 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.