SAT Modulo Monotonic Theories


  • Sam Bayless University of British Columbia
  • Noah Bayless Point Grey Mini Secondary School
  • Holger Hoos University of British Columbia
  • Alan Hu University of British Columbia



SAT, SAT Modulo Theories, Answer Set Programming, Procedural Content Generation


Boolean satisfiability (SAT) solvers have been successfully applied to a wide variety of difficult combinatorial problems. Many further problems can be solved by SAT Modulo Theory (SMT) solvers, which extend SAT solvers to handle additional types of constraints. However, building efficient SMT solvers is often very difficult. In this paper, we define the concept of a Boolean monotonic theory and show how to easily build efficient SMT solvers, including effective theory propagation and clause learning, for such theories. We present examples showing useful constraints that are monotonic, including many graph properties (e.g., shortest paths), and geometric properties (e.g., convex hulls). These constraints arise in problems that are otherwise difficult for SAT solvers to handle, such as procedural content generation. We have implemented several monotonic theory solvers using the techniques we present in this paper and applied these to content generation problems, demonstrating major speed-ups over SAT, SMT, and Answer Set Programming solvers, easily solving instances that were previously out of reach.




How to Cite

Bayless, S., Bayless, N., Hoos, H., & Hu, A. (2015). SAT Modulo Monotonic Theories. Proceedings of the AAAI Conference on Artificial Intelligence, 29(1).



Main Track: Search and Constraint Satisfaction