Graduate Thesis Or Dissertation

Variational Satisfiability Solving

Public Deposited

Downloadable Content

Download PDF


Attribute NameValues
  • 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.
Resource Type
Date Issued
Degree Level
Degree Name
Degree Field
Degree Grantor
Commencement Year
Committee Member
Academic Affiliation
Rights Statement
Related Items
Peer Reviewed



This work has no parents.

In Collection: