Konferenzartikel: Gateway Decompositions for Constrained Reachability Problems

[katz10sea]Bastian Katz, Marcus Krug, Andreas Lochbihler, Ignaz Rutter, Gregor Snelting, Dorothea Wagner, Gateway Decompositions for Constrained Reachability Problems, Proceedings of the 9th International Symposium on Experimental Algorithms, pp. 449--461, Springer, May 2010.


Given a directed graph whose vertices are labeled with propositional constraints, is there a variable assignment that connects two given vertices by a path of vertices that evaluate to true? Constrained reachability is a powerful generalization of reachability and satisfiability problems and a cornerstone problem in program analysis. The key ingredient to tackle these computationally hard problems in large graphs is the efficient construction of a short path condition: A formula whose satisfiability is equivalent to constrained reachability and which can be fed into a state-of-the-art constraint solver. In this work, we introduce a new paradigm of decompositions of digraphs with a source and a target, called gateway decompositions. Based on this paradigm, we provide a framework for the modular generation of path conditions and an efficient algorithm to compute a fine-grained gateway decomposition. In benchmarks, we show that especially the combination of our decomposition and a novel arc filtering technique considerably reduces the size of path conditions and the runtime of a standard SAT solver on real-world program dependency graphs.



Original article available at springerlink.com.


Institutsinterne Autoren

Prof. Gregor Snelting
Ehemalige Mitarbeiter
Dr. rer. nat. Andreas Lochbihler