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 in propositional logic on processor arrays with a reconfigurable bus system of size m × 2n, where m is the number of clauses and n is the number of Boolean variables. The theorem proving problem involves combinatorial exploration of an exponential search space. Our approach to the problem is simpler than using explicit inference rules, as the problem is vectorized and deductions are performed implicitly by simple AND and OR oprrations on vectors. The previous best parallel algorithm for the theorem proving problem available in the literature has a time complexity of O(m log2 n) using O(2n) processors. Thus, our algorithm is faster and further; costwise (time complexity × number of processors), it is efficient by a factor of log2 n. © 1995.