Edinburgh Research Explorer

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Original languageEnglish
Title of host publicationHigh Performance Computing Simulation, 2009. HPCS'09. International Conference on
PublisherIEEE
Pages168-175
Number of pages8
ISBN (Print)978-1-4244-4906-4
DOIs
StatePublished - 2009

Abstract

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.

ID: 23595135