Schubert, TobiasBecker, BerndBrinkschulte, UweBecker, JürgenFey, DietmarGroßpietsch, Karl-ErwinHochberger, ChristianMaehle, ErikRunkler, Thomas A.2019-10-302019-10-3020043-88579-370-9https://dl.gi.de/handle/20.500.12116/29385In this paper we present a parallel prover for the propositional satisfiability problem called PICHAFF. The algorithm is an adaption of the state-of-the-art solver CHAFF optimised for our scalable, dynamically reconfigurable multiprocessor system based on Microchip PIC microcontroller. Like usually in modern SAT solvers it includes lazy clause evaluation, conflict-driven learning, non-chronological backtracking, and clause deletion. A simple but efficient technique called Dynamic Search Space Partitioning is used for dividing the search space into disjoint portions to be treated in parallel by up to 9 processors. Besides explaining of how such a complex algorithm could be implemented on simple microcontroller we also give experimental results demonstrating the potential of the implemented methods.enText/Conference Paper1617-5468