A CONSTANT-TIME ALGORITHM FOR THEOREM-PROVING IN PROPOSITIONAL LOGIC ON RECONFIGURABLE MESHES

In this paper, we present an O(1) time algorithm for theorem proving i n propositional logic on processor arrays with a reconfigurable bus sy stem of size m x 2(n), where m is the number of clauses and n is the n umber of Boolean variables. The theorem proving problem involves combi natorial exploration of an exponential search space. Our approach to t he problem is simpler than using explicit inference rules, as the prob lem is vectorized and deductions are performed implicitly by simple AN D and OR operations on vectors. The previous best parallel algorithm f or the theorem proving problem available in the literature has a time complexity of O(mlog(2)n) using O(2(n)) processors. Thus, our algorith m is faster and further; costwise (time complexity x number of process ors), it is efficient by a factor of log(2)n.