I am happy to announce that the following paper has been
accepted at the 25rd Euromicro International Conference on Parallel,
Distributed, and Network-Based Processing (PDP 2017) to be held in St Petersburg,
Russia on March 6-8.
Title and authors:
Title : Parallel Satisfiability Solver Based on Hybrid Partitioning Method
Tarek Menour (1,3), Souheib Baarir(1,2,3).
(1) Paris Ouest Nanterre la Défense University
(2) LRDE, EPITA, Kremlin-Bicêtre, France
(3) LIP6 Laboratory, CNRS UMR 7606, Paris, France
Abstract :
This paper presents a hybrid partitioning method used to improve the performance of
solving a Satisfiability (SAT) problem. The principle of our approach consists firstly in
applying a static partitioning to decompose the search tree in finite set of disjoint
sub-trees, then 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
than others. The advantage of this method is to give a good disjoint sub-trees. However,
the drawback is the imbalance load between computing cores.
To overcome this drawback, we propose, as novelty, to extend the static partitioning by
combining with a new dynamic partitioning that assures a good load balancing between
cores. Each time a new waiting core is detected, the dynamic partitioning select
automatically by 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 results show that a good speedup is
achieved by using our hybrid method.
Show replies by date