Incremental Satisfiability Solving and its Applications

Siert Wieringa

    Research output: ThesisDoctoral ThesisCollection of Articles

    Abstract

    The propositional logic satisfiability problem (SAT) is a computationally hard decision problem. Despite its theoretical hardness, decision procedures for solving instances of this problem have become surprisingly efficient in recent years. These procedures, known as SAT solvers, are able to solve large instances originating from real-life problem domains, such as artificial intelligence and formal verification. Such real-life applications often require solving several related instances of SAT. Therefore, modern solvers posses an incremental interface that allows the input of sequences of incrementally encoded instances of SAT. When solving these instances sequentially the solver can reuse some of the information it has gathered across related consecutive instances. This dissertation contains six publications. The two focus areas of the combined work are incremental usage of SAT solvers, and the usage of parallelism in applications of SAT solvers. It is shown in this work that these two seemingly contradictory concepts form a natural combination. Moreover, this dissertations unifies, analyzes, and extends the results of the six publications, for example, by studying information propagation in incremental solvers through graphical visualizations. The concrete contributions made by the work in this dissertation include, but are not limited to: Improvements to algorithms for MUS finding, the use of graphical visualizations to understand information propagation in incremental solvers, asynchronous incremental solving, and concurrent clause strengthening.
    Translated title of the contributionIncremental Satisfiability Solving and its Applications
    Original languageEnglish
    QualificationDoctor's degree
    Awarding Institution
    • Aalto University
    Supervisors/Advisors
    • Heljanko, Keijo, Supervising Professor
    • Heljanko, Keijo, Thesis Advisor
    Publisher
    Print ISBNs978-952-60-5568-8
    Electronic ISBNs978-952-60-5569-5
    Publication statusPublished - 2014
    MoE publication typeG5 Doctoral dissertation (article)

    Keywords

    • Incremental satisfiability solving
    • parallel satisfiability solving
    • applications of satisfiability solving

    Fingerprint

    Dive into the research topics of 'Incremental Satisfiability Solving and its Applications'. Together they form a unique fingerprint.

    Cite this