Distributed Parallel SAT Checking with Dynamic Learning using DOTS
Wolfgang Blochinger, Carsten Sinz · 2001
We present a novel method for distributed parallel au-tomatic theorem proving. Our approach uses a dynam-ically learning parallel SAT checker incorporating dis-tributed multi-threading and mobile agents. Individual threads process dynamically created subproblems, while agents collect and distribute new knowledge created by the learning process. As parallelization platform we use the Distributed Object-Oriented Threads System (DOTS) that provides support for both distributed threads and mo-bile agents. We present experiments indicating the useful-ness of the presented approach for different application do-mains.