• DocumentCode
    188653
  • Title

    Communication in Massively-Parallel SAT Solving

  • Author

    Ehlers, Thorsten ; Nowotka, Dirk ; Sieweck, Philipp

  • Author_Institution
    Dept. of Comput. Sci., Univ. Kiel, Kiel, Germany
  • fYear
    2014
  • fDate
    10-12 Nov. 2014
  • Firstpage
    709
  • Lastpage
    716
  • Abstract
    The exchange of learnt clauses is a key feature in parallel SAT solving. We present an approach based on a communication graph. Each solver thread corresponds to a node in this graph. Communication between two solvers is allowed if the respective nodes are connected by an edge. This yields another dimension in controlling the amount of communication. We show results for this approach, gaining significant speedups for up to 256 parallel solvers.
  • Keywords
    Boolean functions; computability; graph theory; Boolean satisfiability; communication graph; parallel SAT solving; solver thread; Benchmark testing; Computer architecture; Databases; Hardware; Portfolios; Sugar; Topology; Distributed Computing; High Performance Computing; Portfolio; Satisfiability;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Tools with Artificial Intelligence (ICTAI), 2014 IEEE 26th International Conference on
  • Conference_Location
    Limassol
  • ISSN
    1082-3409
  • Type

    conf

  • DOI
    10.1109/ICTAI.2014.111
  • Filename
    6984547
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=188653