Parallel Satisfiability Solver Based on Hybrid Partitioning Method

Authors

Tarek Menouer, Souheib Baarir

Where

Proceedings of the 25th Euromicro International Conference on Parallel, Distributed and Network-based Processing (PDP)

Place

St. Petersburg, Russia

Type

inproceedings

Projects

Spot

Date

2017-03-01

Abstract

This paper presents a hybrid partitioning method used to improve the performance of solving a Satisfiability (SAT) problems. The principle of our approach consist firstly to apply a static partitioning to decompose the search tree in finite set of disjoint sub-trees, than assign each sub-tree to one computing core. However it is not easy to choose the relevant branching variables to partition the search tree. We propose in this context to partition the search tree according to the variables that occur more frequently then others. The advantage of this method is that it gives a good disjoint sub- trees. However, the drawback is the imbalance load between all computing cores of the system. To overcome this drawback, we propose as novelty to extend the static partitioning by combining with a new dynamic partitioning that assure a good load balancing between cores. Each time a new waiting core is detected, the dynamic partitioning selects automatically using an estimation function the computing core which has the most work to do in order to partition dynamically its sub-tree in two parts. It keeps one part and gives the second part to the waiting core. Preliminary result show that a good speedup is achieved using our hybrid method.

Documents

• Paper

Bibtex (lrde.bib)

@InProceedings{	  menouer.17.pdp,
  author	= {Tarek Menouer and Souheib Baarir},
  title		= {Parallel Satisfiability Solver Based on Hybrid
		  Partitioning Method},
  booktitle	= {Proceedings of the 25th Euromicro International Conference
		  on Parallel, Distributed and Network-based Processing
		  (PDP)},
  address	= {St. Petersburg, Russia},
  month		= mar,
  pages		= {54--60},
  year		= {2017},
  abstract	= {This paper presents a hybrid partitioning method used to
		  improve the performance of solving a Satisfiability (SAT)
		  problems. The principle of our approach consist firstly to
		  apply a static partitioning to decompose the search tree in
		  finite set of disjoint sub-trees, than assign each sub-tree
		  to one computing core. However it is not easy to choose the
		  relevant branching variables to partition the search tree.
		  We propose in this context to partition the search tree
		  according to the variables that occur more frequently then
		  others. The advantage of this method is that it gives a
		  good disjoint sub- trees. However, the drawback is the
		  imbalance load between all computing cores of the system.
		  To overcome this drawback, we propose as novelty to extend
		  the static partitioning by combining with a new dynamic
		  partitioning that assure a good load balancing between
		  cores. Each time a new waiting core is detected, the
		  dynamic partitioning selects automatically using an
		  estimation function the computing core which has the most
		  work to do in order to partition dynamically its sub-tree
		  in two parts. It keeps one part and gives the second part
		  to the waiting core. Preliminary result show that a good
		  speedup is achieved using our hybrid method.},
  doi		= {10.1109/PDP.2017.70}
}