Encoding reachability with quantification

Michael Cashmore, Maria Fox, Enrico Giunchiglia

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


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
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


ConferenceQUANTIFY 2014 – First International Workshop on Quantification


  • quantification
  • quantified boolean formulae (QBF)

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

Cite this