A generalization of SAT and #SAT for robust policy evaluation
| Autor: | André Platzer, Geoffrey J. Gordon, Erik Zawadzki |
|---|---|
| Předmět: |
Discrete mathematics
Structure (mathematical logic) Class (computer programming) Theoretical computer science Computer science business.industry Generalization Computer programming Domain (software engineering) Set (abstract data type) TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES #SAT Complexity class business |
| Zdroj: | Scopus-Elsevier ResearcherID IJCAI |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|