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.

翻译：我们提出图回溯（graph backtracking）——一种面向基于CDCL的SAT求解的细粒度回溯方案，该方案由用户自定义的权重函数参数化。在冲突修复过程中，我们摒弃决策层抽象，转而将蕴含图作为精确的引导结构，以最小化未赋值文字的权重。图回溯方法是可靠且完备的。通过用特定权重函数模拟时序回溯与非时序回溯，我们证明该方法是对二者的泛化。本文在实验性求解器NapSAT中实现了该方案。实验结果表明，相比标准方法，图回溯所需的文字传播次数更少，从而提升了求解器的运行效率。