C-sat

A parallel SAT solver for clusters

Kei Ohmura, Kazunori Ueda

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    29 Citations (Scopus)

    Abstract

    Parallelizing modern SAT solvers for clusters such as Beowulf is an important challenge both in terms of performance scalability and stability. This paper describes a SAT Solver c-sat, a parallelization of MiniSat using MPI. It employs a layered master-worker architecture, where the masters handle lemma exchange, deletion of redundant lemmas and the dynamic partitioning of search trees, while the workers do search using different decision heuristics and random number seeds. With careful tuning, c-sat showed good speedup over MiniSat with reasonably small communication overhead on various clusters. On an eight-node cluster with two Dual-Core Opterons on each node (32 PEs), c-sat ran at least 23 times faster than MiniSat using 31 PEs (geometric mean; at least 31 times for satisfiable problems) for 189 large-scale problems from SAT Competition and two SAT-Races.

    Original languageEnglish
    Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Pages524-537
    Number of pages14
    Volume5584 LNCS
    DOIs
    Publication statusPublished - 2009
    Event12th International Conference on Theory and Applications of Satisfiability Testing, SAT 2009 - Swansea
    Duration: 2009 Jun 302009 Jul 3

    Publication series

    NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume5584 LNCS
    ISSN (Print)03029743
    ISSN (Electronic)16113349

    Other

    Other12th International Conference on Theory and Applications of Satisfiability Testing, SAT 2009
    CitySwansea
    Period09/6/3009/7/3

    Fingerprint

    Seed
    Scalability
    Tuning
    Lemma
    Communication
    Geometric mean
    Search Trees
    Random number
    Large-scale Problems
    Vertex of a graph
    Parallelization
    Deletion
    Partitioning
    Speedup
    Heuristics
    Architecture

    ASJC Scopus subject areas

    • Computer Science(all)
    • Theoretical Computer Science

    Cite this

    Ohmura, K., & Ueda, K. (2009). C-sat: A parallel SAT solver for clusters. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5584 LNCS, pp. 524-537). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5584 LNCS). https://doi.org/10.1007/978-3-642-02777-2_47

    C-sat : A parallel SAT solver for clusters. / Ohmura, Kei; Ueda, Kazunori.

    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5584 LNCS 2009. p. 524-537 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5584 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Ohmura, K & Ueda, K 2009, C-sat: A parallel SAT solver for clusters. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 5584 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5584 LNCS, pp. 524-537, 12th International Conference on Theory and Applications of Satisfiability Testing, SAT 2009, Swansea, 09/6/30. https://doi.org/10.1007/978-3-642-02777-2_47
    Ohmura K, Ueda K. C-sat: A parallel SAT solver for clusters. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5584 LNCS. 2009. p. 524-537. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-02777-2_47
    Ohmura, Kei ; Ueda, Kazunori. / C-sat : A parallel SAT solver for clusters. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5584 LNCS 2009. pp. 524-537 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
    @inproceedings{820ee9941c2f4249a98d2ada3636bf7f,
    title = "C-sat: A parallel SAT solver for clusters",
    abstract = "Parallelizing modern SAT solvers for clusters such as Beowulf is an important challenge both in terms of performance scalability and stability. This paper describes a SAT Solver c-sat, a parallelization of MiniSat using MPI. It employs a layered master-worker architecture, where the masters handle lemma exchange, deletion of redundant lemmas and the dynamic partitioning of search trees, while the workers do search using different decision heuristics and random number seeds. With careful tuning, c-sat showed good speedup over MiniSat with reasonably small communication overhead on various clusters. On an eight-node cluster with two Dual-Core Opterons on each node (32 PEs), c-sat ran at least 23 times faster than MiniSat using 31 PEs (geometric mean; at least 31 times for satisfiable problems) for 189 large-scale problems from SAT Competition and two SAT-Races.",
    author = "Kei Ohmura and Kazunori Ueda",
    year = "2009",
    doi = "10.1007/978-3-642-02777-2_47",
    language = "English",
    isbn = "3642027768",
    volume = "5584 LNCS",
    series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
    pages = "524--537",
    booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

    }

    TY - GEN

    T1 - C-sat

    T2 - A parallel SAT solver for clusters

    AU - Ohmura, Kei

    AU - Ueda, Kazunori

    PY - 2009

    Y1 - 2009

    N2 - Parallelizing modern SAT solvers for clusters such as Beowulf is an important challenge both in terms of performance scalability and stability. This paper describes a SAT Solver c-sat, a parallelization of MiniSat using MPI. It employs a layered master-worker architecture, where the masters handle lemma exchange, deletion of redundant lemmas and the dynamic partitioning of search trees, while the workers do search using different decision heuristics and random number seeds. With careful tuning, c-sat showed good speedup over MiniSat with reasonably small communication overhead on various clusters. On an eight-node cluster with two Dual-Core Opterons on each node (32 PEs), c-sat ran at least 23 times faster than MiniSat using 31 PEs (geometric mean; at least 31 times for satisfiable problems) for 189 large-scale problems from SAT Competition and two SAT-Races.

    AB - Parallelizing modern SAT solvers for clusters such as Beowulf is an important challenge both in terms of performance scalability and stability. This paper describes a SAT Solver c-sat, a parallelization of MiniSat using MPI. It employs a layered master-worker architecture, where the masters handle lemma exchange, deletion of redundant lemmas and the dynamic partitioning of search trees, while the workers do search using different decision heuristics and random number seeds. With careful tuning, c-sat showed good speedup over MiniSat with reasonably small communication overhead on various clusters. On an eight-node cluster with two Dual-Core Opterons on each node (32 PEs), c-sat ran at least 23 times faster than MiniSat using 31 PEs (geometric mean; at least 31 times for satisfiable problems) for 189 large-scale problems from SAT Competition and two SAT-Races.

    UR - http://www.scopus.com/inward/record.url?scp=70350624361&partnerID=8YFLogxK

    UR - http://www.scopus.com/inward/citedby.url?scp=70350624361&partnerID=8YFLogxK

    U2 - 10.1007/978-3-642-02777-2_47

    DO - 10.1007/978-3-642-02777-2_47

    M3 - Conference contribution

    SN - 3642027768

    SN - 9783642027765

    VL - 5584 LNCS

    T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

    SP - 524

    EP - 537

    BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

    ER -