PaInleSS: a Framework for Parallel SAT Solving

Authors

Ludovic Le Frioux, Souheib Baarir, Julien Sopena, Fabrice Kordon

Where

Proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing (SAT'17)

Type

inproceedings

Publisher

Springer, Cham

Keywords

parallel, satisfiability, clause sharing, portfolio, cube and conquer

Date

2017-06-30

Abstract

Over the last decade, parallel SAT solving has been widely studied from both theoretical and practical aspects. There are now numerous solvers that dier by parallelization strategies, programming languages, concurrent programminginvolved libraries, etc. Hence, comparing the eciency of the theoretical approaches is a challenging task. Moreoverthe introduction of a new approach needs either a deep understanding of the existing solvers, or to start from scratch the implementation of a new tool. We present PaInleSS: a framework to build parallel SAT solvers for many-core environments. Thanks to its genericity and modularity, it provides the implementation of basics for parallel SAT solving like clause exchanges, Portfolio and Divide-and-Conquer strategies. It also enables users to easily create their own parallel solvers based on new strategies. Our experiments show that our framework compares well with some of the best state-of-the-art solvers.

Documents

• Paper

Bibtex (lrde.bib)

@InProceedings{	  le-frioux.17.sat,
  author	= {Ludovic {Le Frioux} and Souheib Baarir and Julien Sopena
		  and Fabrice Kordon},
  title		= {{PaInleSS}: a Framework for Parallel {SAT} Solving},
  booktitle	= {Proceedings of the 20th International Conference on Theory
		  and Applications of Satisfiability Testing (SAT'17)},
  year		= 2017,
  month		= aug,
  pages		= {233--250},
  volume	= {10491},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer, Cham},
  abstract	= {Over the last decade, parallel SAT solving has been widely
		  studied from both theoretical and practical aspects. There
		  are now numerous solvers that dier by parallelization
		  strategies, programming languages, concurrent programming,
		  involved libraries, etc. Hence, comparing the eciency of
		  the theoretical approaches is a challenging task. Moreover,
		  the introduction of a new approach needs either a deep
		  understanding of the existing solvers, or to start from
		  scratch the implementation of a new tool. We present
		  PaInleSS: a framework to build parallel SAT solvers for
		  many-core environments. Thanks to its genericity and
		  modularity, it provides the implementation of basics for
		  parallel SAT solving like clause exchanges, Portfolio and
		  Divide-and-Conquer strategies. It also enables users to
		  easily create their own parallel solvers based on new
		  strategies. Our experiments show that our framework
		  compares well with some of the best state-of-the-art
		  solvers.},
  doi		= {FIXME}
}