- Library Home /
- Search Collections /
- Open Collections /
- Browse Collections /
- UBC Theses and Dissertations /
- SAT modulo monotonic theories
Open Collections
UBC Theses and Dissertations
UBC Theses and Dissertations
SAT modulo monotonic theories Bayless, Sam
Abstract
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.
Item Metadata
Title |
SAT modulo monotonic theories
|
Creator | |
Publisher |
University of British Columbia
|
Date Issued |
2017
|
Description |
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.
|
Genre | |
Type | |
Language |
eng
|
Date Available |
2017-03-30
|
Provider |
Vancouver : University of British Columbia Library
|
Rights |
Attribution-NonCommercial-NoDerivatives 4.0 International
|
DOI |
10.14288/1.0343418
|
URI | |
Degree | |
Program | |
Affiliation | |
Degree Grantor |
University of British Columbia
|
Graduation Date |
2017-05
|
Campus | |
Scholarly Level |
Graduate
|
Rights URI | |
Aggregated Source Repository |
DSpace
|
Item Media
Item Citations and Data
Rights
Attribution-NonCommercial-NoDerivatives 4.0 International