Generalizing CDCL with Graph Backtracking
For SAT solver developers, this provides a flexible backtracking framework that can outperform standard chronological and non-chronological methods.
Graph backtracking generalizes CDCL backtracking by using the implication graph to minimize literal unassignment weight, reducing literal propagations and improving solver runtime in the NapSAT implementation.
We present graph backtracking, a novel, fine-grained backtracking scheme for CDCL-based SAT solving, parametrized by a user-defined weight function. For conflict repair, we challenge the decision level abstraction and use the implication graph as a precise guiding structure to minimize the weight of literals that are unassigned. Graph backtracking is sound and complete. We show that it is a generalization of chronological and non-chronological backtracking by simulating them with specific weight functions. Our approach is implemented in the experimental solver NapSAT. Empirical results show that graph backtracking requires fewer literal propagations than standard approaches, leading to improved solver runtime.