Tarek Menouer

Parallel learning portfolio-based solvers

By Tarek Menouer, Souheib Baarir

2017-06-01

In Proceedings of the international conference on computational science (ICCS)

Abstract

Exploiting multi-core architectures is a way to tackle the CPU time consumption when solving SAT- isfiability (SAT) problems. Portfolio is one of the main techniques that implements this principle. It consists in making several solvers competing, on the same problem, and the winner will be the first that answers. In this work, we improved this technique by using a learning schema, namely the Exploration- Exploitation using Exponential weight (EXP3), that allows smart resource allocations. Our contribution is adapted to situations where we have to solve a bench of SAT instances issued from one or several sequence of problems. Our experiments show that our approach achieves good results.

Continue reading

Parallel satisfiability solver based on hybrid partitioning method

By Tarek Menouer, Souheib Baarir

2017-03-01

In Proceedings of the 25th euromicro international conference on parallel, distributed and network-based processing (PDP)

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.

Continue reading

Search

Tags