We present randoCoP, a theorem prover for classical firstorder logic, which integrates randomized search techniques into the connection prover leanCoP 2.0. By randomly reordering the axioms of the problem and the literals within its clausal form, the incomplete search variants of leanCoP 2.0 can be improved significantly. We introduce details of the implementation and present comprehensive practical results by comparing the performance of randoCoP with leanCoP and other theorem provers on the TPTP library and problems involving large theories.
Connection calculi, such as the connection calculus [
The downside of restricted backtracking is the loss of completeness. Whereas proofs for some formulae can be found very quickly, it might be impossible to find proofs for other formulae anymore. Since restricted backtracking cuts off alternative connections, the benefit of this approach strongly depends on the proof search order. The proof search order, in turn, usually depends on the order of clauses and literals in the given formula. Whereas the proof search procedure quickly finds a proof for one order, another order of the same clauses might result in an incomplete proof search order, i.e. no proof is found at all. By reordering the clauses, the downside of restricted backtracking can be minimized.
randoCoP extends the leanCoP 2.0 implementation by repeatedly reordering the axioms and literals of a given problem at random. This increases the chance to find a proof, in particular for the incomplete prover variants. In Section 2 we present experimental results of several reordering techniques and details of the implemented reordering strategy. In Section 3 the performance of randoCoP is compared with current state-of-the-art theorem provers.
We first describe the basic motivation behind the randomized reordering technique. Afterwards we present a detailed practical analysis, which determines the specific reordering strategy that is used within randoCoP. 2.1
Motivation leanCoP searches for connections in the order of the given input clauses. Connections to clauses at the beginning of the input clauses are considered first, before (on backtracking) clauses at the end are examined. Therefore reordering clauses is a simple way of modifying the proof search order. But the effect of reordering clauses is limited for complete search strategies (see Section 2.2), since every clause is considered sooner or later anyway.
leanCoP 2.0 has the option to restrict backtracking by cutting off alternative
connections in branches that have already been closed before [
The complete search strategy (left hand side), does not reach the proof depth required for a solution. The search with restricted backtracking (in the middle), reaches the depth of the solutions but not the required breadth. Only the search strategy with restricted backtracking and repeatedly reordering the clauses (right hand side) is able to find a proof.
Clauses can be reordered in several ways, e.g. by rotating or shifting clauses. leanCoP 2.0 already contains an option for reordering clauses that uses a simple perfect shuffle algorithm. But the effect on the proof search is small, since the generated clause orders are not sufficiently diverse. A random reordering mixes the order of clauses more thoroughly. Therefore instead of the built-in reordering technique a randomized reordering should be used. Since the outcome of the proof search needs to be reproducible, a deterministic pseudo-random reordering needs to be implemented. 2.2
Our practical experiments have shown that a reordering of the axioms of a given problem is more effective than the reordering of clauses after the clausal form translation has been applied. These experiments also showed that reordering the literals within the clauses has a positive effect on the proof search as well.
The proof search order is randomly modified in the following way. Let A1 ∧ A2 ∧ . . . An∧ ⇒ C be the given formula where A1, A2, . . . , An are the axioms and C is the conjecture of the problem. Let πm : {1, . . . , m} → {1, . . . , m} be a (pseudo-)random permutation. 1. Reordering of axioms: The following formula is generated: Aπn(1) ∧ Aπn(2) ∧ . . . ∧ Aπn(n) ⇒ C. Let C1, C2, . . . , Cm be this formula in clausal form. 2. Reordering of literals: For each clause Ci={L1, . . . , Lk} the reordered clause Ci0={Lπk(1), . . . , Lπk(k)} is generated. C10, . . . , Ck0 is the final set of clauses.
We first want to find the options of the leanCoP 2.0 core prover that are most
suited for our randomized reordering approach. A variant of the leanCoP 2.0
Prolog core prover is determined by a set of options that control the proof search
[
If none of these options is given the standard translation is used for the
axioms whereas the definitional translation is used for the conjecture [
The option conj is complete only for formulae with a provable conjecture, and the options scut and cut are only complete if used in combination with the option comp(I).
The following tests were performed on all 3644 non-clausal problems (FOF
division) of the TPTP library [
The prover variants using restricted backtracking (options cut and scut) benefit most from the randomized reordering technique. The greatest advance is made for the variant using the default clausal form translation and both of the options cut and scut. The variants using a full definitional (def) or the standard (nodef) clausal form translation and no restricted backtracking show a lower performance. The most successful variants using reordering use the options {cut}, {cut,scut}, {conj,cut}, and {conj,cut,scut}.
We have tested the most successful variants again using different time limits for each order of the axioms/literals. Table 2 shows the results using an overall time limit of 180 seconds and a time limit of 2 seconds, 3 seconds and 4 seconds for proving each order allowing around 90, 60 and 45 reorderings, respectively. The difference in the number of proved problems is rather small with a slight advantage for a time limit of 3 seconds.
Further evaluations have shown that the most number of problems are proved by repeatedly running the two variants {cut,scut} and {def,conj,cut} each for a time limit of 3 seconds and 2 seconds on each axiom/literal order, respectively.
In order to prove and refute a large number of problems within the first few seconds, the proof process is started by running the most successful complete prover variant using the options cut and comp(7) once for 5 seconds. A complete prover variant using the option def only is invoked at the end of the proof process for at least 10 seconds. 2.3
The Implementation randoCoP uses the random library of ECLiPSe Prolog, which contains the predicate rand_perm/2 that randomly permutes a list, and randomise/1 to seed and initialize the random generator, which allows the same sequence of permutations to be generated, and thus makes the result reproducible.
randoCoP consists of a shell script that calls the leanCoP 2.0 core prover extended by a few predicates realizing the reordering of axioms and literals. This shell script is called with an argument that determines the overall time limit and invokes the prover variants according to Section 2.2.
Let T otalT ime be this given time limit in seconds. Then the shell script invokes the following variants of the core prover in the following order: 1. Prover variant {cut,comp(7)} for 5 seconds 2. Repeated reordering step, (T otalT ime − 15)/5 times: (a) Reordering of axioms and literals (b) Prover variant {cut,scut} for 3 seconds (c) Prover variant {def,conj,cut} for 2 seconds 3. Prover variant {def} for 10 seconds
If, for example, T otalT ime is set to 600 seconds, then (600-15)/5=117 reordering steps are done and after each reordering the two prover variants are run for 3 seconds and 2 seconds, respectively. 3
To evaluate the performance we tested randoCoP on all non-clausal problems in the TPTP library, and the problems of the MPTP challenge. All tests were done on a system with a 3 GHz Xeon processor and 4 Gbyte of memory running Linux and ECLiPSe Prolog 5.8. We compare the performance of randoCoP with the current state-of-the-art provers. 3.1
For the tests all 3644 problems of version 3.3.0 of the TPTP library [
In Table 3 the performance of randoCoP is compared with the following
theorem provers: Otter 3.3 [
randoCoP proves more problems than Equinox, iProver, Prover9, leanCoP 2.0,
SNARK and Otter. It solves more problems in the SEU domain than any other
prover. The SEU domain contains problems from set theory taken from the
MPTP [
[%] 0s to 1s 1s to 10s 10s to 100s 100s to 600s rating 0.0 rating >0.0 rating 1.0 0.00...0.24 0.25...0.49 0.50...0.74 0.75...1.00
FNE FEQ PEQ AGT ALG CSR GEO GRA KRS LCL MED MGT NLP NUM PUZ SET SEU SWC SWV
SYN refuted time out gave up errors 3.2
The MPTP challenge is a set of problems from the Mizar library translated into
first-order logic [
The result of randoCoP on the bushy and chainy division is shown in Table 4 and Table 5, respectively. Again, equality axioms are added, which results in formulae with a total of up to 1700 axioms. The performance is compared with the theorem provers mentioned in Section 3.1. randoCoP shows a decent performance in both division. The time complexity is better compared to the other provers, as many problems are (still) proved after 10 seconds. We have not tested the provers MaLARea 0.1, SRASS 0.1, and Fampire 1.3, which prove 187/142, 171/127, and 191/126 of the problems in the bushy/chainy division, respectively (according to the MPTP challenge web site).
We have presented randoCoP, a theorem prover for classical first-order logic, which integrates a random proof search strategy into the connection prover leanCoP 2.0. Repeatedly reordering the axioms of the problem and the literals within its clausal form improves performance of leanCoP 2.0 significantly.
Some incomplete strategies of leanCoP 2.0 effectively restrict backtracking and increase the depth of the search space that can be investigated within a certain amount of time. But they might cut off specific proof search orders required to find a proof. randoCoP partly compensates for this disadvantage and the loss of completeness by increasing again the breadth of the explored search space. The combination of restricted backtracking and randomized reordering is highly effective, in particular for hard problems containing many axioms.
The core prover of randoCoP and leanCoP 2.0 consists only of a few lines of Prolog code. This indicates that tens to hundreds of thousands of lines in, e.g., C and low-level optimizations are not needed to succeed in automated theorem proving. Instead it shows that good heuristics for traversing the vast search are important in automated reasoning research.
The RCTHEO system [
The SETHEO system offers a dynamic subgoal reordering option. The reordering is not at random but prefers subgoals with the highest probability to fail, in order to reduce the search space. Syntactic criteria, such as the number of variables, are used to determine the specific order. The subgoal order is then determined dynamically whenever the next subgoal is selected.
We have tested SETHEO without and with subgoal reordering on all nonclausal problems of the TPTP library (see Section 3.1). Without subgoal reordering SETHEO proves 1192 out of the 3644 problems. With subgoal reordering (using the option -dynsgreord 2) it only solves 1185 problems, i.e. the performance does not really improve. This confirms our own testing with reordering on several variants of the leanCoP 2.0 core prover (see Section 2.2). The effect of reordering axioms (or clauses) and literals is limited when a complete search in connection calculi is done. In this case the performance can even get worse. On the other hand the incomplete variants of the leanCoP 2.0 core prover benefit significantly from the randomized reordering technique.
Further research includes the adaption of randoCoP to other (non-classical)
logics — such as intuitionistic logic [
The source code of randoCoP can be obtained at the leanCoP website at http://www.leancop.de. Acknowledgements. The authors would like to thank the referees for their useful comments, which have helped to improve this paper.