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 efects on the entire solving process.
SAT and SMT solvers have become indispensable tools in the previous two decades, with
applications spanning from hardware and software verification [
New applications pose new challenges to SAT and SMT solvers, and there is a constant
pressure to make SAT and SMT technology even more eficient and robust. Therefore, new
implementational and algorithmic enhancements of the existing procedures used in SAT and
SMT solvers have become a very popular research direction. One such improvement in the area
of SAT solving was presented by Hickey and Bacchus [
The main goal of this work is to evaluate the potential of using the described technique within
SMT solvers. The process of theory propagation [
The rest of the paper is organized as follows. In Section 2 we present the basic concepts and
notions needed in the rest of the text. In Section 3 we describe the basic trail saving method, as
presented in [
In this paper we assume the standard syntax and semantics of the first order logic with equality,
adopting the terminology from [
We follow the usual approach for solving SMT problems, based on the CDCL(T)1 scheme
[
The notation used in the following text is mostly borrowed from [
When a CDCL-based SAT solver is coupled with a theory solver for some first order theory T, a conflict may also arise if the theory solver deduces that a subset of literals from is T-unsatisfiable. Such a conflict is called a theory conflict (or T-conflict), and is a T-conflict reason which is used as a starting point for conflict analysis. The theory solver may also T-infer literals (i.e. discover literals of that are T-consequence of some subsets of literals from ). These literals are pushed on (the process known as theory propagation). If a literal is T-inferred from the set ⊆ , then is called (T-propagation) reason of . It is again denoted by () and may be used during the conflict analysis in the future.
A formula is unsatisfiable if a conflict (propositional or T-conflict) happens when = 0, and is satisfiable if all literals of have assigned values, none of the clauses are falsified and there is no T-conflict detected by the theory solver.
In this section we discuss the basic trail saving algorithm [
In order to preserve the correctness of the CDCL algorithm, the property of reason soundness
[
In the basic variant of the trail saving algorithm [
The basic functions of the trail saving algorithm [
Saving the trail. The function SaveTrail is invoked by the solver immediately before a backjump to the level is performed. It first checks whether the prepending of the newly saved portion of the trail to may spoil the reason soundness of . As we will discuss later in more detail, this may happen only when a new conflict occurs immediately after a backjump, while we are still at the level . Therefore, in such cases we must clear before [[ + 1 . . . − 1]] is prepended, in order to stay on the safe side. For this reason, we keep track of the decision level of the previous backjump as , and reset the saved trail if = . After that, [[ + 1 . . . − 1]] is prepended to . The function SaveTrail also saves the reasons of the saved literals. The variable represents the position of the next-to-process literal in the list . This variable is reset at the end of the function SaveTrail.
Example 1. Assume that we have, among others, the following set of clauses: {¬16, ¬15, ¬5}, {9, ¬2, 8}, {¬13, 8, 10}, {19, 3, 20}, {11, ¬1, 10}, {16, ¬6, ¬15}, {14, 8, 15}, {¬12, ¬2, 10}, {¬17, ¬18}, {¬8, ¬7}, {¬20, 7}, {¬22, ¬23}, {¬22, ¬24}, {22, ¬25}, {23, 24, ¬1}, {¬4, ¬19, ¬21}, {19, 8, ¬9}, {¬1, 22, 25}. Assume that after the first several decisions the following state of the trail is reached:
= 0 1 2 ¬3 ¬4 5 6 7 ¬8 9 ¬10 11 ¬12 ¬13 ¬14 15 16 Note that the literals labelled with in the exponent are the decision literals, so the current decision level is = 7. At that moment, a conflict is encountered with the clause {¬16, ¬15, ¬5}. If the reason of ¬16 is the clause {16, ¬6, ¬15}, the conflict analysis gives us the backjump clause {¬15, ¬5, ¬6}, and the backjump level = 4. Before the backjump, the portion of the trail consisting of the levels 5 and 6 is saved, so after the backjump, we have the following state: = 0 1 2 ¬3 ¬4 5 6 ¬15 = 7 ¬8 9 ¬10 11 ¬12 ¬13 Algorithm 1 Trail saving algorithm else if |= then
← + 1 else if |= ¬ then
return () ← + ; () ← + 1 () ◁ Case when concatenation may spoil reason-soundness
◁ Remember the backjump level ◁ Conflicting level is dropped
◁ Saving reasons ◁ For each unprocessed literal ◁ Passing saved literal that is true on ◁ Decisions are not inferred by ◁ Saved decision literal ◁ Saved inferred literal ◁ Passing saved literal that is true on
◁ Conflict found on ◁ Push saved inferred literal to ◁ Confirming changes
◁ Filtered version of
◁ Non-duplicates are preserved in
◁ Cut the portion of after the first conflicting literal
The reasons of saved inferred literals are also saved. For instance, we have (9) =
{9, ¬2, 8}, (¬8) = {¬8, ¬7}, (11) = {11, ¬1, 10}, and
finally, (¬13) = {¬13, 8, 10} (we will need these saved reasons in the later
examples).
Using the saved literals. The function UseSavedTrail uses the literals from the list
to speed up the inference. In the original algorithm [
Example 2. Continuing the previous example, assume that after the next two decides, the following state is reached: = 0 1 2 ¬3 ¬4 5 6 ¬15 17 ¬18 ¬19 20 7 ¬*8 *9 = 7 ¬8 9 ¬10 11 ¬12 ¬13 Note that the literal 7 is now inferred (from the clause {¬20, 7}), and the literals ¬8 and 9 are copied from , once 7 became true in (we mark such literals with * in the exponent). The next literal ¬10 cannot be copied from , since it is a saved decision literal undefined in , so it is not a consequence of at this moment. Note also that is not changed by the function UseSavedTrail, i.e. the literals 7, ¬8, 9 are still on .
SavedLiterals is invoked before each decision. Namely, as we have seen in the previous example, the literals from that are pushed to must remain on until the propagation process at that level is exhausted, in order to maintain the reason-soundness of (otherwise, in case of a conflict, the SaveTrail function would drop the conflicting topmost level, possibly spoiling the reason-soundness of the remaining literals in ). When we are assured that there is no conflict at the topmost level, we may safely drop the processed prefix of , just before the new decision is made.
Example 3. Continuing the previous example, recall that the literals 7, ¬8 and 9 are still on , since their transfer to is not confirmed yet. In the present state of the trail we again have a conflict, this time with the clause {19, 8, ¬9}. During the conflict analysis, we first resolve the literals 9 and ¬8 (using their saved reasons {9, ¬2, 8} and {¬8, ¬7}), reaching the clause {19, ¬2, ¬7}, and then resolve the literal 7 using its reason {7, ¬20} (the resolvent being the clause {19, ¬2, ¬20}), and the literal 20 using its reason {19, 3, 20}, ifnally obtaining the backjump clause {19, ¬2, 3}. The backjump level is now = 3, and the new state is: = = 0 1 2 ¬3 19
¬4 5 6 ¬15 17 ¬18 7 ¬8 9 ¬10 11 ¬12 ¬13 Note that the levels 4 and 5 from the trail were prepended to before the backjump. Note also why it is important to keep the used literals on until their transfer to is confirmed: since the conflicting level is never saved, if the literal ¬8 was not kept on when it was copied to , it would be lost after the backjump, and the literal ¬13 would stay on with an unsound saved reason {¬13, 8, 10}. Now assume that after the next two decides we have the following state: = 0 1 2 ¬3 19 21 ¬4 *5 *6 ¬*15 22 ¬23 ¬24 = 17 ¬18 7 ¬8 9 ¬10 11 ¬12 ¬13 Namely, after the decision 21, the literal ¬4 was inferred from the clause {¬4, ¬19, ¬21}, which once again unblocked the saved trail and the literals 5, 6 and ¬15 were copied from to . Just before the next decision 22, the copied literals from were confirmed on , i.e. they were removed from . Note that this is a safe operation – since these literals are now on the trail , but not at its topmost level, they will either be saved to or stay on after the next backjump, preserving the reason soundness of the literals on . The obtained state of is again conflicting, and this time the conflicting clause is {23, 24, ¬1}. After explaining ¬24 with the clause {¬22, ¬24}, and ¬23 with the clause {¬22, ¬23}, we obtain the backjump clause {¬1, ¬22}. The backjump level is now = 2, and we reach the following state: = 0 1 ¬22 = 2 ¬3 19 21 ¬4 5 6 ¬15 17 ¬18 7 ¬8 9 ¬10 11 ¬12 ¬13 Note that the literals ¬4, 5, 6, ¬15 that were confirmed on are now again on . Filtering the saved trail. Note that concatenation of saved portions of the trail may result in duplicates in . As a consequence, the list may grow indefinitely. Moreover, conlficting literals and ¬ may appear on , so the portion of after the two conflicting literals may be unreachable and, therefore, useless. For this reason, we should periodically iflter the list , by removing the duplicates and all the literals after the first conflicting literal in . This is done by the function FilterSavedTrail. Note that the first conflicting literal ¬ is kept on , since it may help in discovering a conflict. The procedure FilterSavedTrail is invoked whenever the length of becomes greater than the total number of atoms of the formula .
Preserving the reason soundness. It can be argued that the CDCL algorithm enhanced with
the trail saving mechanism remains correct, provided that the reason soundness of is
maintained during the operation of the solver. For the proof of this fact, we refer the interested
reader to the original work of Hickey and Bacchus [
Example 4. In the state from the previous example, the clause {¬1, 22, 25} triggers the unit propagation of the literal 25, which makes the trail in conflict with the clause {22, ¬25}. We first resolve the literal 25 with its reason, and obtain the clause {22, ¬1}, and then resolve the literal ¬22 with its reason {¬1, ¬22}, and obtain the backjump clause {¬1}. The backjump level = 0 this time, so after the backjump we reach the following state: = ¬1 = 0 Note that the previous state of was cleared before the new portion of (the literal 0) was prepended to it. This is because the conflict happened immediately after the backjump, before the next decide. In such a situation, the literals 1 and ¬22 from the conflicting level were neither saved, nor they were kept on , which might compromise the reason soundness of some literals on . For instance, recall that the saved reason of the literal 11 was {11, ¬1, 10}, and this reason is no longer sound, so the concatenation of the saved portions of the trail is not possible.
The described trail saving technique may be naturally extended to be used in the context of CDCL(T)-based SMT solvers, since such solvers are driven by a CDCL SAT solving engine. In this section, the CDCL(T) algorithm with the trail saving enabled is presented and discussed in detail. The overall structure of the CDCL(T) algorithm is not changed – the only thing that should be done to enable the trail saving is to invoke the trail saving functions described in the previous section at the appropriate places (which are mostly the same places as in the CDCL algorithm).
The main loop of the CDCL(T) algorithm. The main loop of the algorithm is implemented in the function Solve (Algorithm 2). It first invokes UnitPropagate and TheoryPropagate procedures to do the inference. These procedures check for unit/theory propagations and conflicts, and will be discussed later in more detail. If a conflict is encountered, a conflict reason is returned. In that case, the procedure Solve starts the conflict analysis, by invoking the AnalyzeConflict4 function which returns the backjump clause and the backjump level . Before backjumping to the level , the procedure first saves the part of the trail that will be retracted (by calling the function SaveTrail). Then it performs the backjump by restoring 3Note that there are cases when a conflict happens at , but the reason-soundness still holds after the concatenation of the saved trails. This means that the resetting of the saved trail each time a conflict is encountered at may be a quite conservative strategy. In our implementation, we try to recognize (some of) such cases in order to avoid unnecessary resets of . 4The pseudo-code of the function AnalyzeConflict is omitted (as well as of several other functions), in order to save space, since it does not invoke any of the trail saving functions. Algorithm 2 CDCL(T) algorithm with the trail saving enabled: Solve function 1: Solve( ) 2: while true do 3: while is changed do 4: ← UnitPropagate() 5: if ̸= ∅ then 6: break 7: ← TheoryPropagate() 8: if ̸= ∅ then 9: break 10: if ̸= ∅ then 11: if = 0 then 12: return UNSAT 13: (, ) ← AnalyzeConflict(, ) 14: SaveTrail() 15: ← [[0...]] 16: RestoreTheorySolverState() 17: ← 18: if || is greater than the total number of atoms in then 19: FilterSavedTrail() 20: ← ∪ {} 21: else 22: if all atoms from are assigned in then 23: return SAT 24: ConfirmPropagatedSavedLiterals() 25: ← PickBranchingVariable(, ) 26: ← + {}; () ← ∅ 27: ← + 1 ◁ Unit and theory propagation loop ◁ Returns a conflicting clause, or ∅ ◁ If a conflict is found, exit the propagation loop
◁ Returns a theory conflict reason, or ∅ ◁ If a conflict is found, exit the propagation loop ◁ A conflict is discovered during the propagation
◁ A conflict at the level 0 ◁ is the backjump clause ◁ Save the retracted portion of the trail ◁ Backjump the trail to the level ◁ Notify the theory solver
◁ Filter if needed ◁ Learning the backjump clause triggers unit propagation ◁ Confirm the changes of ◁ Make a new decision the trail to [[0..]]. It also tells the theory solver to restore its state to the level , and performs the saved trail filtering if needed (by invoking the function FilterSavedTrail). Finally, the backjump clause is learned, triggering the next propagation cycle. On the other hand, if no conflict is encountered during the propagation, and there are still atoms from the formula that are unassigned in , we first confirm the changes of the saved trail by invoking the function ConfirmPropagatedSavedLiterals. Then we pick a literal for the next decide and push it to as a decision literal.
TheoryPropagate which are responsible for the propagation are given in Algorithm 3.
The function UnitPropagate implements the well-known two-watched-literals algorithm for
unit propagation [
We assume that the function TheoryPropagate has a similar global structure, although its precise structure may depend on a concrete theory-specific procedure. It also processes the literals from in a loop, but not necessarily one by one (depending on a concrete procedure, it Algorithm 3 CDCL(T) algorithm with the trail saving enabled: propagation functions 1: UnitPropagate() 2: while there are unprocessed literals on do 3: ← UseSavedTrail() ◁ First, try to use the saved trail 4: if ̸= ∅ then ◁ If a conflict is found, return the conflicting clause 5: return 6: is next-to-process literal from 7: for all ∈ ℎ(¬) do ◁ process the watchlist of the falsified literal ¬ 8: ← FindAlternativeWatch(, ¬) 9: if ̸= ∅ then ◁ A new watch found 10: replaces ¬ as a watch literal of 11: move from ℎ(¬) to ℎ() 12: else ◁ All literals of are false, except, possibly, the other watch ′ 13: if the other watch ′ of is false in then 14: return ◁ is a conflicting clause 15: else if the other watch ′ of is undefined in then 16: ← + {′} ◁ Unit propagation 17: (′) = ◁ is the propagation reason 18: return ∅ 19: 20: TheoryPropagate() 21: while there are unprocessed literals on do 22: ← UseSavedTrail() ◁ First, try to use the saved trail 23: if ̸= ∅ then ◁ If a conflict is found, return the conflicting clause 24: return 25: 1, . . . , is next-to-process literals from ◁ is theory-dependent 26: (, ) ← DoTheTheoryInference(1, . . . , ) 27: if ̸= ∅ then ◁ If a theory conflict is found, return the theory conflict reason 28: return 29: for all in do ◁ Otherwise, push the inferred literals to 30: ← + {} 31: () ← ◁ The reason will be generated lazily, if needed 32: return ∅ might process all unprocessed literals at once). The function UseSavedTrail is invoked once per the loop iteration, before the processing of the literals. The theory-specific inference is captured by the function DoTheTheoryInference, which, by assumption, returns either a theory conflict reason , or the set of literals that are T-inferred from the prefix of up to the literal , in case when no theory conflict is encountered. In the latter case, the literals from are pushed to . However, their reasons are not set, since the reasons of T-inferred literals are usually generated by the theory solver lazily, i.e. only when needed, during the conflict analysis. Thus, we set () to a special value , which serves as a placeholder for the true reason which may be calculated later, if needed.
An issue that deserves a discussion here concerns the exact location and the frequency of
invocation of the function UseSavedTrail within the propagation functions. In case of the
unit-propagation, we exactly followed the approach from the original trail saving algorithm,
presented by Hickey and Bacchus [
The question remains whether this approach is the best approach. The rationale behind the approach is that the saved trail should be consulted whenever there are new literals on , since some of them may unblock the next portion of (recall that the consumption of is stopped when a saved decision literal that is undefined in is encountered). Although we cannot guarantee that each iteration of the loop will indeed produce new literals on , it will be the case very often in practice. On the other hand, too frequent invocation of the function UseSavedTrail should not be an issue, since its unfruitful calls are not expensive (the function will return immediately if the next literal on is a saved decision literal undefined in ). For this reason, we decided to stick to that approach. Further analysis of this issue is left for the future work.
Saving the theory propagation reasons. Another issue concerns saving of explanations of T-inferred literals. Recall that the function SaveTrail must save the propagation reasons of the inferred literals, together with the literals themselves. In case of unit-propagated literals, this is easy, since their reasons are the clauses of the formula (or some of the learned clauses), and they are immediately available. On the other side, the reasons of the T-inferred literals may not be known yet at the moment when the function SaveTrail is invoked, since we already said that the theory solvers usually produce reasons of propagations lazily, i.e. only when a reason is required during the conflict analysis. This problem can be resolved in two ways: • The theory solver may be asked to produce the reasons of all saved T-inferred literals eagerly, when the trail is saved during the execution of the SaveTrail function. The produced reasons are then saved in the same way as the reasons of the unit-propagated literals. This approach is very easy to implement, since it does not require any modification of the theory solver. On the other hand, producing all the reasons eagerly may be too expensive, since only a portion of them will be actually needed during the conflict analysis. • Instead of saving the reason of a T-inferred literal , we may only save the information that the theory solver is responsible for producing the reason of later.5 The reason will be produced lazily, when it is needed during the conflict analysis. In other words, the idea is to follow the usual approach used in SMT. The main problem with this approach is that the theory solver may not be able to produce the reason of a literal that is, technically, not pushed to as a T-inferred literal during the last propagation cycle, but it is copied from as a saved T-inferred literal from some previous propagation cycle. This means that the internal state of the theory solver has been changed meanwhile, possibly multiple times over consecutive backjumps. This also holds for the data structures within the theory solver that are used by the reason-generating procedures. Such data structures may not contain information needed for explaining the literals that are not propagated to by the theory solver in that propagation cycle, even if those literals are indeed T-consequences of the trail . In order to resolve this issue, non-trivial modification of the theory solver’s data structures may be needed, making this approach much more dificult to implement. 5In case of multiple theory solvers, when a combination of theories is considered, this information should contain a reference to the theory solver responsible for producing the reason of in the future.
In our work we follow the first approach, due to its simplicity. Examining the second approach is left for the future work.
For the purpose of evaluation, the trail saving method described in previous sections is
implemented within the SMT solver argosmt6, which is an open-source CDCL(T)-based SMT solver
implemented in the C++ programming language for research purposes. The solver includes two
theory solvers:
• The EUF theory solver based on the congruent closure procedure described in [
We evaluated the implementation on SMT-LIB [
For comparison, each instance was evaluated with and without trail saving enabled (the two versions of the solver are denoted by argosmt-ts and argosmt-nts, respectively). In both cases, time limit per instance was 1200 seconds. After the results were obtained, several benchmark families were excluded from the further analysis, either because they were too easy for our solver (all instances were solved in less then a second on average by both argosmt-nts and argosmt-ts) or too hard (no instance was solved in the given time limit by neither of the solver’s variants).8 The final results are presented in Table 1. 6The solver is available at github: https://github.com/milanbankovic/argosmt. To experiment with the trail saving, checkout the branch ts and then follow the instructions in the file README.md. 7Instances are available at: https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks 8Too easy: keymaera, meti-tarski, sal, spider_benchmarks (QF_LRA), CLEARSY, Rodin (QF_UF). Too hard: tropicalmatrix (QF_LRA). 42 56 16 49 163
The results show that the trail saving technique has a positive efect in case of some QF_LRA benchmark families, but there are also QF_LRA benchmark families for which the trail saving algorithm does not improve the solver’s performance (either it does not have any efect, or even induces some degradation of performance). On average, there is no significant diference between argosmt-nts and argosmt-ts on QF_LRA instances. On the other hand, the results are positive in general for QF_RDL instances, where argosmt-ts performs better on three of four benchmark families. Finally, the trail saving technique exhibits a bad performance on QF_UF instances on all benchmark families. These claims are also supported by the plots given in Figure 1.
The consistently bad performance on QF_UF instances is somewhat expected, and may be
explained by the expensiveness of the eager reason generation in case of the EUF theory solver.
Moreover, the EUF solver is not expected to benefit much from the saved literals, since it must
process all these literals again and perform merging of the corresponding congruence classes
anyway [
On the other hand, prior to the experiments it was expected that the simplex-based arithmetic
solver would benefit from the trail saving. Indeed, not only the eager reason generation is cheap,
but we can also expect that copying the saved literals from instead of propagating them
again by the theory solver might help in avoiding some very expensive pivoting steps within the
simplex procedure [
In addition to the main experimental evaluation presented in this section, we have also evaluated our solver on all QF_UFLRA benchmark families from SMT-LIB, in order to see how the trail saving method performs when the combination of the two theories is considered. These results are not presented here, since there were not almost any diference in behaviour between argosmt-nts and argosmt-ts on these instances.
We also did some preliminary evaluation on QF_LIA instances, but taken only from several randomly selected benchmark families, which was not suficient to draw some general conclusions. However, the obtained results suggest the similar behaviour as on QF_LRA instances (that is, the behaviour greatly depends on the chosen benchmark family9).
Finally, let us mention that Hickey and Bacchus in their original work [
In this paper, we have discussed the potential of using the method of trail saving within SMT solvers. For the purpose of evaluation, we have implemented the trail saving method within a CDCL(T)-based SMT solver argosmt, equipped with two theory solvers which are among the most commonly implemented within modern SMT solvers – the congruence closure EUF theory solver, and simplex-based linear arithmetic theory solver. Our experimental results show that the trail saving exhibits a consistently bad performance on EUF instances, which is probably caused by the expensiveness of the eager reason generation strategy. On the other hand, the efectiveness of the trail saving on linear arithmetic instances greatly depends on the chosen benchmark family, and further investigation is needed in order to discover the exact traits of the benchmarks that determine the behaviour of the trail saving. Our hypothesis that the eficiency gains should be proportional to the degree of utilization of the saved trail was not supported by the obtained experimental results. This means that the main efect of the trail saving may not be in speeding up the propagation, which was our starting assumption. The main efect is probably the influence on the search, since the saved reasons influence the conflict analysis and the learned backjump clauses. The main line of the further work is, therefore, to perform a more detailed analysis of these efects. Another further research direction is to evaluate the method on other important theories used in SMT (such as theory of arrays, bitvectors and so on). Finally, since the implementation details may significantly influence the obtained experimental results, it might be needed to implement the technique within some state-of-the-art SMT solver, in order to more reliably evaluate the potential of the trail saving method in SMT solving.
This work was partially supported by the Serbian Ministry of Science grant 174021. We are very grateful to the anonymous reviewers whose insightful comments and remarks helped us to make this text much better. 9For example, trail saving performed well on the convert, rings and tropical_matrix benchmark families, but not on the slacks, mathsat and wisa families.