Gesellschaft für Informatik e.V.

Lecture Notes in Informatics

ARCS 2004 - Organic and Pervasive Computing, Workshops Proceedings, March 26, 2004, Augsburg, Germany. P-41, 338-347 (2004).

GI, Gesellschaft für Informatik, Bonn


Uwe Brinkschulte (ed.), Jürgen Becker (ed.), Dietmar Fey (ed.), Karl-Erwin Großpietsch (ed.), Christian Hochberger (ed.), Erik Maehle (ed.), Thomas A. Runkler (ed.)

Copyright © GI, Gesellschaft für Informatik, Bonn


A distributed SAT solver for microcontroller

Tobias Schubert and Bernd Becker


In 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.

Full Text: PDF

GI, Gesellschaft für Informatik, Bonn
ISBN 3-88579-370-9

Last changed 04.10.2013 18:00:34