Katalin Fazekas,
"On SAT-based Solution Methods for Computational Problems"
, Johannes Kepler University, Linz, 6-2020
Original Titel:
On SAT-based Solution Methods for Computational Problems
Sprache des Titels:
Englisch
Original Kurzfassung:
Many decision problems, search problems and optimization problems raise ques-tions that can be answered automatically by computers. These computationalproblems are of great interest in computer science. Deciding the satisfiability ofa propositional formula (in short the SAT problem) is a classical NP-completecomputational problem that has been studied thoroughly in the last six decades.As a result of this vast research, current SAT solvers are efficiently used in awide variety of application domains.The focus of this thesis is on how to exploit these efficient SAT solvers andsolving techniques in solution methods for computational problems that arebeyond SAT. We model most of the considered methods as conditional transi-tion systems over abstract states. This formalization abstracts away the com-plex implementation details while it allows to formally reason about invariants,soundness, completeness and termination of the procedures.First we provide a formal framework to describe and capture how conflict-driven clause learning, the solution technique employed by current SAT solvers,can be applied and extended to address the PSPACE-complete decision problemof quantified Boolean formulas.Then we focus on the computational task where the SAT problem is extendedwith some first-order theories (e.g. functions, arrays). Our aim is to find a satis-fying solution that optimizes a pseudo-Boolean objective function. We proposea procedure where optimization, propositional reasoning, and theory reasoningare clearly separated. This allows the exploitation of efficient specialized solversfor each of these three components.Further, we address incremental SAT solving and continuous formula simplifi-cations: two crucial components for efficient computation in several applications.We propose a sound solution method that combines these powerful techniqueswith less effort and more benefits than before.Finally, we take a look at the antibandwidth problem, a graph labeling taskwith an objective to maximize the smallest difference between labels of neigh-bouring nodes. We introduce a very compact representation of that problembased on binary decision diagrams and then show how to use SAT solvers asefficient black-boxes in an iterative solution method.
Forschungs-