SAT Modulo Monotonic Theories

TL;DR

This paper introduces a framework for building efficient SMT solvers for monotonic theories, enabling faster solutions to graph problems and procedural content generation tasks.

Contribution

It defines monotonic theories and provides a method to construct SMT solvers for them, improving efficiency over existing approaches.

Findings

Significant speed-ups in procedural content generation tasks.

Effective SMT solvers for graph properties like reachability and min-cut.

Ability to solve previously impractical instances.

Abstract

We define the concept of a monotonic theory and show how to build efficient SMT (SAT Modulo Theory) solvers, including effective theory propagation and clause learning, for such theories. We present examples showing that monotonic theories arise from many common problems, e.g., graph properties such as reachability, shortest paths, connected components, minimum spanning tree, and max-flow/min-cut, and then demonstrate our framework by building SMT solvers for each of these theories. We apply these solvers to procedural content generation problems, demonstrating major speed-ups over state-of-the-art approaches based on SAT or Answer Set Programming, and easily solving several instances that were previously impractical to solve.