Accelerating SAT Solving via Differentiable Decision Heuristics

Boolean satisfiability (SAT) is a fundamental computational primitive underlying verification, planning, synthesis, and automated reasoning. Modern CDCL SAT solvers are highly optimized, but their initial branching and phase heuristics are still largely solver-internal defaults that do not explicitly adapt to the structure of each input formula. We introduce optimization-guided initialization framework that uses a GPU-accelerated model to extract formula-level guidance and warm-start key CDCL heuristics, including phase selection and variable activity. The resulting solver preserves the original CDCL search procedure and remains complete, making the method a drop-in enhancement rather than a replacement for state-of-the-art SAT solving. We evaluate on SAT Competition benchmarks and compare against strong competition solvers in both single-threaded and parallel settings. In the single-threaded setting, our best individual initialization achieves a PAR-2 speedup over Kissat with fallback, while the virtual best configuration reaches a PAR-2 speedup and improves 207 instances. Our variants rescue 9 Kissat timeouts, including both SAT and UNSAT formulas. In the parallel setting, a 32-thread phase portfolio achieves a PAR-2 speedup over MallobSat(32T), improves 107 of 167 SAT instances, and solves 15 of the 18 instances on which Kissat times out. These results show that optimization-guided initialization can provide practical, structure-aware diversification for both single-threaded CDCL search and parallel SAT portfolios.