THE SOLUTION OF DISCRETE CONSTRAINT PROBLEMS USING BOOLEAN MODELS The Use of Ternary Vectors for Parallel SAT-Solving

The use of Boolean models for discrete constraint problems has been tried at several occasions, it was, however, not recognized as efficient (Rossi et al., 2006). The solution methods were dominated by using decision trees together with depth-first or breadth-first search and/or resolution algorithms. In this paper we will show the use of ternary vectors for the solution of SAT-problems and all the problems that can be modeled by means of SAT-equations. They are an appropriate data structure representing sets of Boolean vectors. They also allow to include problem-relevant knowledge into the problem-solving process at an early point of time. The respective set operations (mainly the intersection) can be executed in a bit-parallel way (64 bits at present). For larger problems the processing can be transferred to processors working fully in parallel. There is no need for any search algorithms. The approach always finds all solutions of the problem without consideration of special cases (i.e. no solution, one solution, all solutions). Some examples are used to illustrate the approach or have been published before (Sudoku, Queen's problems on the chessboard, node bases in graphs, graph-coloring problems).