A Generalization of SAT and #SAT for Robust Policy Evaluation
Abstract
Both SAT and #SAT can represent difficult problems in seemingly dissimilar areas such as planning, verification, and probabilistic inference. Here, we examine an expressive new language, #_SAT, that generalizes both of these languages. #_SAT problems require counting the number of satisfiable formulas in a concisely-describable set of existentially quantified, propositional formulas. We characterize the expressiveness and worst-case difficulty of #_SAT by proving it is complete for the complexity class #PNP[1], and relating this class to more familiar complexity classes. We also experiment with three new general-purpose #_SAT solvers on a battery of problem distributions including a simple logistics domain. Our experiments show that, despite the formidable worst-case complexity of #PNP[1], many of the instances can be solved efficiently by noticing and exploiting a particular type of frequent structure.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 30, 2014
- Accession Number
- ADA606746
Entities
People
- André Platzer
- Erik Zawadzki
- Geoffrey J. Gordon
Organizations
- Carnegie Mellon University