Trail Saving in SMT

Abstract

In this paper we discuss and evaluate the method of trail saving on backjumps in CDCL(T)-based SMT solvers. The method was originally proposed for CDCL-based SAT solvers at the SAT conference in 2020, showing a positive impact on solving SAT instances. Since a SAT solver tends to follow a similar path down the search tree after a backjump, saving the retracted portion of the trail enables speeding up the inference after the backjump by copying the saved inferred literals to the assertion trail, instead of re-propagating them by the unit-propagation mechanism. A similar behaviour may be expected when SMT solvers are concerned, but since the process of theory propagation within SMT solvers is usually even more expensive, the trail saving technique may potentially have even more significant impact in case of SMT instances. Although the experimental evaluation given in this paper shows some potential of the approach, the obtained results are generally mixed, and depend greatly on the chosen benchmark family, even within the same theory. Further analysis might be needed in order to better understand the behaviour of the method and its effects on the entire solving process.