Measuring Per-Decision Propagation Work as a Formula-Dependent Signal
TL;DR
Hardware accelerators for Boolean satisfiability (SAT) target the solver's inner loop, Boolean constraint propagation (BCP), where PR is a trace statistic of little use to a software solver, but under hardware acceleration it determines whether a formula carries enough work per offload to justify sending it at all.
Abstract
Hardware accelerators for Boolean satisfiability (SAT) target the solver's inner loop, Boolean constraint propagation (BCP). Every offload carries a fixed overhead, so what decides whether acceleration pays is the work delivered per invocation. For a conflict-driven clause-learning (CDCL) solver the natural unit of that work is the propagation rate (PR): propagations per decision. Across seven SATLIB families and 5,199 instances, PR varies roughly fivefold, and is captured neither by the clause-to-variable ratio, the standard predictor of SAT hardness, nor by formula size alone: families matched on size still differ more than twofold. On 210 industrial instances it spans two orders of magnitude across application domains, and within five of them it can be estimated before solving, from the formula's community structure alone. PR is a trace statistic of little use to a software solver; it does not change how the solver runs, but under hardware acceleration it determines whether a formula carries enough work per offload to justify sending it at all.