On the Relationship Between Satisfiability and Markov Decision Processes

@InProceedings{pmlr-v115-salmon20a,
  title = 	 {On the Relationship Between Satisfiability and Markov Decision Processes},
  author =       {Salmon, Ricardo and Poupart, Pascal},
  booktitle = 	 {Proceedings of The 35th Uncertainty in Artificial Intelligence Conference},
  pages = 	 {1105--1115},
  year = 	 {2020},
  editor = 	 {Adams, Ryan P. and Gogate, Vibhav},
  volume = 	 {115},
  series = 	 {Proceedings of Machine Learning Research},
  month = 	 {22--25 Jul},
  publisher =    {PMLR},
  pdf = 	 {http://proceedings.mlr.press/v115/salmon20a/salmon20a.pdf},
  url = 	 {https://proceedings.mlr.press/v115/salmon20a.html},
  abstract = 	 {Stochastic satisfiability (SSAT) and decision-theoretic planning in finite horizon partially observable Markov decision processes (POMDPs) are both PSPACE-Complete. We describe constructive reductions between SSAT and flat POMDPs that open the door to comparisons and future cross-fertilization between the solution techniques of those problems.  We also propose a new SSAT solver called Prime that incorporates recent advances from the SAT and #SAT literature.  Using our reduction from POMDP to SSAT, we demonstrate the competitiveness of Prime on finite horizon POMDP problems.}
}