Abstract
Over the past thirty years, SAT solvers have become increasingly efficient, capable of solving industrial benchmarks with millions of variables. However, they still struggle with specific classes of benchmarks containing only hundreds of variables, leaving researchers searching for ways to uncover their inner workings. In this talk, we introduce an approach that uses causal reasoning to gain insights into the functioning of modern SAT solvers.
Our framework, CausalSAT, generates observational data from the execution of SAT solvers and learns a structured graph representing the causal relationships among the components of a SAT solver. By using CausalSAT to quantitatively verify hypotheses previously regarded as rules of thumb or empirical findings, we can gain a deeper understanding of how modern SAT solvers work. For example, CausalSAT can determine whether a clause with low glue has a higher clause utility, or whether clauses with high glue experience a rapid drop in utility over time.
CausalSAT can also address previously unexplored questions, such as which branching heuristic leads to greater clause utility. Experimental evaluations using practical benchmarks demonstrate that CausalSAT is effective in fitting the data, verifying four rules of thumb, and providing answers to three questions closely related to implementing modern solvers. Through this approach, we hope to shed light on the inner workings of SAT solvers and help improve their efficiency and effectiveness.