The Solution of SAT Problems Using Ternary Vectors and Parallel Processing

This paper will show a new approach to the solution of SAT-problems. It has been based on the isomorphism between the Boolean algebras of finite sets and the Boolean algebras of logic functions depending on a finite number of binary variables. Ternary vectors are the main data structure representing sets of Boolean vectors. The respective set operations (mainly the complement and the intersection) can be executed in a bit-parallel way (64 bits at present), but additionally also on different processors working in parallel. Even a hierarchy of processors, a small set of processor cores of a single CPU, and the huge number of cores of the GPU has been taken into consideration. There is no need for any search algorithms. The approach always finds all solutions of the problem without consideration of special cases (such us no solution, one solution, all solutions). It also allows to include problem-relevant knowledge into the problem-solving process at an early point of time. Very often it is possible to use ternary vectors directly for the modeling of a problem. Some examples are used to illustrate the efficiency of this approach (Sudoku, Queen's problems on the chessboard, node bases in graphs, graph-coloring problems, Hamiltonian and Eulerian paths etc.).