Graduate Thesis Or Dissertation
 

Variational Satisfiability Solving

Public Deposited

Downloadable Content

Download PDF
https://ir.library.oregonstate.edu/concern/graduate_thesis_or_dissertations/dv140182g

Descriptions

Attribute NameValues
Creator
Abstract
  • Over the last two decades, satisfiability and satisfiability-modulo theory (SAT/SMT) solvers have grown powerful enough to be general purpose reasoning engines throughout software engineering and computer science. However, most practical use cases of SAT/SMT solvers require not just solving a single SAT/SMT problem, but solving sets of related SAT/SMT problems. This discrepancy was directly addressed by the SAT/SMT community with the invention of incremental SAT/SMT solving. However, incremental SAT/SMT solvers require users to hand write a program which dictates the terms that are shared between problems and terms which are unique. By placing the onus on users, incremental solvers couple the users’ solution to the users’ exact sequence of SAT/SMT problems—making the solution overly specific—and require the user to write extra infrastructure to coordinate or handle the results. This dissertation argues that the aforementioned problems result from accidental complexity produced by solving a problem that is variational without the concept of variation, similar to problematic use of GOTO statements in the absence of WHILE loop constructs. To demonstrate the argument, this thesis applies theory from variational programming to the domain of SAT/SMT solvers to create the first variational SAT solver. To do so, the thesis formalizes a variational propositional logic and specifies variational SAT solving as a compiler; that compiles variational SAT problems to instructions for an industrial strength SAT solver.
Contributor
License
Resource Type
Date Issued
Degree Level
Degree Name
Degree Field
Degree Grantor
Commencement Year
Advisor
Committee Member
Academic Affiliation
Rights Statement
Related Items
  • Variational SAT prototype
Publisher
Peer Reviewed
Language

Relationships

Parents:

This work has no parents.

In Collection:

Items

Thumbnail Title Date Uploaded Visibility Actions
file details YoungJeffreyM2021.pdf 2021-06-24 Public Download