Facta Univ. Ser.: Elec. Energ., vol. 20, No. 3, December 2007, pp. 395-414.

Set-Based SAT-Solving

Bernd Steinbach and Christian Posthoff

Abstract: The 3-SAT problem is one of the most important and interesting NP-complete problems with many applications in different areas. In several previous papers we showed the use of ternary vectors and set-theoretic considerations as well as binary codings and bit-parallel vector operations in order to solve this problem. Lists of orthogonal ternary vectors have been the main data structure, the intersection of ternary vectors (representing sets of binary solution candidates) was the most important set-theoretic operation. The parallelism of the solution process has been established on the register level, i.e. related to the existing hardware, by using a binary coding of the ternary vectors, and it was also possible to transfer the solution process to a hierarchy of processors working in parallel. This paper will show further improvements of the existing algorithms which are easy to understand and result in very efficient algorithms and implementations. Some examples will be presented that will show the recent results.

Keywords: SAT-problem, ternary vector, intersection, difference.

8psthoff.pdf