PICHAFF ² - A Hierarchical Parallel SAT Solver

We present a hierarchical distributed SAT procedure for microchip PIC microcontrollers. The algorithm is an adaption of the state-of-the-art solver CHAFF optimised for the limited resources of the microchip processors. The underlying hardware environment is a special multiprocessor system based on PC ISA slot cards, each of them holding up to 9 PIC microcontrollers. We propose a novel work stealing scheme, which is able to manage multiple of these multiprocessor cards in parallel. Besides discussing technical aspects we also point out the efficiency of our approach by a set of experiments