0000000000422288
AUTHOR
Joschka Kupilas
Improving Interpolants for Linear Arithmetic
Craig interpolation for satisfiability modulo theory formulas have come more into focus for applications of formal verification. In this paper we, introduce a method to reduce the size of linear constraints used in the description of already computed interpolant in the theory of linear arithmetic with respect to the number of linear constraints. We successfully improve interpolants by combining satisfiability modulo theory and linear programming in a local search heuristic. Our experimental results suggest a lower running time and a larger reduction compared to other methods from the literature.
Scheduling of Real-Time Networks with a Column Generation Approach
We present an algorithm based on column generation for the real-time scheduling problem of allocating periodic tasks to electronic control units in multiple subsystems connected by a global bus. The allocation has to ensure that tasks can be scheduled, and messages between tasks in different subsystems can be transmitted over the global bus and meet their deadlines. Also tasks and messages occurring in a task chain must be scheduled in a way such that the sequence of execution meets their end-to-end deadline. We show that our approach computes the optimal allocation in our model and due to the column generation approach early provides lower bounds on the optimal value.
On the Low-Dimensional Steiner Minimum Tree Problem in Hamming Metric
It is known that the d-dimensional Steiner Minimum Tree Problem in Hamming metric is NP-complete if d is considered to be a part of the input. On the other hand, it was an open question whether the problem is also NP-complete in fixed dimensions. In this paper we answer this question by showing that the problem is NP-complete for any dimension strictly greater than 2. We also show that the Steiner ratio is 2 - 2/d for d ≥ 2. Using this result, we tailor the analysis of the so-called k-LCA approximation algorithm and show improved approximation guarantees for the special cases d = 3 and d = 4.
On the low-dimensional Steiner minimum tree problem in Hamming metric
While it is known that the d-dimensional Steiner minimum tree problem in Hamming metric is NP-complete if d is part of the input, it is an open question whether this also holds for fixed dimensions. In this paper, this question is answered by showing that the Steiner minimum tree problem in Hamming metric is already NP-complete in 3 dimensions. Furthermore, we show that, the minimum spanning tree gives a 2-2d approximation on the Steiner minimum tree for d>=2. Using this result, we analyse the so-called k-LCA and A"k approximation algorithms and show improved approximation guarantees for low dimensions.