SAT modulo monotonic theories

Satisfiability Modulo Theories (SMT) solvers are a class of efficient constraint solvers which form integral parts of many algorithms. Over the years, dozens of different Satisfiability Modulo Theories solvers have been developed, supporting dozens of different logics. However, there are still many important applications for which specialized SMT solvers have not yet been developed. We develop a framework for easily building efficient SMT solvers for previously unsupported logics. Our techniques apply to a wide class of logics which we call monotonic theories, which include many important elements of graph theory and automata theory. Using this SAT Modulo Monotonic Theories framework, we created a new SMT solver, MonoSAT. We demonstrate that MonoSAT improves the state of the art across a wide body of applications, ranging from circuit layout and data center management to protocol synthesis - and even to video game design.Science, Faculty ofComputer Science, Department ofGraduat