Clause connectivity and isolated solutions: a structural heuristic for SAT variable ordering
Subhas Kumar Ghosh, Vijay Monic Vittamsetti · International Journal of Parallel Emergent and Distributed Systems · 2025
The performance of modern Conflict-Driven Clause Learning (CDCL) SAT solvers is dominated by dynamic, conflict-driven branching heuristics like VSIDS. While effective, these heuristics are largely agnostic to the global structure of the input formula. This paper explores a hybrid approach that marries global structural analysis with local, adaptive learning. We first introduce rigidity, an efficiently computable measure of clause interconnectedness, and prove a formal link between high-rigidity structures and the critical clauses that define isolated solutions. We use this theory to design a simple, static heuristic and, through a detailed trace-based analysis, reveal its fundamental limitations: a purely static approach is too brittle and can starve the solver's crucial conflict-learning engine. This insight motivates our main contribution: Adaptive Rigid-VSIDS (ARV), a hybrid heuristic that seeds VSIDS with rigidity scores and uses a novel, LBD-driven adaptive quota to dynamically balance between static structural guidance and dynamic conflict-driven search. We prove that this adaptive mechanism enjoys sub-linear regret, guaranteeing its robustness. Experimental evaluation shows that ARV is a robust enhancement, providing performance gains on a wide range of structured and random benchmarks compared to the baseline VSIDS.