Modular and Efficient Divide-and-Conquer SAT Solver on Top of the Painless Framework

From LRDE

Abstract

Over the last decade, parallel SATisfiability solving has been widely studied from both theoretical and practical aspects. There are two main approaches. Firstdivide-and-conquer (D&C) splits the search space, each solver being in charge of a particular subspace. The second one, portfolio launches multiple solvers in parallel, and the first to find a solution ends the computation. However although D&C based approaches seem to be the natural way to work in parallel, portfolio ones experimentally provide better performances. An explanation resides on the difficulties to use the native formulation of the SAT problem (i.e., the CNF form) to compute an a priori good search space partitioning (i.e., all parallel solvers process their subspaces in comparable computational time). To avoid this, dynamic load balancing of the search subspaces is implemented. Unfortunately, this is difficult to compare load balancing strategies since state-of-the-art SAT solvers appropriately dealing with these aspects are hardly adaptable to various strategies than the ones they have been designed for. This paper aims at providing a way to overcome this problem by proposing an implementation and evaluation of different types of divide-and- conquer inspired from the literature. These are relying on the Painless framework, which provides concurrent facilities to elaborate such parallel SAT solvers. Comparison of the various strategies are then discussed.

Documents

Bibtex (lrde.bib)

@InProceedings{	  le-frioux.19.tacas,
  author	= {Ludovic {Le Frioux} and Souheib Baarir and Julien Sopena
		  and Fabrice Kordon},
  title		= {Modular and Efficient Divide-and-Conquer {SAT} Solver on
		  Top of the {Painless} Framework},
  booktitle	= {Proceedings of the 25th International Conference on Tools
		  and Algorithms for the Construction and Analysis of Systems
		  (TACAS'19)},
  year		= 2019,
  month		= apr,
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer},
  abstract	= {Over the last decade, parallel SATisfiability solving has
		  been widely studied from both theoretical and practical
		  aspects. There are two main approaches. First,
		  divide-and-conquer (D\&C) splits the search space, each
		  solver being in charge of a particular subspace. The second
		  one, portfolio launches multiple solvers in parallel, and
		  the first to find a solution ends the computation. However
		  although D\&C based approaches seem to be the natural way
		  to work in parallel, portfolio ones experimentally provide
		  better performances. An explanation resides on the
		  difficulties to use the native formulation of the SAT
		  problem (i.e., the CNF form) to compute an a priori good
		  search space partitioning (i.e., all parallel solvers
		  process their subspaces in comparable computational time).
		  To avoid this, dynamic load balancing of the search
		  subspaces is implemented. Unfortunately, this is difficult
		  to compare load balancing strategies since state-of-the-art
		  SAT solvers appropriately dealing with these aspects are
		  hardly adaptable to various strategies than the ones they
		  have been designed for. This paper aims at providing a way
		  to overcome this problem by proposing an implementation and
		  evaluation of different types of divide-and- conquer
		  inspired from the literature. These are relying on the
		  Painless framework, which provides concurrent facilities to
		  elaborate such parallel SAT solvers. Comparison of the
		  various strategies are then discussed.},
  note		= {To appear}
}