Measuring Per-Decision Propagation Work as a Formula-Dependent Signal
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 tha...