You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

PMSat: a parallel version of MiniSAT

Article type: Research Article

Authors: Gil, Luísa | Flores, Paulob | Silveira, Luís Miguelc

Affiliations: [a] Instituto Superior Técnico, Technical University of Lisbon, Portugal. E-mail: luis.filipe.gil@gmail.com | [b] INESC ID / Instituto Superior Técnico, Technical University of Lisbon, Portugal. E-mail: pff@inesc-id.pt | [c] Cadence Research Laboratories, INESC ID / Instituto Superior Técnico, Technical University of Lisbon, Portugal. E-mail: lms@inesc-id.pt

Keywords: parallel computing, SAT-solver, satisfiability, message passing interface

DOI: 10.3233/SAT190063

Journal: Journal on Satisfiability, Boolean Modeling and Computation, vol. 6, no. 1-3, pp. 71-98, 2010

Received 1 December 2007
|
Revision received 1 August 2008
|
Published: 1 November 2008
Get PDF open access

Abstract

Parallel computing has become an affordable reality forcing a shift in the programming paradigm from sequential to concurrent applications, specially those who demand much computational power or with large search spaces like SAT-solvers. In this context we present the research, planning and implementation of PMSat: a parallel version of MiniSAT with MPI (Message Passing Interface) technology, to be executed in clusters or grids of computers. The main features of the program are described: search modes, search space pruning and share of learnt clauses. An analysis of its performance and load balance is also presented.

Show more