2026-07-20T05:12:11Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:26320 2026-07-16T10:50:11Z ddc:004 open_access

Generalizing CDCL with Graph Backtracking Coutelier, Robin Hader, Thomas Kovács, Laura SAT Solving Backtracking Conflict Analysis CDCL 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, complete, and terminating. 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Robin Coutelier and Thomas Hader and Laura Kovács 2026 Is Part Of LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2026.14 urn:nbn:de:0030-drops-263203 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.14 eng https://creativecommons.org/licenses/by/4.0/legalcode