Chronological vs. non-chronological backtracking in satisfiability modulo theories

Abstract

SMT solvers are a powerful tool used in many verification applications. They are designed to check the satisfiability of a logic formula in a given set of theories. The core of any SMT solvers is a fine-tuned SAT solver enhanced with more expressive theory reasoners. Recently, SAT solvers have seen a new paradigm emerge with the introduction of Chronological Backtracking. This new approach has already shown some improvements on state-of-the-art standalone SAT solvers. In the following, we detail the functioning of CDCL solvers and the assumptions that non-chronological backtracking enables. After that, we study what it takes to convert a standard SAT solver to support chronological backtracking. We discuss both necessary and optional changes to the solver and present algorithms for each of them. We implement these changes on the SAT solver of veriT, an SMT solver written in C. Finally, we consider some details when adapting the SMT solver to support chronological backtracking. We present ideas for future work and discuss the potential benefits of this new approach.