Cooperation of Heterogeneous Provers

1 Introduct ion

Search is a central problem solving method employed in AI systems. For most problem areas there exist many systems based on different search paradigms like branch­ and-bound, evolutionary algorithms , or problem decom­ position. All these paradigms have different strengths and weaknesses and much effort has been invested in implementing systems suitable for dealing with hard and interesting problem instances.

An example for such a problem area is automated de­ duction. The paradigms used are problem decomposi­ tion in analytical provers and (intelligent) enumeration of logical consequences in saturation-based provers. For each paradigm there are several calculi and for each cal­ culus different implementations, typically with many pa­ rameters allowing for different incarnations of a prover.

Many experimental studies and prover competitions have shown that it is very difficult to find a priori the best prover for a given problem instance. Therefore com­ petition approaches where several incarnations of one prover or several provers run on different machines until one prover is successful have been proposed (see [Ertel , 1992J) and are used in applications. However, from an economical point of view such approaches are not very ef­ ficient, since only one machine contributes to solving the instance. A cooperation of the provers would be more in­ teresting and should also lead to finding solutions faster by achieving synergetical effects.

There are approaches for cooperation of homogeneous search systems that have been used for coupling differ­ ent incarnations of the same prover. Further, Sutcliffe [1992] proposed a concept for heterogeneous provers but failed to deliver convincing results. The problems to solve in order to achieve a successful cooperation of dif­ ferent provers are (1) finding appropriate types of results to interchange, (2) selecting useful results out of the large number of produced results, and (3) having efficient im­ plementations of the provers.

In this paper, we present a general approach for achieving cooperation between search systems using dif­ ferent paradigms that tackles the problems mentioned above for automated deduction. Our TECHS approach (TEams for Cooperative Heterogeneous Search) allows us to use existing provers with only small modifications, limits the amount of communication by filtering the re­ sults of a sending prover, does not unnecessarily disturb the work of receiving provers since received data is fi l­ tered with respect to current and future needs, and has the ability to integrate specialized provers.

Our experiments with three state-of-the-art provers, namely SPASS, SETHEO and DISCOUNT, show that their cooperation indeed outperforms the simple compe­ tition approach for all tested domains and all time lim­ its. In the tested domains of the TPTP ([Sutcliffe et al., 1994]) TECHS solves up to twice as many hard prob­ lems as can be solved by the individual provers taken together.

2 The TECHS Approach

The general idea of the TECHS approach is to inter­ change selected results between the search agents of a search team in regular time intervals. The search agents are incarnations of the search systems that have been in­ tegrated into the distributed system by enhancing them with communication facilities. If there is more than one incarnation of a search system in the team then the in­ carnations have to differ in their search control. We call the phases where the search agents independently work on their problem working phases, the phases where in­ formation is exchanged cooperation phases.

To start the team, each agent is given either the whole problem instance to solve or the parts of the instance it can work with. The selection process of results takes place both on the side of a sending agent, by a so-called send-referee, and on the side of the receiving agent, by a so-called receive-referee . .Each search agent may have between 1 and n- 1 send-referees, if there are n agents in the team, and 1 or no receive-referee.

The task of a send-referee is to select results from the current search state of its agent that should be communi­ cated to the other agents the send-referee is responsible for. The criteria used by a send-referee are either totally based on the success the results have had for its agent or include some general knowledge about the demands of the receiving agents. If a send-referee is responsible for the selection of results for more than one receiving agent, in most cases only success-based criteria can be used. Typically send-referees evaluate results with re­ spect to their syntactic structure and the search steps the results were involved in.

The task of a receive-referee is to select those results sent to its agent that are considered useful for its agent in its current state or in future states. Therefore the criteria used by receive-referees either reflect the current demands and needs of its agent or try to anticipate fu­ ture demands and needs. Because an agent receives only a small number of results , the criteria used by receive­ agents can involve more expensive computations, like the impact of a result on the current search state, than in the case of send-referees.

3 TECHS in Theorem Proving

In theorem proving, the TECHS approach requires dif­ ferent provers running in parallel on different computing nodes . Proof problems are specified in first-order clausal logic. The provers employ either calculi which are com­ plete for first-order logic (universal provers) or calculi which are complete for a sub-logic of first-order logic (specialized provers). We allow the use of saturation­ based and analytic calculi.

In the following, we first introduce the saturation­ based calculi superposition and unfailing completion, and the analytical connection tableau calculus. This is be­ cause we employ provers based on these calculi in our experiments. After that, we explain in detail how the TECHS concept can be instantiated for provers based on the introduced calculi. Since clauses are to be ex­ changed between the provers we must at first cope with the topic of how to extract clauses from the proof search . After that, we proceed by introducing several methods for selecting clauses, i.e. we describe possible send- and receive-referees. Finally, we explain how a prover can integrate received clauses into its search state.

3.1 Basics of Theorem Proving

The superposition calculus ([Bachmair and Ganzinger, 1994]) contains several inference rules which can be ap­ plied to a set of clauses that constitute a search state. Generally, its inference rules are expansion inference rules (superposition left and right, equality resolution, and equality factoring). These rules allow the genera­ tion of new clauses that are added to the search state. All inference rules are well-suited for handling equality, i.e. no equality axioms are needed. In addition to expan­ sion rules contraction rules like rewriting or subsumption can be employed. These rules delete redundant clauses or replace clauses by simpler ones.

In order to show the inconsistency of a clause set C, starting with C derivations of clause sets have to be per­ formed until a set D is derived which contains the empty clause. A theorem prover based on superposition usu­ ally maintains a set ;:P of so-called passive clauses from which it selects and removes one clause C at a time. This clause is put into the set ;:A of activated clauses. Activated clauses are, unlike passive clauses, allowed to produce new clauses via the application of some infer­ ence rules. The inferred new clauses are put into ;:P. Initially, :FA = 0 and ;:P = C. The search stops if the empty clause is derived. The indeterministic selection or activation step is realized by heuristic means. A heuris­ tic 1i associates a number we E 1N with each C E ;:P, and the C E ;:P with the smallest weight we is selected.

The unfailing completion procedure ([Bachmair et al., 1989]) essentially is a restriction of superposition to unit equations and allows for the development of efficient provers for pure equational logic.

The connection tableau calculus ( CTC for short) works on connection tableaux for a clause set C (see [Letz et al., 1994]). It employs three inference rules in order to transform one tableau (tree of literals) into another. The start rule attaches the literals of an input clause be­ neath the unmarked root node. Tableau reduction uni­ fies a literal s at the leaf of an open branch with the complement of a literal r on the same branch, and ap­ plies the substitution to the whole tableau . Hence, by reduction branches can be closed. If a literal of an input clause is unifiable with the complement of the leaf lit­ eral of an open branch, extension can attach the literals of the input clause beneath the leaf literal. Since the tableau must remain connected after the extension step (each non-leaf literal must be identical to the comple­ ment of one of its immediate successors in the tree) the tableau must be instantiated with this unifier (see [Letz et al., 1994]). Because the CTC has no specific rules for handling equality, equality axioms must possibly be added to the axiomatization.

In order to show the inconsistency of a set C, all tableaux derivable from the trivial tableau have to be enumerated until a closed tableau appears. This search space can be represented by a search tree. Nor­ mally, tableaux enumeration procedures apply consecu­ tively bounded iterative deepening search with backtrack­ ing ([Korf, 1985]). In this approach iteratively larger finite initial parts of the search tree are explored with depth-first search.

3.2 Extraction of clauses

The first step of an exchange of information is the ex­ traction of clauses from the search states a prover has produced in a working phase. We distinguish between saturation-based and CTC-based provers.

The extraction of valid clauses from search states of saturation-based provers is very easy because search states are sets of clauses. Even more, a theorem prover can take all interesting clauses to be selected from the ac­ tual search state at the beginning of a cooperation phase. This is because the provers only derive new clauses, delete unnecessary clauses , or simplify clauses . Hence, the sequence of produced search states (clause sets) is not needed. It is sufficient to consider the most recently derived clause set. We restricted ourselves to the extrac­ tion of active clauses since these clauses are maximally contracted w.r .t . the current clause set.

CTC-based provers conduct a search with iterative deepening and backtracking in the search tree of all con­ nection tableaux. A single search state is only one of these tableaux. Hence, it is only possible to extract in­ formation on one proof attempt from a search state. If the proof attempt represented by the search state does not lead to a proof it might be that all clauses which can be extracted from it are unnecessary. Then, send­ referees might have to chose from a pool consisting of unnecessary clauses only. This shows that clauses must be extracted from all search states enumerated during a working phase, i.e. they must essentially be extracted from the search tree of all tableaux.

Because of the fact that the search tree of all tableaux is in general not given explicitly, clauses must be ex­ tracted from the enumerated tableaux during the search process. A possible method to do this is to utilize bottom­ up lemma mechanisms (see, e.g., [Letz et al., 1994]) of connection tableau-based theorem provers. We used a second variant and extracted top-down lemmas, so-called subgoal clauses (see [Fuchs, 1998a]) , from a tableau . A subgoal clause is the clause of the open leaf literals of a tableau. Before a send-referee is applied to the set of extracted clauses it is reasonable to compute a minimal clause set by eliminating subsumed clauses.

3.3 Realization of send-referees

A send-referee in a system based on the TECHS ap­ proach consists of a pair ( S, <p) of a filter predicate S and a selection function <p. The prover that receives the results of the send-referee obtains those clauses in the cooperation phases that pass through the filter and that are selected by <p. The filter predicate S limits the set of clauses that are eligible for transmission. Typically, clauses are filtered out that are redundant w.r.t . the re­ ceivers. Redundant means that a receiver cannot use the clauses in its inference mechanism due to its spe­ cific logic. The selection function <p can employ several judgment functions 'lj;l, ... , 'lj;n. These functions 'lj;; as­ sociate a natural number with each clause C, and C is considered the better the higher the value 'lj;; (C) is. <p eventually selects the clauses with the best judgments.

Firstly, we have developed a judgment function 'lj;gen which considers syntactic features of clauses. It com­ putes a weighted sum of the number of variables and two times the number of function symbols of a clause and hence prefers general short clauses which contain many variables and only few function symbols. These clauses are useful for saturation-based provers because they might often take part in contracting inferences (subsumption , rewriting). They are often also useful for CTC-based provers because open tableau branches might be closed by extending the branches with them and closing the introduced literals with reduction steps.

Secondly, function 'lj;hi·t judges the role of clauses in the search process conducted so far. It is defined by 'lj;hist(C) = a1 ·sub( C)+ a2 · exp(C), a1 > 0 > a2 . For a saturation-based prover, sub( C) denotes the number of clauses subsumed by C, exp(C) is the number of ex­ pansion inferences C was involved in. For a CTC-based prover, sub( C) is the number of clauses subsumed by C after the extraction and exp( C) is the number of exten­ sion or reduction inferences applied to (instances) of lit­ erals of C. If the receiver of clauses is a saturation-based prover the idea is to select clauses which may reduce the search space by subsuming other clauses without simul­ taneously introducing many new clauses by expanding inferences. The criterion is also sensible for receiving CTC-based provers because an uncontrolled increase of the search space caused by the additional clauses might be prevented.

Finally, we employ the function 'lj;deriv that judges the derivation tree of a clause w.r.t . its possible useful­ ness for the receiver. The derivation tree of a clause taken from a clause set of a saturation-based prover can partially be constructed by tracing back the infer­ ences needed to infer the clause as far as possible (re­ call that clauses may be deleted during the derivation) . The derivation tree of a subgoal clause of a CTC-based prover is represented by the tableau the clause was ex­ tracted from. If a clause is selected for a saturation-based prover utilizing heuristic 1l the function 'lj;deriv considers whether clauses with a high heuristic weight regarding 1l are part of the derivation tree. If this is the case, it might be difficult for the receiver to infer the clause on its own and hence the proof search can drastically be reduced if the clause is needed in a proof. If the receiver of a clause is a CTC-based prover and the sender a saturation-based prover, we consider whether the clause is the result of an equality inference like superposition. Such clauses are especially useful for CTC-based provers since they have difficulties handling equality. If sender and receiver are CTC-based provers, such subgoal clauses are use­ ful whose respective tableaux can only be inferred by the receiver if a high resource value is employed. Then , high speed-ups can occur if such clauses can be used in a proof.

Due to lack of space we cannot describe the referees in detail. Exact descriptions of send-referees for super­ position and unfailing completion provers can be found in [Fuchs and Denzinger, 1997), descriptions of send­ referees for CTC-based provers in [Fuchs, 1998a] and [Fuchs , 1999].

3.4 Realization of receive-referees

A receive-referee is a selection function <p which also uses judgment functions for measuring the quality of clauses. Our first function 1/Jpop. judges whether a received clause may be part of a proof that can quickly be found. For a saturation-based prover 1/Jpop is defined by 1/Jpop(C) = LC'EFA v(C, C'). v judges whether both C and C' contribute to a proof. E.g., for superposition­ based provers v judges whether many short clauses can be derived from C and C'. Exact definitions of the function v for superposition and unfailing completion provers can be found in [Fuchs and Denzinger, 1997] . In our approach, CTC-based provers employ receive­ referees only if they receive clauses from saturation­ based provers. Then, we define 1/Jpop as follows . If S is the set of extracted subgoal clauses of the receiving prover, 1/Jpop (C) = LC'ES v(C, C'). There, v judges whether C might contribute to close the tableau rep­ resented by the subgoal clause C'. The function sim­ ply computes the difference of the number of tableau branches which can be closed by C and the number of branches that remain open.

The second judgment function 1/Jdse prefers clauses which need not be part of a proof but are nevertheless able to decrease the search effort in future . We use this function for saturation-based provers only. The function 1/Jdse produces higher values if many contracting infer­ ences are possible with a clause. Again, exact definitions can be found in [Fuchs and Denzinger, 1997].

3.5 Integration of clauses

The integration of clauses into the search state of a superposition-based prover · is very simple since it works on sets of clauses . Thus , a clause can be integrated by adding it to the set of active clauses and performing all inferences possible with it (see [Fuchs, 1998b]).

For the integration of clauses into the search state of a CTC-based prover there exist two possibilities. The first is to add the new clauses to the old axioms and to per­ form a re-start of the proof run. The second is to avoid a re-start, to add the new clauses to the old axioms, and to continue the search at the current choice point. The first variant has the disadvantage that the whole search of a CTC-based prover is lost and must possibly be re­ peated. However, the variant has the advantage that it can be implemented very easily. Moreover, in contrast to the second variant it guarantees that during the itera­ tive deepening process a proof can be found in a minimal segment of the search space. Since the segments usually grow exponentially, despite the repetition of parts of the work done so far proofs may then be found faster. There­ fore, we decided to employ the simple first variant .

4 Experiments

In order to reveal the power of our cooperation approach we conducted experimental studies with the well-known theorem provers SPASS, SETHEO, and DISCOUNT run­ ning on different workstations of a prover network. We have chosen two different test areas: on the one hand several domains from the TPTP problem library v.l.2.1., on the other hand problems stemming from an applica­ tion in software component retrieval. In the following , all time limits or intervals are measured as wall clock time, which means that for the cooperative runs also the time needed for communication is included. Communi­ cation was implemented in the simplest way possible, via reading from and writing in files.

4.1 Experiments with TPTP domains

We have chosen the domains BOO, CAT, COL, and GRP as our test domains. These domains cover a large num­ ber of problems with different difficulty. Most problems contain unit equations so that the equational prover DIS­ COUNT can at least obtain parts of the proof problems .

We coupled the provers SPASS, SETHEO, and Dis­ couNT in the following way. SPASS and SETHEO run in their standard settings (that were used for the CADE competition CASC-13). Since the DISCOUNT standard heuristic AddWeight is very similar to that of SPASS, we used a goal-oriented heuristic for DISCOUNT as de­ scribed in [Denzinger and Fuchs, 1994]. This heuristic is not as powerful as the AddWeight heuristic when work­ ing alone but is well-suited for cooperation purposes. We allowed for a bidirectional information exchange be­ tween SPASS and SETHEO and between SPASS and DISCOUNT every 5 seconds. SETHEO and DISCOUNT did not exchange information. This is because subgoal clauses of SETHEO are mainly non-unit clauses which are useless for DISCOUNT. Further , it is not sensible to add too many equations to the input set of SETHEO because this increases the branching rate of the search tree too much. The referees were parameterized as fol­ lows. SPASS and DISCOUNT selected 10 clauses for each other via send-referees, 5 of these clauses were finally selected by their receive-referees. For achieving cooper­ ation between SPASS and SETHEO, their send-referees selected 40 clauses . Then, their receive-referees selected from these clauses 10 clauses in the domains COL and GRP, 30 clauses in the domains CAT and BOO.

Table 1 presents the results obtained in form of the number of hard problems solved within a certain time limit. A problem is 'hard' if none of the provers alone can solve it within 10 seconds. Table 1 displays the results of the single provers, of a competitive parallel system consisting of the three provers ( comp), and the results of cooperative systems consisting of SPASS and SETHEO (SP-SE), SPASS and DISCOUNT (SP-DI), and of all provers (all).

In all tested domains, the cooperation of all provers outperforms the competitive approach for all time lim­ its, for domain CAT it even solves twice the number of problems. Even with only one cooperation phase (i.e.

with a :::; lOs time limit) the results are already better than the results of the single provers and the competitive approach. The BOO and GRP domains show that all systems contribute to the improvement in performance.

It should be noted that the performance of DISCOUNT alone (and in comp) is very bad due to the fact that the results of the goal-oriented heuristic are reported. But even if we "cheat" and report the results of Add Weight, the results of comp still are worse than the TECHS coop­ eration (while the results in CAT and COL would remain unchanged, for BOO 9 and for GRP 43 problems would be solved within the 500 seconds).

4.2 Experiments with software component retrieval

Besides the use of TPTP domains, we have evaluated TECHS with problems stemming from a concrete ap­ plication, namely software component retrieval. These problems are generated by the NORA/HAMMR tool that tries to retrieve software components with deductive techniques (see [Schumann and Fischer, 1997]). There, we have the following situation. Software components are available in a software library and specified by their pre- and postconditions. Queries are also formulated by pre- and postconditions. In order to find a suitable library component for a given query proof tasks are con­ structed that check for each library component whether or not it matches the query (via plug-in compatibility). We have chosen a library and queries of list processing functions and constructed several proof problems from it. All in all, we tackled 81 provable problems.

In order to solve these problems, we coupled SPASS , DISCOUNT, and SETHEO in the following way. We used all provers in their standard settings. Whereas SPASS and DISCOUNT were coupled in a bidirectional manner as before, we only allowed SPASS to send se­ lected clauses to SETHEO. The integration of subgoal clauses of SETHEO into the search states of SPASS and DISCOUNT decreased the performance. Again, we let the provers cooperate every 5 seconds. The referees were pa­ rameterized as for domains CAT and BOO.

Table 2 presents the results obtained in form of the number of problems solved within certain time limits. Again, we observe a significantly better performance by the cooperation of all systems than by the competitive approach. While the competitive approach can merely slight ly increase the number of problems solvable in the time limit , all cooperative combinations significantly in­ crease the success rate. Note again that the best perfor­ mance is achieved if all systems are working together.

5 Related Work

Distribution and cooperation concepts for search sys­ tems have mainly been developed as homogeneous con­ cepts. This is also true for automated theorem prov­ ing, as several overview paper indicate (see, for exam­ ple, [Bonacina and Hsiang, 1994]). A concept , that is by many considered heterogeneous , is A-Teams (see [Taluk­ dar et al., 1993]). A-Teams is a shared-memory, data flow architecture like approach in which agents work­ ing on the same type of results use the appropriate part of the shared memory as a common search state. So far, no effort has been undertaken to inc! ude tree- or graph-based search paradigms in A-Teams. Also, the cooperation of A-Team agents is much closer than the cooperation of TECHS agents, since an A-Teams agent communicates the results of each search step it has per­ formed. This does not allow to use existing search sys­ tems as agents easily. In A-Teams there is also no referee concept for limiting communication.

Another concept, that has a certain heterogeneous fla­ vor , is Teamwork [Denzinger, 1995]. Teamwork has been developed to distribute automated deduction [Denzinger et al., 1997] and has some similarities to TECHS. In Teamwork, periodically the work of the search agents is evaluated by referees that use success-based criteria to judge the whole agent and to select good results. In contrast to TECHS , for all agents a new common start state is generated by using the state of the best agent and the selected results of the other agents. So, most of the agents are different incarnations of one search systems. Other agents, called specialists, can only con­ tribute certain results that are used to direct the search of all agents. Due to the common new start state, there is no use of demand-based criteria for selecting results.

A truly heterogeneous search system was presented in [Hogg and Williams, 1993] for solving graph coloring problems. The system consisted of a tree-based search agent that heuristically constructed the possible color­ ings and a repair agent, that worked on inconsistent col­ orings in order to generate a consistent one. The agents communicate via a blackboard on which partial colorings (called hints) are written in random intervals . The t ree-based agent also randomly reads hints and chooses its node that fits to the hint to work on instead of the node its heurist ic would choose. Whenever the repair agent is stuck, it uses with a certain probability a hint to generate a new coloring instead of generating a ran­ dom one. Obviously, a knowledge-based selection using referees is not included in this approach.

In [Sutcliffe, 1992] a heterogeneous cooperation con­ cept for automated deduction was proposed. The central concept was a distributed implementation of a shared memory (a so-called tuple-space), in which each agent wrote all formulas generated by it. No selection pro­ cess was involved and no existing provers could be used . Therefore the experiments were not convincing.

6 Future Work

We have presented a cooperation methodology for exist­ ing search systems and we have demonstrated that this methodology yields significant improvements in the area of automated deduction. Besides testing the method­ ology for other areas of search (cooperation of genetic algorithms with branch and bound , for example), future work will also be directed to using other types of infor­ mation than clauses. These other types include selected negative results and various control information.

Negative results of an agent may be used by other agents to either avoid producing such results or to re­ move them from their search states. Control information can mostly be used by agents of the same type so as to improve their search focus or to avoid searching in the same parts of the search space. But also agents of dif­ ferent types may gain from certain control information.