Copyright © 2011 American Scientific Publishers Advanced Science Letters

All rights reserved Vol. 4, 400–407, 2011

Printed in the United States of America

The Parallel Theorem Proving Algorithm

Based on Semi-Extension Rule

Liming Zhang1,2, Dantong Ouyang1,2, Jian Zhao1,2 and Hongtao Bai1,2

1School of Computer Science and Technology, Jilin University, Changchun 130012, China

2Key Laboratory of Symbolic Computation and Knowledge Engineering of Ministry of Education,

Jilin University, Changchun 130012, China

After a deep investigation on the maximum terms space of the clause set, the concept of the partial maximum terms space of the clause set, which the maximum terms of the clause set decomposed, is brought forward. By investigating the extension rule, this paper introduces the concept of the satisfiability and the unsatisfiability of the partial maximum terms space, and gives an algorithm determining the satisfiability of a partial space of the maximum terms - algorithm PSER (Partial Semi-Extension Rule). Then, the TP problem is decomposed into several sub-problems independent of each other, which can be solved by the given parallel computing method PPSER (Parallel Partial Semi-Extension Rule).

Keywords: Theorem Proving, Parallel Algoritm, Extension Rule.

1. INTRODUCTION

The classical NP-complete problem of TP has seen much interest in not just the theoretical computer science community, but also in areas where practical solutions to this problem which enable significant practical applications1. However, NP-Completeness does not exclude the possibility of finding algorithms that are efficient enough for solving many interesting satisfiability instances. These instances arise from many diverse areas - many practical problems in AI planning2-5, circuit testing6,7 and verification8-10 for instance.

This research has resulted in the development of several TP algorithms that have seen practical success. These algorithms are based on various principles such as Resolution11,12, Search13, Binary Decision Diagrams14, and Extension rules15.

Extension-rule based TP method has commended considerable respect from many related researchers. For the generation of the target language based on the knowledge compilation, and achieved good results.

*Email Address: limingzhang@jlu.edu.cn

Besides, many researchers applied the extension rule to the model counting problem18, and many amended it so as to applied it into the TP of modal logic19 .Still some researchers improved the extension rule, and put forward series of algorithms such as NER, RIER, etc20,21.

Extension-rule based TP method has commended considerable respect from many related researchers. For example, Murray16,17 has applied the extension rule into

the generation of the target language based on the knowledge compilation, and achieved good results. Besides, many researchers applied the extension rule to the model counting problem18, and many amended it so as to applied it into the TP of modal logic19 .Still some researchers improved the extension rule, and put forward series of algorithms such as NER, RIER, etc20,21.

This paper is organized as follows. In section 2, the related extension-rule based TP methods are given. In section 3, the parallel TP method based on the Semi-extension rule is presented. The experimental results of comparing the algorithm proposed in this paper with other algorithms are also presented in section 4. Finally, our work of this paper is summarized in the last section.

2. EXTENSION-RULE BASED THEOREM PROVING METHOD

We begin by specifying the notation that will be used in the rest of this paper. We use Ψ to denote a set of clauses in conjunctive normal form (CNF), C to denote a single clause, and M to denote the set of all the atoms that appear inΨ. The extension rule is defined as follows.

DEFINITION 115.Given a clause C, C∈Ψ , D ={ CA, CA | “A” is an atom, A∈M, “A” and “A” does not appear in C}, we call the deduction process proceeding from C to D the extension rule of on C, and call D the result of applying the extension rule of on C.

THEOREM 115.A clause C is logically equivalent to the result of the extension rule D.

This theorem ensured the equivalence between the original clause set and the expanded clause set, thus extension rule can be regarded as an inference rule.

DEFINITION 222.A non-tautology clause is a maximum term on a set M iff it contains all the atoms in M in either positive form or negative form.

THEOREM 215.Given a set of clauses Ψ, let M be the set of all the atoms in it (|M|= m). If all the clauses in Ψ are maximum terms on M, then the clause set Ψ is unsatisfiable iff it contains 2m clauses.

Apparently the set of all the maximum terms consist of m atoms is surely contains 2m maximum terms. Therefore, it is only need to compute the number of distinct maximum terms can be deduced from the clause set that we can determine its satisfiability. In addition, when counting the number of the maximum terms that can be deduced from the clause set, we can use the inclusion-exclusion principle presented below.

THEOREM 322.(Inclusion–exclusion principle) The element number of the union of sets of set A1, A2,…, An can be compute using the formula below:

A1∪A2∪…∪An… -1n+1A1A2…An.

THEOREM 415.The intersection of the sets that consist of the maximum terms expanded by two clauses respectively will be empty iff these two clauses contain complementary literals.

Given a set of clauses ΨC1, C2, … , Cn, let M be the set of atoms that appear in it (|M|= m).Let Pi be the sets of all the maximum terms we can get from Ci by using the extension rule, and let S be the number of distinct maximum terms we can get from Ψ. By using the extension rule, we will have SP1∪P2 ∪…∪Pn.

3. PARALLEL PROVING ALGORITHM BASED ON SEMI-EXTENSION RULE

The idea of the paralleled semi-extension rule based algorithm is as follows. Firstly, the algorithm decomposes the maximum terms space of the clause set into several partial maximum terms spaces, which convert the SAT problem of the clause set into the SAT problem of the partial maximum terms spaces. If there is a certain partial maximum terms space that is satisfiable, then the clause set is satisfiable. If all the partial maximum terms spaces are unsatisfiable, then the clause set is unsatisfiable. In other words, the clause set is satisfiable. In the following, the concept of the partial maximum terms space will be given.

DEFINITION 3. For the set M={L1,L2,…Lm}, the 2m maximum terms corresponding to M is {L1∨L2∨…∨Lm-1∨Lm, L1∨L2∨…∨Lm-1∨Lm,…,L1∨L2∨…∨Lm-1∨Lm, L1∨L2∨…∨Lm}, and we number each maximum term as mi(0),mi(1),…,mi(2m-2),mi(2m-1).

DEFINITION 4.Given a clause set ΨC1, C2,…,Cn, let M be the set of its literals, andMm. We call maximum terms space of M as MI(M). Assuming that 1≤2k≤2m,if we would like to decompose the maximum terms space into 2k spaces, then each space is of this form MIS(j)={mi(j)|j∈{ mi(2m×(j-1)/ 2k), mi(2m×(j-1)/2k+1),…, mi(2m×(j)/ 2k-1)}}, 1≤j≤2k .

DEFINITION 5. For the partial maximum terms space MIS(j), 1≤j≤2k≤2m. If all the maximum terms in it can be expanded by the clauses of the clause set, then MIS(j) is said to be unsatisfiable. If there exist a certain maximum term that cannot be expanded by any clause of the clause set, then MIS(j) is said to be satisfiable.

THEOREM 5.If every partial maximum terms space is unsatisfiable, then the clause set is unsatisfiable. If there is a certain partial maximum terms space that is satisfiable, then the clause set is satisfiable.

In the following, the algorithm PSER which determines the satisfiability of the partial maximum terms space will be given

DEFINITION 6. M={L1,L2,…,Lm},m=|M|. Let clause C= Li∨…∨Lj…∨Ld, 1≤i≤j≤d≤m, which d is referred as the degree of clause C. Ψ={CLk, CLk|d<k≤m }, we call the operation proceeding from C to the elements of Ψ the semi-extension rule, and the elements of Ψ the result of the semi-extension rule.

PROPOSITON 1.According to definition 6, when applying the semi-extension rule on C, the remaining m-d atoms could be positive or negative, therefore C can semi-expand 2m-d clauses.

PROPOSITION 2.Let d1 and d2 be the degrees of clause C1 and C2 respectively, while d1<d2 and C1C2. According to proposition 1, the clause that C1 or C2 can semi-expand is obtained by compose the m-d1 atoms or m-d2 atoms in positive form or in negative form. Therefore, clauses that C2 can semi-expand are a subset of the clauses that C1 can expand.

According to proposition 2, when determining whether the maximum terms clause can be expanded by the clauses, we should determine whether it can be expanded by the clauses of smaller degree first. In the following, the algorithm determining the satisfiability of the partial maximum terms space will be given.

In the following, the related theorem and algorithm of Expand will be given.

THEOREM 621.Given a clause setΨ={C1,C2,…,Cn}, Let M be the set of its literals, and |M|=m. A maximum term T=L1∨L2∨…∨Lm on M can be expanded by clause C= Li∨…∨Lj…∨Ld, 1≤i≤j≤d≤m, iff { Li,…,Lj,…,Ld } {L1,L2,…,Lm}.

In the above, we gave the solving method of partial maximum terms space and the algorithm determining its satisfiability. The maximum terms space of a clause set can be decomposed into several partial maximum terms spaces. In doing so, the SAT problem of a clause set is converted into the SAT problems of several partial maximum terms spaces. If there is a partial maximum terms space that cannot be expanded, then the clause set is satisfiable. Or else, if all the partial maximum terms space is unsatisfiable, then the clause set is unsatisfiable. In the following, the parallel TP algorithm based on semi-extension rule will be given.

The concrete flow of the algorithm is as follows: The parent process distributes Threadnum sub-threads, and then these sub-threads are arranged to many cores of the processor by the Operating System, respectively. Each sub-thread calls the function PSER, and records the corresponding returned results using Result[j], while the parent process monitors running result of each sub-thread. If there is a sub-thread that its Result[j] is SAT, then the algorithm returns SAT. If the Result[j] of every sub-thread is UNSAT, then the algorithm returns UNSAT.

4 EXPERIMENTAL RESULT

On the basis of literature 21, in this section, we compare our algorithm PPSER with algorithm NER, algorithm IER and Directional Resolution algorithm 12 proposed by Dechter and et al, respectively. The experiments are carried out on a Dell Dimension C521, AMD Athlon(tm) 64 X2 Dual Core Processor 3600+, 1.9GHz 1022MB RAM with Windows XP. This experiment uses Uniform Random-3-SAT benchmark 23 lays on phase change zone and standard test cases of frb 24 as test cases. For the entire 1000 issues of uf20-90, table 1 only shows the experimental results of 10 issues randomly selected. The first column of the table shows the sample name, the latter 3 columns shows the runtime of three algorithms corresponding to each issue which the unit of data is Seconds (s). For each test case, we will test 10 times and take the mean value as the experimental results. As we can see from the test, our algorithm PPSER has a significant advantage on efficiency compared with the original algorithm, which is 8-20 times higher than the relatively fast algorithm NER.

Table.1. Experimental Results of Uniform Random-3-SAT Benchmark Instances.

First, we select instances, which the parameters are <N,20,10> and <N, 30,10> respectively, for testing, where the parameter N is restricted as 60 ≤ N ≤ 160. For each instance of different difficulty levels, they will randomly generate 10 samples for solving, and let the mean value as the final result. The experimental result is in Figure 1 and Figure 2.

Fig.1. <N, 20, 10>

Fig.2. <N, 20, 10>

By testing the Random SAT problems, we can see from figure 1 and figure 2, that our algorithm PPSER has an obvious advantage on efficiency, which is 6-15 times higher than the relatively fast algorithm NER. Moreover, when the number of clauses increased to 130 above, the computing time of our algorithm PPSER is increased gently.

5. CONCLUSIONS

This method decompose the maximum terms space of the clause set into several partial maximum terms spaces, and determines the satisfiability of each partial maximum terms space. If all the partial maximum terms space are unsatisfiable, the clause set is unsatisfiable. Or else, if there is a certain partial maximum terms space that is satisfiable, then the clause set is satisfiable. Besides, when determining the satisfiability of the partial maximum terms space, if we found that a maximum term can be expanded by a certain clause, then all the maximum terms semi-expanded based on this clause have no need to determine their expandability, thus effectively reduced the number of the maximum terms to be determined. The experiment results show that our algorithm PPSER has a reasonable execution efficiency, which is superior to algorithm NER, DR, IER and et al.

ACKNOWLEDGMENTS

This work was supported in part by NSFC under Grant Nos. 60973089.

REFERENCES

[1] Massart Thierry, Meuter Cedric, V B Laurent. On the complexity of partial order trace model checking, Inform. Process. Lett. 106 (2008) 120-126

[2] M. Davis, H. Putnam. A computing procedure for quantification theory. Journal of ACM, 7(3)(1960) 201-215.

[3] Dechter R, Rish I. Directional resolution: the davis-putnam procedure. Proceeding of 4th International Conference on Principles of KR&R, Bonn, Germany: Morgan Kaufmann, (1994) 134-145.

[4] M. Davis, G. Logemann, D. Loveland, A machine program for theorem proving. Communications of the ACM, 5 (1962) 394-397.

[5] R. E. Bryant. Graph-based algorithms for boolean function manipulation , IEEE Transactions on Computers, 35 (1986) 677-691.

[6] H Lin, JG Sun, YM Zhang. Theorem proving based on the extension rule, Journal of Automated Reasoning, 31 (2003) 11-21.

[7] K Xu, F Boussemart, F Hemery, C Lecoutre. Random constraint satisfaction: easy generation of hard (satisfiable) instances , Artificial Intelligence, 171 (2007) 514-534.

Received: 1 July 2011. Accepted: 15 August 2011

Advanced Science Letters 论文模板