---
title: "A Generalization of SAT and #SAT for Robust Policy Evaluation"
authors:
  - "Erik Peter Zawadzki"
  - "André Platzer"
  - "Geoffrey J. Gordon"
doi: ""
url: "https://ijcai.org/proceedings/2013/380"
pdf: "https://ijcai.org/proceedings/2013/0380.pdf"
venue: "Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence"
year: 2013
pages: "2583-2589"
track: ""
keywords:
---

# A Generalization of SAT and #SAT for Robust Policy Evaluation

Erik Peter Zawadzki, André Platzer, Geoffrey J. Gordon

*Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence*, pages 2583-2589.

## 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 that it is complete for the complexity class #P^{NP[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 #P^{NP[1]} , many of the instances can be solved efficiently by noticing and exploiting a particular type of frequent structure.