<div class="csl-bib-body">
<div class="csl-entry">Kiesl-Reiter, B. (2019). <i>Structural reasoning methods for satisfiability solving and beyond</i> [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2019.65201</div>
</div>
-
dc.identifier.uri
https://doi.org/10.34726/hss.2019.65201
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/7583
-
dc.description.abstract
Automated-reasoning tools have various applications in artificial intelligence and formal verification, ranging from the detection of bugs in software and hardware to the solution of long-standing mathematical problems. In this thesis, we present automated-reasoning methods that modify the syntactic structure of logical formulas. In particular, we deal with formulas from propositional logic and first-order logic as well as with quantified Boolean formulas. In the first part of the thesis, we introduce so-called redundancy properties that characterize cases in which formulas can be modified without affecting their satisfiability or unsatisfiability. Based on some of these redundancy properties, we then define new strong proof systems for propositional logic. As we demonstrate, these proof systems are not only highly expressive but also well-suited for automation. Harnessing their advantages, we define a satisfiability-solving paradigm that generalizes the well-known conflict-driven clause learning (CDCL) paradigm by pruning the search space more aggressively. In an empirical evaluation, we show that a solver based on our paradigm can solve formulas that aredue to theoretical restrictionstoo hard for ordinary CDCL solvers. In the second part of the thesis, we lift several popular redundancy properties from propositional logic to first-order logic. Many of these redundancy properties have been successfully used in satisfiability solving but it was unclear if they could be lifted to first-order logic. We lift them in a uniform way by introducing the principle of implication modulo resolution, which is a generalization of so-called quantified implied outer resolvents known from the theory of quantified Boolean formulas. Using these redundancy properties, we then define corresponding clause-elimination techniques and analyze their confluence properties in detail. To illustrate their practical usefulness, we implemented and evaluated a preprocessing tool that boosts the performance of theorem provers by eliminating blocked clauses from first-order formulas. Finally, we show how satisfiability-preserving formula modifications can be used to clarify the relationship between two important proof systems for quantified Boolean formulasthe long-distance-resolution calculus and the QRAT proof system. Recently, it has been shown that long-distance resolution is remarkably powerful both in theory and in practical QBF solving. It was, however, unknown how long-distance resolution is related to QRAT, a proof system introduced for certifying the correctness of QBF-preprocessing techniques. We show that QRAT polynomially simulates long-distance resolution.
en
dc.language
English
-
dc.language.iso
en
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
propositional logic
en
dc.subject
first-order logic
en
dc.subject
quantified boolean formulas
en
dc.subject
automated reasoning
en
dc.subject
sat solving
en
dc.subject
qsat solving
en
dc.subject
preprocessing
en
dc.subject
theorem proving
en
dc.subject
proof complexity
en
dc.title
Structural reasoning methods for satisfiability solving and beyond
en
dc.type
Thesis
en
dc.type
Hochschulschrift
de
dc.rights.license
In Copyright
en
dc.rights.license
Urheberrechtsschutz
de
dc.identifier.doi
10.34726/hss.2019.65201
-
dc.contributor.affiliation
TU Wien, Österreich
-
dc.rights.holder
Benjamin Kiesl-Reiter
-
dc.publisher.place
Wien
-
tuw.version
vor
-
tuw.thesisinformation
Technische Universität Wien
-
dc.contributor.assistant
Seidl, Martina
-
tuw.publication.orgunit
E192 - Institut für Logic and Computation
-
dc.type.qualificationlevel
Doctoral
-
dc.identifier.libraryid
AC15343479
-
dc.description.numberOfPages
136
-
dc.identifier.urn
urn:nbn:at:at-ubtuw:1-123001
-
dc.thesistype
Dissertation
de
dc.thesistype
Dissertation
en
tuw.author.orcid
0000-0003-3522-3653
-
dc.rights.identifier
In Copyright
en
dc.rights.identifier
Urheberrechtsschutz
de
tuw.advisor.staffStatus
staff
-
tuw.assistant.staffStatus
staff
-
tuw.advisor.orcid
0000-0001-5673-2460
-
item.languageiso639-1
en
-
item.openairetype
doctoral thesis
-
item.grantfulltext
open
-
item.fulltext
with Fulltext
-
item.cerifentitytype
Publications
-
item.mimetype
application/pdf
-
item.openairecristype
http://purl.org/coar/resource_type/c_db06
-
item.openaccessfulltext
Open Access
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering