Towards more efficient parallel SAT solving

From LRDE

Abstract

Boolean SATisfiability has been used successfully in many applicative contexts. This is due to the capability of modern SAT solvers to solve complex problems involving millions of variables. Most SAT solvers have long been sequential and based on the CDCL algorithm. The emergence of many-core machines opens new possibilities in this domain. There are numerous parallel SAT solvers that differ by their strategies, programming languages, etc. Hencecomparing the efficiency of the theoretical approaches in a fair way is a challenging task. Moreover, the introduction of a new approach needs a deep understanding of the existing solvers' implementations. We present Painless: a framework to build parallel SAT solvers for many-core environments. Thanks to its genericness and modularity, it provides the implementation of basics for parallel SAT solving. It also enables users to easily create their parallel solvers based on new strategies. Painless allowed to build and test existing strategies by using different chunk of solutions present in the literature. We were able to easily mimic the behaviour of three state-of-the-art solvers by factorising many parts of their implementations. The efficiency of Painless was highlighted as these implementations are at least efficient as the original ones. Moreover, one of our solvers won the SAT Competition'18. Going further, Painless enabled to conduct fair experiments in the context of divide-and-conquer solvers, and allowed us to highlight original compositions of strategies performing better than already known ones. Also, we were able to create and test new original strategies exploiting the modular structure of SAT instances.

Documents

Bibtex (lrde.bib)

@PhDThesis{	  le-frioux.19.phd,
  author	= {Ludovic {Le Frioux}},
  title		= {Towards more efficient parallel SAT solving},
  school	= {Sorbonne Universit\'e},
  year		= 2019,
  address	= {Paris, France},
  month		= jul,
  abstract	= {Boolean SATisfiability has been used successfully in many
		  applicative contexts. This is due to the capability of
		  modern SAT solvers to solve complex problems involving
		  millions of variables. Most SAT solvers have long been
		  sequential and based on the CDCL algorithm. The emergence
		  of many-core machines opens new possibilities in this
		  domain. There are numerous parallel SAT solvers that differ
		  by their strategies, programming languages, etc. Hence,
		  comparing the efficiency of the theoretical approaches in a
		  fair way is a challenging task. Moreover, the introduction
		  of a new approach needs a deep understanding of the
		  existing solvers' implementations. We present Painless: a
		  framework to build parallel SAT solvers for many-core
		  environments. Thanks to its genericness and modularity, it
		  provides the implementation of basics for parallel SAT
		  solving. It also enables users to easily create their
		  parallel solvers based on new strategies. Painless allowed
		  to build and test existing strategies by using different
		  chunk of solutions present in the literature. We were able
		  to easily mimic the behaviour of three state-of-the-art
		  solvers by factorising many parts of their implementations.
		  The efficiency of Painless was highlighted as these
		  implementations are at least efficient as the original
		  ones. Moreover, one of our solvers won the SAT
		  Competition'18. Going further, Painless enabled to conduct
		  fair experiments in the context of divide-and-conquer
		  solvers, and allowed us to highlight original compositions
		  of strategies performing better than already known ones.
		  Also, we were able to create and test new original
		  strategies exploiting the modular structure of SAT
		  instances.}
}