Search

In this paper, we discuss the computational complexities of determining optimal length refutations of infeasible integer programs (IPs). We focus on three different types of refutations, namely read-once refutations, tree-like refutations, and dag-like refutations. For each refutation type, we are interested in finding the length of the shortest possible refutation of that type. In the case of this paper, the length of a refutation is equal to the number of inferences in that refutation. The refutations in this paper are also defined by the types of inferences that can be used to derive new constraints. We are interested in refutations with two inference rules. The first rule corresponds to the summation of two constraints and is called the ADD rule. The second rule is the DIV rule which divides a constraint by a positive integer. For integer programs, we study the complexity of approximating the length of the shortest refutation of each type (read-once, tree-like, and dag-like). In this paper, we show that the problem of finding the shortest read-once refutation is NPO PB-complete. Additionally, we show that the problem of finding the shortest tree-like refutation is NPO-hard for IPs. We also show that the problem of finding the shortest dag-like refutation is NPO-hard for IPs. Finally, we show that the problems of finding the shortest tree-like and dag-like refutations are in FPSPACE. [ABSTRACT FROM AUTHOR]

In this paper, we study the efficacy of several mathematical programming formulations for the single-source shortest path problem, the negative cost cycle detection problem, and the shortest negative cost cycle problem in arc-dependent networks. In an arc-dependent network, the cost of an arc a depends upon the arc preceding a. These networks differ from traditional networks in which the cost associated with an arc is a fixed constant and part of the input. Arc-dependent networks are useful for modeling a number of real-world problems, such as the turn-penalty shortest path problem, which cannot be captured in the traditional network setting. We present new integer and non-linear programming formulations for each problem. We also perform the first known empirical study for arc-dependent networks to contrast the execution times of the two formulations on a set of graphs with varying families and sizes. Our experiments indicate that although non-linear programming formulations are more compact, integer programming formulations are more efficient for the problems studied in this paper. Additionally, we introduce a number of cuts for each integer programming formulation and examine their effectiveness. [ABSTRACT FROM AUTHOR]

This paper is concerned with designing algorithms for and analyzing the computational complexity of the partial vertex cover problem in trees. Graphs (and trees) are frequently used to model risk management in various systems. In particular, Caskurlu et al. in [4] have considered a system which essentially represents a tripartite graph. The goal in this model is to reduce the risk in the system below a predefined risk threshold level. It can be shown that the main goal in this risk management system can be formulated as a Partial Vertex Cover problem on bipartite graphs. In this paper, we focus on a special case of the partial vertex cover problem, when the input graph is a tree. We consider four possible versions of this setting, depending on whether or not, the vertices and edges are weighted. Two of these versions, where edges are assumed to be unweighted, are known to be polynomial-time solvable. However, the computational complexity of this problem with weighted edges, and possibly with weighted vertices, remained open. The main contribution of this paper is to resolve these questions by fully characterizing which variants of partial vertex cover remain NP-hard in trees, and which can be solved in polynomial time. In the paper, we propose two pseudo-polynomial DP-based algorithms for the most general case in which weights are present on both the edges and the vertices of the tree. One of these algorithms leads to a polynomial-time procedure, when weights are confined to the edges of the tree. The insights used in this algorithm are combined with additional scaling ideas to derive an FPTAS for the general case. A secondary contribution of this work is to propose a novel way of using centroid decompositions in trees, which could be useful in other settings as well. [ABSTRACT FROM AUTHOR]

This paper is concerned with the design and analysis of a certifying algorithm for checking the lattice point feasibility of a class of constraints called unit two variable per inequality (UTVPI) constraints. A UTVPI constraint has at most two non-zero variables and the coefficients of the non-zero variables belong to the set {+1,-1}. These constraints occur in a number of application domains, including but not limited to program verification, abstract interpretation, and operations research. As per the literature, the fastest known model generating algorithm for checking lattice point feasibility in UTVPI constraint systems runs in O(m·n+n2·logn) time and O(n2) space, where m represents the number of constraints and n represents the number of variables in the constraint system (Lahiri and Musuvathi, in: Proceedings of the 5th  international workshop on the frontiers of combining systems (FroCos), lecture notes in computer science, vol 3717, pp 168–183, 2005). In this paper, we design and analyze a new algorithm for checking the lattice point feasibility of UTVPI constraints. The presented algorithm runs in O(m·n) time and O(m+n) space. Additionally it is certifying in that it produces a satisfying assignment in the event that it is presented with feasible instances and refutations in the event that it is presented with infeasible instances. The importance of providing certificates cannot be overemphasized, especially in mission-critical applications. Our approaches for the lattice point feasibility problem in UTVPI constraint systems is fundamentally different from existing approaches for this problem; indeed, it is based on new insights into combining well-known inference rules for these systems. [ABSTRACT FROM AUTHOR]