Concurrent-distributed programming techniques for SAT using DPLL-stålmarck

This paper reports our work on application of concurrent/distributed techniques to SAT. These were investigated using each of the following methods: the DPLL algorithm, the dilemma rule of the Stalmarck´s algorithm and a concurrent/distributed hybrid SAT solver: DPLL-Stalmarck, using a combination of the DPLL and the dilemma rule based algorithm. The prototypes have been implemented using Alice, an SML based language with support for distribution and concurrency. Our prototype framework allows for rapid-prototyping of and experimentation with application of various concurrent/distributed programming techniques to SAT. The emphasis is not on building an industry-standard SAT solver, but rather an investigation of the efficacy of use of these techniques for SAT at various levels of granularity.