Grid based propositional satisfiability solving

Antti E. J. Hyvärinen

    Research output: ThesisDoctoral ThesisCollection of Articles

    Abstract

    This work studies how grid and cloud computing can be applied to efficiently solving propositional satisfiability problem (SAT) instances. Propositional logic provides a convenient language for expressing real-world originated problems such as AI planning, automated test pattern generation, bounded model checking and cryptanalysis. The interest in SAT solving has increased mainly due to improvements in the solving algorithms, which recently have increasingly focused on using parallelism offered by multi-CPU computers. Partly orthogonally to these improvements this work studies several novel approaches to parallel solving of SAT instances in a grid of widely distributed "virtual" computers instead of workstations or supercomputers. Two types of parallel SAT solving approaches are analyzed and used as building blocks for more complex systems: using several solvers which compete to solve a given instance in parallel, and splitting the search space of the instance and solving the resulting partitions in parallel. The work presents several efficient partitioning functions, critical in successful splitting according to an analytical result, and presents novel solving systems that are less dependent on the partitioning function efficiency. Finally, the work studies combining clause learning, a key technique in modern SAT solvers, with the novel types of parallel solvers. Different heuristics are studied for filtering clauses learned in parallel, and the work proposes techniques which allow exchanging the clauses between different splits. The practical significance of the results are studied using large, standard benchmark sets from SAT competitions. Some of the approaches are able to solve several instances that have either not been solved at all by any other solver, or which are significantly slower to solve with other solvers.
    Translated title of the contributionGrid based propositional satisfiability solving
    Original languageEnglish
    QualificationDoctor's degree
    Awarding Institution
    • Aalto University
    Supervisors/Advisors
    • Niemelä, Ilkka, Supervising Professor
    • Junttila, Tommi, Thesis Advisor
    Publisher
    Print ISBNs978-952-60-4367-8
    Electronic ISBNs978-952-60-4368-5
    Publication statusPublished - 2011
    MoE publication typeG5 Doctoral dissertation (article)

    Keywords

    • constraint based search
    • randomized search
    • propositional satisfiability problem
    • DPLL procedure
    • clause learning
    • parallel computing
    • cloud computing
    • grid computing

    Fingerprint Dive into the research topics of 'Grid based propositional satisfiability solving'. Together they form a unique fingerprint.

    Cite this