Abstract

Traditional approaches to solving satisfiability problems have been centered on assigning values to one variable at a time and simplifying the expression. This paper shows an effective algorithm which takes advantage of the parallel nature of bit processing at the register level of computers, in order to process all of the boolean variables in a satisfiability formula simultaneously. This inherent parallelism is used to intersect known solution sets from different clauses of the formula. If there exists a non-empty intersection of solution sets from each clause, then the formula is shown to be satisfiable.