摘要

Suppose that we are given a vector consisting of only 1's and 0's and we are interested in finding some special properties of this vector. For instance, we like to determine whether all of the bits from location s to location e in the vector are all 1's or whether there exists a 1 from location s to location e. In more complicated cases, we are given two bit-vectors and we like to investigate the mutual properties between the two vectors. For instance, we want to find all locations i in vector B such that there exists a k in vector A, k <= i, such that A(k) = 1 and in vector B, locations from k to i all assume value 1. These problems all involve 'for-all' or 'there-exists' notations and can of course be solved by sequential programs. In this paper, we are interested in bit-parallel process to solve these problems. That is, we are interested in solving the problem efficiently by using 'bitwise-and', 'bitwise-or' and other bitwise logical operations. A sequence of logical operations can be expressed as a logical formula. This paper proposes a systematical method to find such logical formulas to solve problems involving bit-vectors with 'for-all' and 'there-exists' notations. Five logical prototype problems, named 'single-for-all' (1's), 'single-there-exists', 'multiple-for-all', 'multiple-there-exists' and 'multiple-there-exists-and-for-all', are defined in this paper. For each problem, we show that there exists a corresponding logical formula that can be computed using bit-parallel operations in O(n/w) time, where w is the word size of the machine. We also propose four variants for these five problems, and show that their logical formulas can be obtained using those of the five prototype problems.

全文