Resolution and parallelizability: barriers to the effficient parallelization of SAT solvers - INRAE - Institut national de recherche pour l’agriculture, l’alimentation et l’environnement Accéder directement au contenu
Communication Dans Un Congrès Année : 2013

Resolution and parallelizability: barriers to the effficient parallelization of SAT solvers

Résumé

Recent attempts to create versions of Satisfiability (SAT) solvers that exploit parallel hardware and information sharing have met with limited success. In fact, the most successful parallel solvers in recent competitions were based on portfolio approaches with little to no exchange of information between processors. This experience contradicts the apparent parallelizability of exploring a combinatorial search space. We present evidence that this discrepancy can be explained by studying SAT solvers through a proof complexity lens, as resolution refutation engines. Starting with the observation that a recently studied measure of resolution proofs, namely depth, provides a (weak) upper bound to the best possible speedup achievable by such solvers, we empirically show the existence of bottlenecks to parallelizability that resolution proofs typically generated by SAT solvers exhibit. Further, we propose a new measure of parallelizability based on the best-case makespan of an offline resource constrained scheduling problem. This measure explicitly accounts for a bounded number of parallel processors and appears to empirically correlate with parallel speedups observed in practice. Our findings suggest that efficient parallelization of SAT solvers is not simply a matter of designing the right clause sharing heuristics; even in the best case, it can be — and indeed is — hindered by the structure of the resolution proofs current SAT solvers typically produce.
Fichier principal
Vignette du fichier
Resolution and parallelizability_barriers to the efficient parallelization of SAT Solvers_GK_1.pdf (551.31 Ko) Télécharger le fichier
Origine : Fichiers éditeurs autorisés sur une archive ouverte
Loading...

Dates et versions

hal-02746869 , version 1 (03-06-2020)

Identifiants

  • HAL Id : hal-02746869 , version 1
  • PRODINRA : 263218

Citer

George Katsirelos, Ashish Sabharwal, Horst Samulowitz, Laurent Simon. Resolution and parallelizability: barriers to the effficient parallelization of SAT solvers. AAAI 2013 - 27th AAAI Conference, Association for the Advancement of Artificial Intelligence (AAAI). USA., Jul 2013, Bellevue, United States. ⟨hal-02746869⟩
16 Consultations
4 Téléchargements

Partager

Gmail Facebook X LinkedIn More