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.