Automated Strategy Invention for Confluence of Term Rewrite Systems

We informally define some theoretical properties of term rewriting in this section, hoping to ease the understanding of the behavior underlining automatic confluence provers. A formal description can be found in the appendix.

We assume a disjoint set of variable symbols $\mathcal{V}$ and a finite signature $\mathcal{F}$. The set of terms $\mathcal{T(F,V)}$ is built up from $\mathcal{V}$ and $\mathcal{F}$. The set of variables occurring in a term $t$ is denoted by $\mathit{Var}(t)$. A term rewrite system (TRS) consists of a set of rewrite rules $l\rightarrow r$ where $l,r\in\mathcal{T(F,V)}$, $l\notin\mathcal{V}$, and $\mathit{Var}(r)\subseteq\mathit{Var}(l)$. We write $t_{1}\rightarrow^{*}t_{n}$ to denote $t_{1}\rightarrow t_{2}\rightarrow...\rightarrow t_{n}$ where $n$ could be one. A TRS is confluent if and only if $\forall s,t,u\in\mathcal{T(F,V)}(s\rightarrow^{*}t\land s\rightarrow^{*}u\Rightarrow\exists v\in\mathcal{T(F,V)}(t\rightarrow^{*}v\land u\rightarrow^{*}v))$. Consider the TRS of $\{f(g(x),h(x))\rightarrow a,g(b)\rightarrow d,h(c)\rightarrow d\}$ (Gramlich 1996). It is not confluent since $f(d,h(b))\leftarrow f(g(b),h(b))\rightarrow a$, and no rules are applicable to $f(d,h(b))$ and $a$. A term is called linear if no variable multiply occurs in it. A rewrite rule $l\rightarrow r$ is called left-linear if $l$ is linear. A TRS is called left-linear if all its rules are left-linear. Left-linearity is crucial for confluence analysis since most existing confluence techniques only apply to such systems. In this paper, a term is called compositional if it is neither a variable nor a constant.

CSI is one of the state-of-the-art automatic confluence provers that participates in the annual confluence competition. It ranks first in five categories of competitions in CoCo 2024. To show (non-)confluence of TRSs, CSI automatically executes a range of techniques, scheduled by a complicated configuration document written by experts in confluence analysis. Subsequently, CSI either outputs YES, NO, or MAYBE indicating confluence, non-confluence, or indetermination, respectively.

CSI implements 93 term rewriting analysis techniques (many of them parametrized or transforming the system into one that can be analyzed by other techniques) and utilizes a complicated strategy language to control them. In CSI, these techniques are called processors. They are designed to prove the properties of TRSs, perform various transformations, and check the satisfiability of certain conditions. The strategy language can flexibly combine the execution of processors such as specifying parallel or sequential applications, disregarding unexpected results, assigning time limits, and designating repeated applications.

Since the generated proofs are almost always large and difficult to manually check, CSI relies on an external certifier CeTA (Thiemann and Sternagel 2009) to verify its proofs. To utilize CeTA, CSI outputs a certificate of its proof in the certification problem format (Sternagel and Thiemann 2014). Given a certificate, CeTA will either answer CERTIFIED or present a reason to reject it. Not all processors implemented in CSI are verifiable because CSI cannot produce certificates for all processors, and CeTA does not implement the verification procedures for all processors.

Grackle (Hůla and Jakubův 2022) is a strategy optimization system designed to automate the generation of various effective strategies for a given solver based on benchmark problems. Such solvers receive a problem and decide the satisfiability of a particular property of the problem. It was originally designed for automated reasoning tools and has been applied to various solvers such as Prover9 (McCune 2005–2010), E (Schulz 2013) and Lash (Brown and Kaliszyk 2022) for proving boolean satisfiability problems (De Moura and Bjørner 2011) and Vampire (Kovács and Voronkov 2013) for proving satisfiability modulo theories problems (De Moura and Bjørner 2011). We choose Grackle for our research, as it is highly adaptable and we are not aware of any strategy invention program that would allow the kinds of strategies needed for automatic rewriting tools. Additionally, Grackle has achieved good results with the solvers it was previously applied to.

Given a set of problems as input, Grackle automatically invents a large number of strategies and selects those most complementary in problem solving. Here, complementation first means that each selected strategy must be most efficient for solving a number of unique problems. Moreover, it indicates that within a limit of the number of selected strategies, the combination of all selected strategies can maximize the number of provable problems.

Grackle repeatedly executes a dual-phase process to generate complementary strategies. The first phase is strategy evaluation, followed by strategy invention. Grackle users need to provide a number of initial strategies before the execution. In the evaluation phase, Grackle evaluates all strategies in its portfolio on a comprehensive benchmark with a selected time limit. Initially, the portfolio only comprises the initial strategies. New strategies are provided by the invention phase, and the strategies in the portfolio are updated based on the evaluation results. This evaluation clusters the set of benchmark problems into subsets $P_{S}$ for each strategy $S$, where $P_{S}$ contains the problems where the strategy $S$ performs best. Only the strategies mastering at least a given number of unique problems remain in the portfolio. In the invention phase, Grackle invents new strategies using the best-performing strategy $S$ and its corresponding benchmark problems $P_{S}$. New strategies are invented and tested on $P_{S}$ via external parameter tuning programs ParamILS (Hutter et al. 2009) or SMAC3 (Lindauer et al. 2022). Then, Grackle integrates the newly invented strategies into the portfolio and repeats the evaluation phase.

Grackle employs the same approach to describe its parameter search space as ParamILS. The space is described by a set of available parameters, each of which is associated with a default value and several disjoint potential values. Grackle users need to input the potential values based on their domain-specific experiences on the particular solvers.

In order to find new strategies for CSI, we need first to represent the parameter space in a meaningful way. Directly using a tool like Grackle to randomly combine parameters may produce unsound results. This is a unique challenge compared to previous applications of strategy invention. The solvers to which Grackle was previously applied cannot produce unsound results, while CSI’s users need to carefully specify their strategies to ensure soundness.

There are three reasons why CSI may produce unsound results given an entirely random strategy. First, some processors are not intended for confluence analysis. They may intend to prove other properties of TRSs, such as termination (Baader and Nipkow 1998). Second, even for the same processor, it may be designed to prove different properties of TRSs with different flags. Third, some transformation processors may transform the confluent problem into an unexpected problem. For example, they can transform it to a relative termination problem (Zantema 2004).

By default, CSI utilizes a complicated configuration document with 255 lines written by term rewriting experts to perform confluence analysis. A comprehensive explanation of a previous default strategy can be found in (Nagele, Felgenhauer, and Middeldorp 2017), which slightly differs from the contemporary default strategy.

We separate the default strategy of CSI into 23 sub-strategies, which, along with CSI’s default strategy, also serve as the initial strategies for Grackle. Among the 23 sub-strategies, eight are designed to show confluence, 14 are utilized to show non-confluence, and one is capable of showing both.

We maintain the structure used in CSI’s default strategy during the strategy invention. We make such a decision because CSI relies on proved theorems to (dis)prove confluence; however, not all theorems are implemented as a single processor. Such a theorem states that under particular conditions, if some properties of a TRS can be proved, then it is confluent. To utilize such theorems, we need to combine the strategy language and processors to perform transformations on the original TRS and prove the necessary properties of the transformed problem. If we generate strategies randomly, it will be difficult to generate such useful structures and may produce unsound strategies due to inappropriate transformations.

We search for three categories of parameters.

First, we search for processor flags which do not violate the soundness guarantee. To ensure soundness, we only search for flags for processors existing in CSI’s default strategy. Second, we include iteration parameters, such as time limits or repeated numbers of execution, to regulate the running of a certain sub-strategy. These parameters are defined in CSI’s strategy language. To reduce the overall parameter space and ensure soundness, our parameter space only incorporates the iteration parameters used for sub-strategies within CSI’s default strategy. These parameters may offer particular advantages since they are applied by term rewriting experts. Moreover, we add a boolean execution-controlling parameter for every parallel or sequential executed sub-strategies, indicating whether to run the particular sub-strategies in confluence analysis. Assume a strategy A||B, where || denotes a parallel execution. The boolean parameters for A and B can represent whether to run one, both, or neither of them. We do not assign boolean execution-controlling parameters to those sequentially executed sub-strategies if we are uncertain whether their exclusion will cause unsoundness.

We need to construct a strategy for CSI using the parameters searched by Grackle. To achieve this, we start with CSI’s default strategy, replacing the processor flags and iteration parameters with relevant invented parameters. Then, we disable sub-strategies according to the boolean execution-controlling parameters.

After inventing a number of complementary strategies, we want to properly combine them into a single strategy and compare it with the default strategy of CSI. The combination is performed by choosing several strategies from Grackle’s final portfolio and appropriately assigning a time limit to each of them.

In order to effectively divide the time, we split the whole one minute into several time splits. Next, we greedily allocate a strategy to each time split in the sequence by order. Each newly chosen strategy aims at proving the largest number of remaining benchmark problems that have not been proved by the previously chosen strategies. We shuffle the sequence 100 times and greedily select strategies for each shuffled sequence, resulting in strategy schedules comprising sequences of pairs of strategies and time splits. To utilize a strategy schedule, CSI executes each strategy in it by order for a duration of the relevant time split. We split the one-minute duration into many sequences and perform the greedy strategy selection for each. We finally choose the strategy schedule that maximizes the number of provable problems.

We develop a program to randomly generate a large dataset of TRSs, receiving multiple parameters to control the overall generation procedure.

First, the maximum number of available function symbols $F$, constants $C$, variables $V$, and rules $R$ establish the upper bound of the respective quantities of symbols and rules. For each of $F$, $C$, and $V$, a value is randomly selected between zero and the specified maximum, determining the actual number of available symbols. The actual number of rules is randomly chosen between one and $R$. Second, we define a parameter $M$, used during the initialization of function symbols. For each function symbol, an arity is randomly chosen between one and $M$

Another important parameter is the probability of generating a left-linear TRS $L$, which is associated with the likelihood of producing provably confluent TRSs. The majority of contemporary techniques for proving confluence are merely effective for left-linear TRSs. Without regulating the ratios of left-linearity, randomly generated TRSs rarely exhibit left-linearity, making it theoretically difficult to show confluence for them. We also notice that, in practice, CSI can merely prove confluence of very few generated TRSs if the ratios of left-linearity are not controlled. By default, we force 60% of generated TRSs to be left-linear.

Moreover, for a rule $l\rightarrow r$, there is a parameter called $CT$ regulating the probability of generating $l$ and $r$ that are compositional terms. We necessitate it because we prefer complex terms, while constants and variables are quite simple. The value of $CT$ can be larger than one, as it indicates the maximum probability. For each TRS, a value is randomly chosen between zero and $CT$, determining the likelihood of generating compositional terms. If the randomly chosen value is larger than one, we can only generate compositional terms.

Algorithm 1 presents the generation procedure of a single term. While choosing the root symbol, we first randomly sample a value between zero and one and compare it with $comp$ to determine whether to only use $funs$ as candidates for the root symbol. Here, $comp$ is a value randomly chosen between zero and $CT$ during the initialization stage of the generation of a TRS. Meanwhile, according to the definition of rewrite rules in Section 2.1, the left term $l$ in $l\rightarrow r$ cannot be a variable. After choosing a root symbol for the term $t$, we continuously choose new symbols for undefined function arguments until all of them are defined. After selecting a new variable, we need to remove it from the set of available variables if we are generating a left-linear TRS. The size of the terms generated by us is at most 15, where the size of a term is defined as the number of symbols in it. We choose 15 as the maximum value because the sizes of most terms in Cops are smaller than 15.

To generate a rule $l\rightarrow r$, we first execute Algorithm 1 to generate $l$ and then execute it again to generate $r$. We extract all used variables in $l$ and mark them as available variables for the generation of $r$, thereby $Var(r)\subseteq Var(l)$, as required by the definition of rewrite rules in Section 2.1.

We repeat the generation of rewrite rules until reaching the expected number and return the newly generated TRS.

We utilize the program explained in this section to construct a large dataset, facilitating the application of machine learning to confluence analysis. First, we randomly generate 100,000 TRSs with the parameters of the maximum number of available function symbols $F=12$, constants $C=5$, variables $V=8$, and rules $R=15$. Other parameters include the maximum arity of function symbols $M=8$, the probability of generating left-linear TRSs $L=0.6$, and the maximum probability of generating compositional terms $CT=1.6$.

However, the randomly generated dataset can be imbalanced for two reasons. First, there may be significant differences in the number of confluent, non-confluent, and indeterminate problems. Meanwhile, the number of problems mastered by different confluence analysis techniques may vary considerably.

We develop a multi-step procedure to build a relatively balanced dataset. First, we execute CSI’s default strategy on all generated TRSs for one minute using a single CPU. CSI outputs NO or YES or MAYBE for 69,317 or 25,012 or 5,671 TRSs, respectively.

Second, we randomly choose 5,000 problems from each set of problems classified as NO, YES, and MAYBE by CSI.

Third, we execute an unpublished duplicate checker used in CoCo 2024 to remove the duplications in the 15,000 chosen TRSs and 577 Cops TRSs. It checks the equivalence of syntactical structures between TRSs modulo renaming of variables and a special renaming on function symbols of their signatures. If TRSs of an equivalence class occur both in the randomly generated dataset and Cops, we only remove those randomly generated TRSs. We do not remove any duplicate examples from Cops because it is a representative dataset, and Cops merely contains 11 duplicated examples to remove.

Fourth, we want to mitigate the imbalance in the number of problems mastered by different confluence techniques. We execute 26 strategies for all TRSs, aiming at labeling each of them with the most effective strategy. The labeling strategies contain all initial strategies for Grackle, which are explained in Section 3.1. The other two that are used to prove confluence are extracted from two complicated initial strategies, both consisting of many sub-strategies and integrated with transformation techniques that potentially simplify the search for proofs. Specifically, the two complicated initial strategies parallelly execute two important confluence analysis techniques, development closedness (Van Oostrom 1997) and decreasing diagrams (Van Oostrom 1994), not used by the other initial sub-strategies. If we do not use them for labeling, we will not be able to understand whether a TRS is mastered by one of the two important confluence analysis techniques. The time limit for using CSI’s default strategy as a labeling strategy is one minute. The time limit for other labeling strategies is 30 seconds, smaller than one minute because the execution of decomposed sub-strategies is more efficient. We calculate the number of problems most efficiently solved by each labeling strategy. The randomly generated dataset is quite imbalanced, four strategies master more than 1,000 problems; however, 15 strategies master less than 200 problems. To address the imbalance, we randomly choose at most 300 problems for a strategy from its set of mastered problems. We also randomly add 1,200 problems that cannot be solved by any labeling strategy to the dataset.

Finally, we obtain a dataset consisting of 5,192 TRSs. Within this dataset, 1,569 TRSs are classified as confluent, 1,936 as non-confluent, and 1,687 as indeterminate when evaluated by CSI using a single CPU within a one-minute time limit.

Figure 1 shows the final distribution of the number of problems mastered by each labeling strategy. It is not perfectly balanced; however, we consider it relatively balanced, given that certain strategies can only master problems that satisfy particular properties. Such properties can be uncommon in randomly generated TRSs and practical applications.

There are infinitely many strategies that can be chosen as labeling strategies, such as strategies obtained by changing processor flags. We do not choose other labeling strategies because we have already decomposed CSI’s default strategy, enabling us to label problems with all categories of confluence analysis techniques implemented in CSI. Further decomposition or modification of processor flags may allocate problems to different labeling strategies that only slightly differ.

The Cops 2023 dataset comprises a total of 1,655 problems of which 577 are TRS problems. We focus on evaluating our approach on TRS problems since they are standard term rewriting problems for confluence analysis and represent the major category in Cops. Another evaluation dataset consists of data from both Cops and our randomly generated datasets in Section 4.2. For training purposes, we arbitrarily select 289 examples from Cops and 800 examples from the randomly generated dataset. To build the test dataset, we exclude the examples in the training dataset, subsequently randomly selecting 800 examples from the randomly generated dataset and the remaining 288 examples from Cops.

The Grackle time limit for proving a problem is 30 seconds, employed both in the evaluation and the strategy invention phases. During the invention phase, Grackle launches ParamILS which tries to solve the problems with various strategies and outputs the best strategy found. The overall time limit for one strategy invention phase is 45 minutes. Grackle interleaves several evaluation and invention phases. The total execution time of Grackle is two days. Grackle performs parallel execution in both the evaluation and invention phases; therefore, we also limit the number of CPUs it can use. For each dataset, we perform two Grackle runs, configuring the numbers of available CPUs for a single strategy run to be either one or four. When it is set to one and four, the total number of available CPUs for Grackle is set to 52 and 66, respectively. Here, a CPU denotes a core of the AMD EPYC 7513 32-core processor. Grackle’s portfolio stores at most 100 best strategies. Our search space consists of 353 parameters of which 192 are boolean. The entire search space approximately covers $2^{562}$ combinations of parameters.

The use of four CPUs has been selected to match the results of CSI’s default strategy in CoCo 2023 on the competition setup. Given exactly the same problems solved by CSI in our setup described above with four CPUs and in the CoCo competition in their Starexec setup we consider the further comparisons in the paper fair.