The satisfiability of constraints in the theory of equality and uninterpreted functions, a core component of SMT solving, can be decided via a congruence closure algorithm. Classical congruence closure algorithms can provide machine checkable proofs when explaining why terms are equal. Recently, Flatt et al. at FMCAD'22 presented a modified congruence closure algorithm producing demonstrably shorter proofs. The algorithm was implemented and evaluated in the context of equality saturation tools. In this extended abstract we present initial work on implementing this new congruence closure algorithm in cvc5, a state-of-the-art SMT solver. We discuss the challenges from adapting a high-performance implementation and how to address them efectively. We evaluate the implementation on a large set of SMT-LIB benchmarks, and demonstrate experimentally how this new algorithm results in smaller proofs in real-world scenarios. Moreover, we evaluate the performance impact of the new algorithm and determine whether the smaller explanations that can be generated from the shorter proofs are worth the performance overhead of the more expensive algorithm.
Proof-producing SMT solvers have a large potential for increasing the trustworthiness of formal methods applications that rely on solvers to discharge proof obligations. SMT solvers however can produce large proof certificates that can be challenging to check quickly, specially in tools with limited performance, such as formally verified checkers or proof assistants. One way to mitigate this issue is to employ solving techniques that can lead to shorter proofs within the same proof calculus, which will therefore be simpler to check. Flatt et a1]l.p[roposed such a procedure for the classical congruence closure algorithm in the context of equality saturation. In this paper we present an initial implementation of this approach in the congruence closure engine of the state-of-the-art SMT solve2r]. cEvxct5e[nding the core component of state-of-the-art SMT solvers is notoriously challe3]n,gaindg [we discuss the several challenges specific to this setting that we had to face, such as considering backtracking and avoiding cyclic explanations. We also present an evaluation of the current implementation, which indicates a number of future directions of improvements and some encouraging proof compression rates in proofs from the congruence closure algorithm.
Congruence is the property of equality that states that if two atnerdmsare equal, then, for any function , () = ()
. For a given set of equalities, we say that the corresponding congruence closure is the minimal equivalence relation that satisfies these equalities as well as the properties of reflexivity, symmetry, transitivity and congruence.
Eficient algorithms for computing congruence closure were first described by Downey et4a]la. n[ d Nelson and Oppen 5[], where the main application was determining the equivalence of expressions
CEUR
ceur-ws.org in a program, for the purpose of program verification. This algorithm is basedUonnioan-find data structure6[], where each term is a vertex in a graph (calledeqtuhaelity graph, or e-graph), and each equivalence class forms a rooted tree, whose root is called threepcrleassesntative. The graph is built by processing equalities sequentially. At the start, each term is part of an equivalence class containing only itself. When the algorithm processes an equa=lity, if the terms are not already equivalent, it mustmerge their equivalence classes. First it finds the representativeasnodf and then adds an edge between them, with one of them becoming the representative of the merged class.
Then, the algorithm must merge all classes that have become equivalent due to the congruence property. For example, when t h=e is asserted, the ter m()s and () are now also equivalent, so the algorithm must also merge their classes. We call edges added in tchoinsgsrtueepnce edges, and the terms that caused them to be added tjuhsetificration . In our example, the congruence edge that merged the classes o (f) and () will have the term{,s} as its justification.
Once the equality graph is built, whether two terms are equal is determined by finding their class representatives and checking if they are the same. However, for many applications, responding to these queries with a “yes” or “no” answer is not suficient. In some cases, like for SMT solverse,xapnlanation of why two terms are equal is also necessary. These explanations take the form of a set of equalities suficient to ensure that the terms are equivalent. In SMT solvers, producing explanations is crucial since they are used to build conflict clauses in the solver. In the CD)CaLl(gorithm7[] used by most SMT solvers, the solver will make a series of assumptions and use the theory solvers to determine whether they are consistent. If they are not, the theory solver will provide a conflict clause — a subset of the assumptions that is by itself inconsistent, which is used to prune part of the search space. Note that a smaller clause will increase the pruning, and is thus more useful to the solver. Thus, a congruence closure algorithm that can provide explanations (and ideally, short explanations) is crucial for a high performance SMT solver. However, it is well known that finding the smallest possible explanation for the equivalence of two terms is an NP-complete probl8e]m. [ Congruence closure and proofs. Some congruence closure algorithms are also capable of producing proofs. While an explanation is just a set of equalities, a proof is a derivation that uses these equalities and the properties of reflexivity, symmetry, transitivity and congruence to show that the two terms are equivalent.
Proofs from a congruence closure algorithm are also useful for SMT solvers, since they allow the
solver to provide a proof for the unsatisfiability of a formula as a whole. Proof-producing SMT
solvers have become increasingly important in the last few years, and are already used in many
applications9[
A proof-producing congruence closure algorithm is described by Nieuwenhuis et a1l5.].inW[hen asked to explain two equivalent terms, this algorithm traverses the path between them in the equality graph. When encountering a non-congruence edge, the algorithm simply stores the equality that caused that edge to be merged. When encountering a congruence edge with justific{a1t, io2}n, the algorithm recursively explains the equivalence of the t1eramnds 2, and adds all returned equalities to the explanation. Figur1eshows the pseudocode for this algorithm.
While the explanations returned by this algorithm are minimal, they are not nemciensismaurmil,y meaning a shorter explanation may often exist. A property of these algorithms that allows this to happen is the fact that they ignore equalities between terms that were already determined to be equal (calledredundant equalities). For example, if an algorithm has already determined that the atnerdms are equivalent due to some long series of equalities, if it then encounters the e=qua,liittywill discard it. Later, when queried for an explanation of these terms’ equivalence, it would provide a long function get_explanation(start, end): let explanation = [] let lca = find_lowest_common_ancestor(start, end) explanation += explain_along_path(start, lca) explanation += explain_along_path(end, lca) return explanation function explain_along_path(lower, upper): let explanation = [] let current = lower while current != upper: let edge = current.edge_to_parent() if edge.is_congruence_edge(): let (j1, j2) = edge.justification() explanation += get_explanation(j1, j2) else:
explanation += edge current = current.parent() return explanation set of equalities, where the singleton explana{t=io}n would sufice. Observing this limitation, Flatt et al. 1[] developed two new congruence closure algorithms, caTlrleedOpt andGreedy, that do not discard redundant equalities, and instead use them to provide shorter proofs and potentially smaller explanations.
When encountering a redundant equal=ity , these algorithms add the ed(g,e) to the equality graph, not triggering any merges (as the terms were already in the same equivalence class). Now, each equivalence class is not necessarily a tree anymore, so there may be more than one path between two terms in it. Naturally, when queried for an explanation, the goal of these algorithms is to find the path between the terms that represents the shortest proof. This is where the strategies used by the two algorithms diverge. In the following sections, we give a high-level description of the two algorithms introduced by Flatt et a1]l,. b[ut a detailed description, as well as pseudocode, can be found in the original paper.
As mentioned earlier, finding the path between two equivalent terms that results in the smallest proof is an NP-complete problem8][. This is in part because the equalities used as premises to explain a congruence edge might also be reused to explain other edges in the path, meaning the best path to take depends on the edges you already took. If we instead assume that equalities in the proof cannot be shared (and instead have to be duplicated), the problem becomes tractable. This new definition of proof size is called the prooft’rsee size, whereas the original definition is calledDiAtsG size1.
The TreeOpt algorithm is a polynomial algorithm for finding the explanation with optimal tree size, hence the name. It does this by first attributing a weight to each edge, defined as the tree size of the proof for that edge. For non-congruence edges this value is always 1, and for congruence edges it is the tree size of the proof of its justification. Since the weight of a congruence edge might depend on the weight of other congruence edges, the algorithm needs to recompute these weights until it reaches a ifxed point.
Once the weight of all edges is computed, finding the optimal explanation amounts to simply finding 1This refers to the fact that, if we allow this sharing of equalities, the proof is represented by a directed acyclic graph (DAG), whereas if we do not allow sharing, it is represented by a tree. the shortest path between the two terms, taking care to recursively explain the justification of every congruence edge encountered.
The second algorithm presented by Flatt et1]ails.a[ greedy algorithm that attempts to find a small explanation without incurring an increase in complexity. To do this, the algorithm first computes an estimate of the proof size for each edge in the equality graph. This estimate is obtained by computing the proof size of the edge with the traditional congruence closure algorithm, that is, ignoring redundant equalities.
Once the estimates are calculated, the algorithm simply finds the shortest path between the terms, using the estimates as weights for the edges. The algorithm is parameterizfeudelbpyaarameter, which, similarly to1][, we set to 10 as a default. When it encounters a congruence edge, if the fuel is greater than 0, the algorithm recurses (and decrements its fuel) to explain the justification of the congruence edge. However, if the fuel is 0, the algorithm explains the justification by simply using the classical congruence closure algorithm, by finding a path which ignores redundant equalities.
We implemented these new congruence closure algorithms in c2v],ca5 [state-of-the-art SMT solver.
The existing theory solver for the theory of equality and uninterpreted functions, ecqaulalleidtyits
engine, implements a version of a proof-producing congruence closure algorithm as seen in Nieuwenhuis
et al. 1[
A big challenge in adapting the algorithms in Flatt1e]ttoalw. o[rk in a modern SMT solver was dealing with the context-dependent nature of the solver. The CD) CalLg(orithm, used by most modern SMT solvers, solves problems by testing many possible (partial) solutions and backtracking as soon as a solution is determined to be invalid.
This means that, from the viewpoint of the equality engine, the SMT solver will assert a series of equalities, query the equality engine for explaining the reason why a given equality holds, and, if the asserted equalities are found to be inconsistent, revert to a previous state. This means that the equality engine must be able to eficiently produce explanations for the equivalence of any two terms, while also at any point being able to backtrack to a previous state. To do that eficiently, the existing implementation carefully records the steps taken by the congruence closure algorithm, and structures the equality graph so that it can revert those steps, un-merging any equality classes that were merged since the respective backtracking point.
Keeping redundant equalities complicates this process. For example, when backtracking, the equality engine holds an invariant that the number of edges is the same as the number of class merges — since we modified the code to add edges that do not cause merges, we had to add “dummy” entries to the class merges vector in order to keep this invariant. Since some data is cached between calls to get_explanation (for example, the edge weights computed for tThreeOpt algorithm), we also had to make sure that no invalid cached data survives after a backtrack. Otherwise, agceatl_letxoplanation might use cached data from when the equality graph was in a diferent state, which might result in an invalid or suboptimal proof.
Since the equality engine in cvc5 is context-dependent, it is useful to think of the state of the equality graph in terms olfevels. The current level of the equality engine is defined as the number of equalities that were asserted, and for every equality that is backtracked, the level is decreased by 1.
Importantly, when explaining the justification of a congruence edge that was added i n,wleevel cannot use any redundant edges that were added in levels high er, otthhaenrwise the explanation might use that congruence edge itself. Consider the following example:
At level, the term is in the same equality class a, sseparated by a long path of edges. Sin ce and are equivalent, there is a congruence edge bet w(e)enand () , whose justification is{, } . In the next level+, 1 , the equality= () is asserted, merging the equivalence classes of these two terms. At lev e+l 2 , the redundant equal it=y () is asserted, and the corresponding redundant edge is added. Then, the explanation f(o)r≡ () is queried. When explaining the congruence edge between () and () , the algorithm must explain its justification, that is, find a path bet waenend . However, the shortest path between these terms will u(se()t, h()e) edge itself, resulting in a circular explanation.
(a) Example equality graph at level.
(b) Example equality graph at level+ 1 .
(c) Example equality graph at level+ 2 .
To prevent this, we store for each edge the level in which it was created. We also maadxd_eldevael parameter tgoet_explanation, and changed the algorithms to ignore edges whose level is bigger than the maximum level. When explaining a congruence edge with justifica{t i1o, n2}, max_level is set to the level in which1 and 2 were determined to be equivalent. In this way, no circular explanations can be constructed.
In order to evaluate the efectiveness and performance of our implementation, we tested it against a large set of benchmarks. More specifically, we used the 7502 SMT problems in the QF_UF logic from the SMT-LIB benchmarks library16[], an industry-standard set of benchmarks for SMT solvers. The results were generated with a cluster equipped with 16 x Intel(R) Xeon(R) CPU E5-2637 v4 @ 3.50GHz, 62.79 GiB RAM machines, with one core per solver/benchmark pair, 300s time limit, and 8 GB memory limit.
We compare the two newly implemented algorithTmres,eOpt and Greedy, with the classical congruence closure explanation algorithm, from here on referreVdatnoilalsa. We ran cvc5 on each benchmark, using each of the three algorithms. We recorded the time taken to solve each problem, as well as the size of the final proof. These results are shown in Sec4t.i1on
The explanations returned by the congruence closure algorithm inform the search of the SMT solver, which in turn changes which equalities are asserted to the equality engine, and the explanations that are requested. Therefore, simply looking at the final proof size is not the most direct way to compare the diferent algorithms. To get a more direct comparison, we instrumented cvc5 to, on each individual call toget_explanation, run all three algorithms at the same time and record the size of each explanation returned. These results are shown in Sect4i.2o.n
This data shows that, as expected, tThreeeOpt algorithm is much less eficient thanVanilla. On the other hand, the performance of Gthreeedy algorithm is not as bad, representing on average an 18% increase in runtime over tVhaenilla algorithm, and being in many cases faster than it. We believe theses cases are due to smaller conflict clauses being provided, thus pruning a larger portion of the search space, speeding up the solver.
As for proof size, we did not measure a significant impact of the new algorithms in the final proof size. On averageG,reedy andTreeOpt proofs were respectively 0.2% and 0.1% larger tVhaannilla proofs. In most cases, proofs from all three algorithms were almost exactly the same size. In the best cases, proofs fromGreedy andTreeOpt were respectively 80% and 78% smaller than the corresponding Vanilla proofs. However, in the worst cases, the two new algorithms produced proofs that were up to 70% larger than the correspondiVnagnilla proofs.
We also compared, in each callgteot_explanation, the sizes of the proofs returned by each algorithm. In particular, foGrreedy andTreeOpt, we are interested in the proof size ratio, that is, the size of the proof returned by the algorithm, divided by the size of the proof returnedVbayntilhlea algorithm.
For both algorithms, 83% of callsgteot_explanation result in proofs that are the same size as the Vanilla proof (that is, the proof size ratio is 1). For both algorithms, the average proof size ratio was 0.98, and the minimum was 0.065. This means that while most proofs produced by these algorithms are almost the same size as the ones froVmanilla, in some cases they can be up to 93.5% smaller.
Looking at only the proofs whose size actually changed between algorithms (that is, excluding those where the proof size ratio is 1), the average proof size ratio was 0.86 for both algorithms, representing a reduction in proof size of 14%.
In rare occasions, the algorithms produced larger proofsVtahnainlla. For Greedy, the worst proof size ratio was 2.2, and foTrreeOpt it was 1.75. This is explained by the fact that these algorithms search for proofs with minimal tree size, while the final size of the proof is computed as its DAG size.
In conclusion, our work shows that congruence closure algorithms that keep redundant equalities can be eficiently implemented in a state-of-the-art SMT solver, with reasonable runtime overhead. Furthermore, we show that these techniques can have a measurable, even if modest, impact on proof size. However, there are still many avenues for future work that need to be explored. For one, a more extensive evaluation is necessary, investigating benchmarks from logics beyond QF_UF, and considering other metrics like impact on proof checking time. Also, new algorithms and heuristics that use this technique may be developed that present better performance, or that are better suited for use in an SMT solver. While it is too soon to tell whether this technique will be practical for use in SMT solvers, we hope that we were able to show that is has a lot of potential. [15] R. Nieuwenhuis, A. Oliveras, Proof-producing congruence closure, in: J. Giesl (Ed.), Term Rewriting and Applications, Springer Berlin Heidelberg, Berlin, Heidelberg, 2005, pp. 453–468. [16] C. Barrett, P. Fontaine, C. Tinelli, The Satisfiability Modulo Theories Library (SMTww-LwI.BS)M,TLIB.org, 2016.