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.
展开▼
