Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

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

Abstract : 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.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

Littérature citée [24 références]  Voir  Masquer  Télécharger

https://hal.inrae.fr/hal-02746869
Déposant : Migration Prodinra <>
Soumis le : mercredi 3 juin 2020 - 10:55:07
Dernière modification le : mercredi 16 septembre 2020 - 17:03:36

Fichier

Resolution and parallelizabili...
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

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

Collections

Citation

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⟩

Partager

Métriques

Consultations de la notice

9

Téléchargements de fichiers

10