A Generalization of SAT and #SAT for Robust Policy Evaluation

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

A Generalization of SAT and #SAT for Robust Policy Evaluation

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

Download BibTeX Cite

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.

Erik Peter Zawadzki, André Platzer, and Geoffrey J. Gordon. 2013. A Generalization of SAT and #SAT for Robust Policy Evaluation. In Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence, IJCAI-13. IJCAI, 2583–2589. https://ijcai.org/proceedings/2013/380

@inproceedings{ijcai2013p380,
  title     = {A Generalization of SAT and #SAT for Robust Policy Evaluation},
  author    = {Zawadzki, Erik Peter and Platzer, André and Gordon, Geoffrey J.},
  booktitle = {Proceedings of the Twenty-Third International Joint Conference on
               Artificial Intelligence, {IJCAI-13}},
  publisher = {AAAI Press / International Joint Conferences on Artificial Intelligence},
  editor    = {Francesca Rossi},
  pages     = {2583--2589},
  year      = {2013},
  month     = {8},
  url       = {https://ijcai.org/proceedings/2013/380},
}

TY  - CPAPER
TI  - A Generalization of SAT and #SAT for Robust Policy Evaluation
AU  - Zawadzki, Erik Peter
AU  - Platzer, André
AU  - Gordon, Geoffrey J.
T2  - Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence, IJCAI-13
PB  - AAAI Press / International Joint Conferences on Artificial Intelligence
PY  - 2013
SP  - 2583
EP  - 2589
UR  - https://ijcai.org/proceedings/2013/380
ER  -