Encoding reachability with quantification

Michael Cashmore, Maria Fox, Enrico Giunchiglia

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

Abstract

We report on techniques for translating bounded propositional reachability
problems into Quantified Boolean Formulae (QBF). The techniques exploit
the binary-tree structure of the QBF quantification to produce encodings
logarithmic in the size of the instance and thus exponentially smaller than the
corresponding SAT encoding with the same bound. We briefly describe our experimental
results, and discuss the challenging structure that is implicit in these
encodings.
Original languageEnglish
Title of host publicationProceedings of the Vienna Summer of Logic; 1st Workshop on Quantification (QUANTIFY)
Number of pages3
Publication statusPublished - 2014
EventQUANTIFY 2014 – First International Workshop on Quantification - Vienna, Austria
Duration: 9 Jul 201424 Jul 2014

Conference

ConferenceQUANTIFY 2014 – First International Workshop on Quantification
CountryAustria
CityVienna
Period9/07/1424/07/14

Keywords

  • quantification
  • quantified boolean formulae (QBF)

Fingerprint Dive into the research topics of 'Encoding reachability with quantification'. Together they form a unique fingerprint.

  • Cite this

    Cashmore, M., Fox, M., & Giunchiglia, E. (2014). Encoding reachability with quantification. In Proceedings of the Vienna Summer of Logic; 1st Workshop on Quantification (QUANTIFY)