12
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

      SAT Modulo Monotonic Theories

      Preprint
      , , ,

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          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.

          Related collections

          Author and article information

          Journal
          30 May 2014
          Article
          1406.0043
          31079b94-7616-459c-acc9-9e685de4ee8d

          http://arxiv.org/licenses/nonexclusive-distrib/1.0/

          History
          Custom metadata
          cs.LO

          Comments

          Comment on this article