UWSpace is currently experiencing technical difficulties resulting from its recent migration to a new version of its software. These technical issues are not affecting the submission and browse features of the site. UWaterloo community members may continue submitting items to UWSpace. We apologize for the inconvenience, and are actively working to resolve these technical issues.
 

On the relationship between satisfiability and partially observable Markov decision processes

Thumbnail Image

Files

Salmon_Ricardo.pdf (762.59 KB)

Date

2018-09-26

Authors

Salmon, Ricardo

Journal Title

Journal ISSN

Volume Title

Publisher

University of Waterloo

Abstract

Stochastic satisfiability (SSAT), Quantified Boolean Satisfiability (QBF) and decision-theoretic planning in finite horizon partially observable Markov decision processes (POMDPs) are all PSPACE-Complete problems. Since they are all complete for the same complexity class, I show how to convert them into one another in polynomial time and space. I discuss various properties of each encoding and how they get translated into equivalent constructs in the other encodings. An important lesson of these reductions is that the states in SSAT and flat POMDPs do not match. Therefore, comparing the scalability of satisfiability and flat POMDP solvers based on the size of the state spaces they can tackle is misleading. A new SSAT solver called SSAT-Prime is proposed and implemented. It includes improvements to watch literals, component caching and detecting symmetries with upper and lower bounds under certain conditions. SSAT-Prime is compared against a state of the art solver for probabilistic inference and a native POMDP solver on challenging benchmarks.

Description

Keywords

POMDP, Stochastic SAT, Satisfiability, Planning, Probabilistic Inference, SAT, QBF

LC Keywords

Citation

URI

http://hdl.handle.net/10012/13951

Collections

Theses
Computer Science