Parallel Hybridization for SAT
An Efficient Combination of Search Space Splitting and
Portfolio 

Rodrigue Konan Tchinda and Clémentin Tayou Djamegni
Department of Mathematics and Computer Science
Faculty of Sciences
University of Dschang
P.O. Box 67, Dschang-Cameroon 

ABSTRACT. Search space splitting and portfolio are the two main approaches used in parallel SAT solving. Each of them has its strengths but also, its weaknesses. Decomposition in search space splitting can help improve speedup on satisfiable instances while competition in portfolio increases robustness. Many parallel hybrid approaches have been proposed in the literature but most of them still cope with load balancing issues that are the cause of a non-negligible overhead. In this paper, we
describe a new parallel hybridization scheme based on both search space splitting and portfolio that does not require the use of load balancing mechanisms (such as dynamic work stealing).

RÉSUMÉ. Les deux principales approches utilisées dans la résolution parallèle du problème de satisfiabilité propositionnelle sont DPR (Diviser Pour Régner) et portfolio. Chacune d’elles comporte des forces et des faiblesses. La décomposition dans DPR permet d’améliorer le speedup sur les instances satisfiables tandis que la compétition dans les portfolios accroit la robustesse. Plusieurs approches hybrides pour la résolution parallèle de SAT ont été présentées dans la littérature mais la plupart d’entre elles souffrent encore des problèmes dus aux mécanismes de rééquilibrage dynamique de charges qui sont à l’origine d’un surcoût non négligeable. Nous décrivons dans ce papier un nouveau schéma d’hybridation parallèle basé sur les deux approches DPR et portfolio ne nécessitant pas la mise en oeuvre des mécanismes de rééquilibrage de charges (tels que le vol de tâche).

KEYWORDS : SAT, portfolio, search space splitting, parallel hybridization

MOTS-CLÉS : SAT, portfolio, DPR, hybridation parallèle

Video short presentation