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

Fingerprint

Binary trees

Keywords

  • quantification
  • quantified boolean formulae (QBF)

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)
Cashmore, Michael ; Fox, Maria ; Giunchiglia, Enrico. / Encoding reachability with quantification. Proceedings of the Vienna Summer of Logic; 1st Workshop on Quantification (QUANTIFY). 2014.
@inproceedings{c612afa3fe0e43cf8464e513fe36ad96,
title = "Encoding reachability with quantification",
abstract = "We report on techniques for translating bounded propositional reachabilityproblems into Quantified Boolean Formulae (QBF). The techniques exploitthe binary-tree structure of the QBF quantification to produce encodingslogarithmic in the size of the instance and thus exponentially smaller than thecorresponding SAT encoding with the same bound. We briefly describe our experimentalresults, and discuss the challenging structure that is implicit in theseencodings.",
keywords = "quantification, quantified boolean formulae (QBF)",
author = "Michael Cashmore and Maria Fox and Enrico Giunchiglia",
year = "2014",
language = "English",
booktitle = "Proceedings of the Vienna Summer of Logic; 1st Workshop on Quantification (QUANTIFY)",

}

Cashmore, M, Fox, M & Giunchiglia, E 2014, Encoding reachability with quantification. in Proceedings of the Vienna Summer of Logic; 1st Workshop on Quantification (QUANTIFY). QUANTIFY 2014 – First International Workshop on Quantification, Vienna, Austria, 9/07/14.

Encoding reachability with quantification. / Cashmore, Michael; Fox, Maria ; Giunchiglia, Enrico.

Proceedings of the Vienna Summer of Logic; 1st Workshop on Quantification (QUANTIFY). 2014.

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

TY - GEN

T1 - Encoding reachability with quantification

AU - Cashmore, Michael

AU - Fox, Maria

AU - Giunchiglia, Enrico

PY - 2014

Y1 - 2014

N2 - We report on techniques for translating bounded propositional reachabilityproblems into Quantified Boolean Formulae (QBF). The techniques exploitthe binary-tree structure of the QBF quantification to produce encodingslogarithmic in the size of the instance and thus exponentially smaller than thecorresponding SAT encoding with the same bound. We briefly describe our experimentalresults, and discuss the challenging structure that is implicit in theseencodings.

AB - We report on techniques for translating bounded propositional reachabilityproblems into Quantified Boolean Formulae (QBF). The techniques exploitthe binary-tree structure of the QBF quantification to produce encodingslogarithmic in the size of the instance and thus exponentially smaller than thecorresponding SAT encoding with the same bound. We briefly describe our experimentalresults, and discuss the challenging structure that is implicit in theseencodings.

KW - quantification

KW - quantified boolean formulae (QBF)

M3 - Conference contribution book

BT - Proceedings of the Vienna Summer of Logic; 1st Workshop on Quantification (QUANTIFY)

ER -

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