@misc{HeinzSachenbacher2008, author = {Heinz, Stefan and Sachenbacher, Martin}, title = {Using Model Counting to Find Optimal Distinguishing Tests}, issn = {1438-0064}, url = {http://nbn-resolving.de/urn:nbn:de:0297-zib-10832}, number = {08-32}, year = {2008}, abstract = {Testing is the process of stimulating a system with inputs in order to reveal hidden parts of the system state. In the case of non-deterministic systems, the difficulty arises that an input pattern can generate several possible outcomes. Some of these outcomes allow to distinguish between different hypotheses about the system state, while others do~not. In this paper, we present a novel approach to find, for non-deterministic systems modeled as constraints over variables, tests that allow to distinguish among the hypotheses as good as possible. The idea is to assess the quality of a test by determining the ratio of distinguishing (good) and not distinguishing (bad) outcomes. This measure refines previous notions proposed in the literature on model-based testing and can be computed using model counting techniques. We propose and analyze a greedy-type algorithm to solve this test optimization problem, using existing model counters as a building block. We give preliminary experimental results of our method, and discuss possible improvements.}, language = {en} } @misc{Ridder2008, author = {Ridder, Johanna}, title = {Wegeprobleme der Graphentheorie}, issn = {1438-0064}, url = {http://nbn-resolving.de/urn:nbn:de:0297-zib-10782}, number = {08-26}, year = {2008}, abstract = {Den k{\"u}rzesten Weg in einem Graphen zu finden ist ein klassisches Problem der Graphentheorie. {\"U}ber einen Vortrag zu diesem Thema beim Tag der Mathematik 2007 von R. Bornd{\"o}rfer kam ich in Kontakt mit dem Konrad-Zuse-Zentrum (ZIB), das sich u.a. mit Wegeoptimierung besch{\"a}ftigt. Ein Forschungsschwerpunkt dort ist im Rahmen eines Projekts zur Chipverifikation das Z{\"a}hlen von L{\"o}sungen, das, wie wir sehen werden, eng mit dem Z{\"a}hlen von Wegen zusammenh{\"a}ngt. Anhand von zwei Fragen aus der Graphentheorie soll diese Facharbeit unterschiedliche L{\"o}sungsmethoden untersuchen. Wie bestimmt man den k{\"u}rzesten Weg zwischen zwei Knoten in einem Graphen und wie findet man alle m{\"o}glichen Wege? Nach einer Einf{\"u}hrung in die Graphentheorie und einer Konkretisierung der Probleme wird zun{\"a}chst f{\"u}r beide eine L{\"o}sung mit auf Graphen basierenden Algorithmen vorgestellt. W{\"a}hrend der Algorithmus von Dijkstra sehr bekannt ist, habe ich f{\"u}r das Z{\"a}hlen von Wegen einen eigenen Algorithmus auf der Basis der Tiefensuche entwickelt. Im zweiten Teil der Arbeit wird das Konzept der ganzzahligen Programmierung vorgestellt und die L{\"o}sungsm{\"o}glichkeiten f{\"u}r Wegeprobleme, die sich dar{\"u}ber ergeben. Schließlich wurden die vorgestellten Algorithmen am Beispiel des S- und U-Bahnnetzes von Berlin implementiert und mit Programmen, die die gleichen Fragen {\"u}ber ganzzahlige Programmierung l{\"o}sen, verglichen.}, language = {de} } @misc{AchterbergHeinzKoch2008, author = {Achterberg, Tobias and Heinz, Stefan and Koch, Thorsten}, title = {Counting solutions of integer programs using unrestricted subtree detection}, issn = {1438-0064}, url = {http://nbn-resolving.de/urn:nbn:de:0297-zib-10632}, number = {08-09}, year = {2008}, abstract = {In the recent years there has been tremendous progress in the development of algorithms to find optimal solutions for integer programs. In many applications it is, however, desirable (or even necessary) to generate all feasible solutions. Examples arise in the areas of hardware and software verification and discrete geometry. In this paper, we investigate how to extend branch-and-cut integer programming frameworks to support the generation of all solutions. We propose a method to detect so-called unrestricted subtrees, which allows us to prune the integer program search tree and to collect several solutions simultaneously. We present computational results of this branch-and-count paradigm which show the potential of the unrestricted subtree detection.}, language = {en} }