JaCk-SAT: A new parallel scheme to solve the satisfiability problem (SAT) based on join-and-check

Abstract

This paper presents and investigates for the first time a new trail for parallel solving of the Satisfiability problem based on a simple and efficient structural decomposition heuristic. A new J oining a nd model C hec k ing scheme (JaCk-SAT) is introduced. The main goal of this methodology is to recursively cut the variable-set in two subsets of about equal size. On the one hand, in contrast with recent propositions [12,16] for sequential resolution, we do not use sophisticated hypergraph decomposition techniques such as Tree Decomposition that are very likely infeasible. On the other hand, in contrast with all the actual propositions [27] for parallel resolution, we make use of a structural decomposition (of the problem) instead of a search space one. The very first preliminary results of this new approach are presented. © 2008 Springer-Verlag Berlin Heidelberg.