Logo des Repositoriums

Auflistung nach Autor:in "Schubert, Tobias"

1 - 1 von 1
  • Konferenzbeitrag
    A distributed SAT solver for microcontroller
    (ARCS 2004 – Organic and pervasive computing, 2004) Schubert, Tobias; Becker, Bernd
    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.