3.2.1. The process of separating SC

Unlike a traditional binary resolution, the CS rule is essentially a dynamic, multi-clauses deduction rule. It should be noted that the contradiction separation clause C+ is not only the result of two clause resolutions but also the cooperative deduction result of multi-clauses in the P.

The SC is separated from multi-clauses in the P. Intuitively, the deductive based on S-CS Rule is the process of obtaining C+ by separating contradictions from P until C+ is empty.

According to Definition 2.1, the contradiction is a cartesian set. The core of applying the S-CS rule is effectively separating CS from multi-clauses to obtain the contradiction separation clause C+.

Thus, we propose a method to obtain C+ quickly. We assume the processed clause set P=C1,C2,…,Cm, and the literals in each clause are divided into two parts. That is, Ciσi=Ciσi+,Ciσi−, (σi is a substitution to C_i). What's more, C⁺ = C1σ1+,…,Cmσm+, C⁻ = C1σ1−,…,Cmσm−. The process is as follows:

Step 1. Obtaining given-clause C_g = l1,…,ln from U according to clause selection strategy. Putting all literal into Cg+, then Cg+=l1,…,ln and Cg−=∅.

Step 2. Find a substitute σi make σilili∈Cg+ and ~σiljlj∈C− be a complementary pair. Then, removing σili from Cgσi+_.

Step 3. If Cgσi+ is empty, canceling all substitutions and returning to step 1.

Step 4. Finding a substitute σi to make σilili∈Cg+, and~σilklk∈C kσk+ and C kσk−=∅ be a complementary pair. Then, moving the ~σilk from C kσk+ to C kσk− and removing σili from Cgσi+_.

Step 5. Repeating Step2 until no substitute σi is found.

Step 6. Putting Cgσ+ into C⁺.

The pseudo-code in Figure 2 is correspond to the above process of build SC, when C_g added to P, we can obtain a new contradiction separation clause C⁺ in the deduction. This process is dynamic. Finally, C⁺ is the result of multi-clauses cooperating.

Figure 2

The pseudo-code for Bulid standard constradiction algorithm.

In the above process, there will be some cases of given-clause C_g:

1. All literals need to be removed from Cgσi+

   1. Because they are complementary to ~σiljlj∈C−(Step 3). We think this inference is invalid because C_g has no direct effect on obtaining the C⁺ (no increase, no decrease).

   2. Because they are complementary to ~σilklk∈C kσk+ and C kσk−=∅ (Step 4). This case will be discussed in Section 3.2.2.

2. No literal is removed from C_g.

   No newly generated CS and C_g remain in P.

3. Some literals are removed from Cgσi+.

   It is the most common case, which means that the S-CS rule is successfully applied with C_g so that the new C⁺ can be obtained.

3.2.2. Restart

The technology for finishing the current CS construction process and starting a new deduction process is called the restart. Employing some restart strategies can avoid falling into a local search.

1. Restarting when all literals are removed from C_g in Step 4.

   Obviously, in this case, the number of words in the C⁺ is the least. Thus, by removing some literals from C⁺ without adding new ones in it, we can restore all substitution (rollback) and put the C_g back to U.

2. Restarting when the clause cannot be selected from U.

In this case, either set U is empty, or each clause in U participating in the deduction is invalid.

Note that we say a clause is invalid has two situations: the case i) and some constraints are not met. For example, the maximum number of literals in C⁺ is 2, but when some given-clauses participate in deduction, this limit is exceeded.

The restart process is as follows:

1. Adding all clauses in P to U and clearing the set p.

2. Simplifying set U and removing redundant clauses.

3. Selecting clause C_g from U again and putting it into P according to the selection strategy to start a new round of deduction.

3.3.1. Heuristic strategy based on S-CS rule

The traditional binary resolution based on saturate employs various heuristic strategies. These strategies usually come from two considerations:

1. Controlling the expansion of the proof-search space as much as possible to avoid too fast expansion of the clause set. However, such control is limited. In most cases, it is difficult to avoid the rapid expansion of the search space because the decision time increases.

2. Based on the goal-oriented strategy, employing the conjecture clause is preferred in the resolution process. It is a rough heuristic strategy, so the conjecture-clause participation in resolution will generate a large number of lemma clauses. Therefore, most of ATPs will generally combine the goal clause with the minimum age of the hybrid strategy.

Compared with the binary resolution method, the deduction method based on the S-CS rule comes with an outstanding feature: If and only if the contradiction separation clause C⁺ is empty, the clause set S is UNSAT. Therefore, for the heuristic strategy based on S-CS rule, the following two rules are followed:

• Rule 1: The literals in the contradiction separation clause C⁺ is as little as possible.

• Rule 2: The effect of unification/substitution on literals in C− is as small as possible.

For rule 1, there are two meanings. The first is to make the most use of the unit clause. The priority to use the unit clause must satisfy rule 1. Secondly, make full use of the coordination of multi-clause when there are more than two clauses in P. The more synergized effectors of all clauses are involved, the more literals will be removed from given-clause C_g.

For rule 2, the literal P(x) has better synergy than literal P(a). So we do not want the literal instanced too early, which will be discussed in Section 3.4.

Compared with the traditional binary resolution, the above two rules make the heuristic strategy based on the S-CS rule pay more attention to dynamic control of the deductive process, as well as are comfortable to be implemented.

3.3.2. Clause selection

Clause selection is the most crucial choice point of resolution-based provers [5]. The VAMPIRE prover was the CASC (Conference on Automated Deduction ATP System Competition) winner in recent years, which uses two parameters for clause selection: the age and the weight of a clause [12]. Another powerful purely equational theorem prover E prover uses some heuristic strategiesy [5]: first-in/first-out FIFO, symbols count, and goal-directed evaluation function. GKC [15] is a fresh resolution prover, which uses a 2-layer clause selection queues algorithm. The first layer uses the common ratio-based algorithm. Further, the second layer uses four separate queues based on the clause's age.

In the ATP based on the S-CS rule, we perform the selection of a given clause by employing a dynamic-static combined strategy to satisfy the above rules, as has been proposed in Section 3.3.1.

Our clause selection strategy based on S-CS rule as follows:

1. Static clause selection strategy

   1. Selecting clauses from one of the queues by Least literals priority.

   2. Selecting clauses from one of the queues by employing a stability-weight ratio. That will be discussed in Section 3.4.

2. Dynamic clause selection strategy

   Unlike the binary resolution, the dynamic strategy is one of the significant advantages of S-CS rule. The core idea is to guide the entire deduction process by the control strategy of the contradiction separation clause C⁺.

   1. Dynamic strategy for controlling the number of literals in C⁺

      Each deduction based on the S-CS rule will generate a C⁺. In order to make the literals in C⁺ be as little as possible, we set a threshold N_r. Let |C⁺| denote the number of literals in C⁺. If |C⁺| > N, contradiction separation fails, i.e., this inference is invalid. Rollback and put the C_g back to U, reselect given clause.

      Setting the threshold N is also a dynamic learning process. For example, with an initial value N = 1, when all the given-clause C_g from U are invalid, then N = N + 1;

   2. Least |C⁺| priority strategy

      The dynamic strategy is different from the static strategy. When N > 1 and there are some candidate clauses C₁, …, C_m with the same number of literals. We can try to inference with them separately, so the clause with the smallest |Ci+|,(i∈m) is preferred. Due to trying each candidate clauses, the deduction efficiency is affected. In practice, the candidate clause with more complementary predicates in the C− is preferred.

   3. Older clause or goal clause priority strategy

      Firstly, the older clause needs to be chosen; the two clauses are of the same age, choosing the goal clause or the descendants of the goal clause.

3.4.1. Weight function based on term stability

In the unification and substitution process, the variable in first-order logic probably replaces other variables and constants. Term stability is applied to evaluate how easy it is for a term to substitute for another term during the inference process, which reflects the complexity of the term's substitution. Thus we the term f(x) is more stable than x, and ground term f(a), a is the most stable.

3.4.2. Literal selection

During the S-CS building process, it needs to find a substitute σi that makes σili{li∈Cg+} and ~σilj{lj∈C− or lj∈C+} a complementary pair. It is known that different substitution sequences lead to different results. For example, there is a set C− in P and a given clause.

C−:{~P3(x₁, x₂, x₃), ~P2(x₁, x₂), ~Q2(x₁, x₃)}. If we prefer literal P3(a₁, a₂, a₃), we will obtain a substitution σ1:{a₁/x₁, a₂/x₂, a₃/x₃}. Obviously, there is no complementary pair in C− for the literals P2(x₁₁, a₁), Q2(x₁₂, a₁). They will be added into the C⁺. But if we find σ for literal P2(x₁₁, a₁), at first. Then only literal P3(a₁, a₂, a₃) is retained. In other words, literal selection strategies directly affect ATP performance.

Actually, we hope that literal selection strategies can achieve the following effects:

1. Keeping the literals as few as possible in C_g

2. Avoiding literal instance in C−, if possible, in the deduction process. To has the minimum influence on the C− after the unification.

   Therefore, we employ some literal-selection strategies as follows:

   1. Literal-stability priority queues.

      It gives higher priority to literal with smaller S(l).

   2. Literal-relational priority queues.

      It gives higher priority to literal with smaller R(l).

   3. Dynamic information for literal priority queues.

      The dynamic weight function is: d(l)=usel+αfi,α>1 where usel indicates the actual usage count of literal l, f_i denotes the statistics on the number of failures of the l in the inference process. It gives higher priority to literal with smaller d(l).

3.4.3. Other dynamic restriction strategies

According to the limitation of computing resources, such as CPU time, memory size, and storage space，we give the dynamic restriction strategies based on the S-CS rule.

The main idea is to set some thresholds, initially small values. When some property of a new clause exceeds these thresholds, discard this new clause. If the S-CS rule fails and the proof-search restart, these thresholds are increased.

These limits are as follows:

• Limit the maximum function layer of clause.

  At first, we count the maximum function nesting layer of the original clause, let flimit=fmax/2,fmax. The proof-search begin of the limit f_limit, if maximum funcion nesting layer of C⁺ exceeds f_limit, it is discarded. If the S-CS proof-search fails, flimit=flimit+1.

• Limit the maximum size of clause.

  As same, count the maximum length of clause in S, let |C|_{limit =} [1, |C|_max]. If |C⁺| > |C⁺|_limit, the C⁺ is discarded