We formulate eccentricity computation for exponentially large graphs as a decision problem for Quantified Boolean Formulas (QBFs.) and demonstrate how the notion of eccentricity arises in the area of formal hardware verification. In practice, the QBFs obtained from the above formulation are difficult to solve because they span a huge Boolean space. We address this problem by proposing an eccentricity-preserving graph transformation that drastically reduces the Boolean search space by decreasing the number of variables in the generated formulas. Still, experimental analysis shows that the reduced formulas are not solvable by state-of-the-art QBF solvers. Thus, we propose a novel SAT-based decision procedure optimized for these formulas. Despite exponential worst-case behavior of this procedure, we present encouraging experimental evidence showing its superiority to other public-domain solvers. © Springer-Verlag 2004.
CITATION STYLE
Mneimneh, M., & Sakallah, K. (2004). Computing vertex eccentricity in exponentially large graphs: QBF formulation and solution. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2919, 411–425. https://doi.org/10.1007/978-3-540-24605-3_31
Mendeley helps you to discover research relevant for your work.