Search

Efficient verification algorithms for neural networks often depend on various abstract domains such as intervals, zonotopes, and linear star sets. The choice of the abstract domain presents an expressiveness vs. scalability trade-off: simpler domains are less precise but yield faster algorithms. This paper investigates the hexatope and octatope abstract domains in the context of neural net verification. Hexatopes are affine transformations of higher-dimensional hexagons, defined by difference constraint systems, and octatopes are affine transformations of higher-dimensional octagons, defined by unit-two-variable-per-inequality constraint systems. These domains generalize the idea of zonotopes which can be viewed as affine transformations of hypercubes. On the other hand, they can be considered as a restriction of linear star sets, which are affine transformations of arbitrary H -Polytopes. This distinction places hexatopes and octatopes firmly between zonotopes and linear star sets in their expressive power, but what about the efficiency of decision procedures? An important analysis problem for neural networks is the exact range computation problem that asks to compute the exact set of possible outputs given a set of possible inputs. For this, three computational procedures are needed: (1) optimization of a linear cost function; (2) affine mapping; and (3) over-approximating the intersection with a half-space. While zonotopes allow an efficient solution for these approaches, star sets solves these procedures via linear programming. We show that these operations are faster for hexatopes and octatopes than they are for the more expressive linear star sets by reducing the linear optimization problem over these domains to the minimum cost network flow, which can be solved in strongly polynomial time using the Out-of-Kilter algorithm. Evaluating exact range computation on several ACAS Xu neural network benchmarks, we find that hexatopes and octatopes show promise as a practical abstract domain for neural network verification. [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]

In this paper, we propose several algorithms for determining an optimal length tree-like refutation of linear feasibility in systems of Unit Two Variable Per Inequality (UTVPI) constraints. Given an infeasible UTVPI constraint system (UCS), a refutation certifies its infeasibility. The problem of finding refutations in a UCS finds applications in domains such as program verification and operations research. In general, there exist several types of refutations of feasibility in constraint systems. In this paper, we focus on a specific type of refutation called a tree-like refutation. Tree-like refutations are complete , in the sense that if a system of linear constraints is infeasible, then it must have a tree-like refutation. Associated with a refutation is its length, which equals the total number of constraints (accounting for the reuse of constraints) that are used to establish the infeasibility of the corresponding linear constraint system. Our goal in this paper is to find an optimal length tree-like refutation (OTLR) of an infeasible UCS. We describe two deterministic algorithms that find an OTLR of a UCS. If m is the number of constraints, n is the number of variables in the system, and k is the length of an OTLR, then our two algorithms run in O (n 3 ⋅ log k) time and O (m ⋅ n ⋅ k) time respectively. We also propose a true-biased, randomized algorithm for this problem. This algorithm runs in O (m ⋅ n ⋅ log n) time, and returns the length of an OTLR with probability (1 − 1 e). We extend our work to weighted UTVPI constraint systems (WUCS), where a positive weight is associated with each UTVPI constraint. The weight of a tree-like refutation is defined as the sum of the weights of the constraints used by the refutation. The problem of finding a minimum weight refutation in a WUCS is called the weighted optimal length tree-like refutation (WOTLR) problem and is known to be NP-hard. We propose a pseudo-polynomial time algorithm for the WOTLR problem and convert it into a fully polynomial time approximation scheme (FPTAS). [ABSTRACT FROM AUTHOR]

• The copy complexity of a Horn formula equals the copy complexity of the corresponding system of constraints. • The copy complexity of Horn formulas with respect to unit resolution is (m − 1) when copies of derived clauses are allowed. • A polynomial time algorithm that can determine if a 2-CNF formula has a unit read-once resolution refutation. In this paper, we discuss the copy complexity of Horn formulas with respect to unit resolution. A Horn formula is a boolean formula in conjunctive normal form (CNF) with at most one positive literal per clause. Horn formulas find applications in a number of domains, such as program verification (abstract interpretation) and logic programming (answer set programming). Quantified Horn clauses are used extensively in temporal verification of universal properties. Resolution is one of the oldest proof systems (refutation systems) for the boolean satisfiability problem (SAT), when the input is presented in conjunctive normal form (CNF). It is both sound and complete, although inefficient, when compared to other stronger proof systems for boolean formulas. Despite its inefficiency, the simple nature of resolution makes it an integral part of several theorem provers. Unit resolution is a restricted form of resolution in which each resolution step needs to use a clause with only one literal (unit literal clause). While not complete for general CNF formulas, unit resolution is complete for Horn formulas. Read-once resolution is a form of resolution in which each clause (input or derived) may be used in at most one resolution step. As with unit resolution, read-once resolution is incomplete in general and complete for Horn clauses. This paper focuses on a combination of unit resolution and read-once resolution called unit read-once resolution. Unit read-once resolution is incomplete for Horn clauses. In this paper, we study the copy complexity problem in Horn formulas with respect to unit read-once resolution. Briefly, the copy complexity of a formula with respect to unit read-once resolution, is the smallest number k , such that replicating each clause k times guarantees the existence of a unit read-once resolution refutation (UROR). This paper focuses on two problems related to the copy complexity of Horn formulas with respect to unit read-once resolution. We first relate the copy complexity of Horn formulas with respect to unit read-once resolution to the copy complexity of the corresponding Horn constraint system with respect to the addition rule. We also examine a form of copy complexity in which we permit replication of derived clauses, in addition to the input clauses. Finally, we provide a polynomial time algorithm for the problem of checking if a 2-CNF formula has a UROR. [ABSTRACT FROM AUTHOR]

In this paper, we study the problem of finding read-once refutations (ROR) of linear feasibility in a specialized class of constraint systems called UTVPI+ constraint systems (UCS +). The refutations in this paper are analyzed using the ADD inference rule. Recall that a Unit Two Variable Per Inequality (UTVPI) constraint is a constraint of the form a i ⋅ x i + a j ⋅ x j ≤ b , where b ∈ Z , and a i , a j ∈ { 0 , 1 , − 1 }. A conjunction of such constraints is called a UTVPI constraint system (UCS). UCSs find applications in a number of domains such as abstract interpretation and scheduling. We examine a more general form of UCSs that allows for a limited number of non-UTVPI constraints to be added to a UCS. We refer to these more general UCSs as UTVPI+ constraint systems or UCS + s. If a UCS + has only k non-UTVPI constraints, then we refer to it as a UCS k +. Our focus in this paper is on refutations, i.e., proofs of infeasibility in UCS + s. In particular, we study read-once refutations of linear feasibility in UCS + s. Although the problem of finding read-once refutations of UCSs is polynomial time solvable, the presence of non-UTVPI constraints makes the problem NP-hard. However, if the number of non-UTVPI constraints is fixed, then read-once refutations can be found in polynomial time. In fact, in this paper, we show that the ROR problem is fixed-parameter tractable (FPT) for UCS k + s , with respect to k , the number of non-UTVPI constraints in the system. We also provide a lower bound on the efficiency of a class of parameterized algorithms for this problem, based on the Strong Exponential Time Hypothesis. [ABSTRACT FROM AUTHOR]

As the modern integrated circuit continues to grow in complexity, the design of very large-scale integrated (VLSI) circuits involves massive teams employing state-of-the-art computer-aided design (CAD) tools. An old yet significant CAD problem for VLSI circuits is physical design automation. In physical design automation, we need to compute the best physical layout of millions to billions of circuit components on a tiny silicon surface. The process of mapping an electronic design to a chip involves several physical design stages, one of which is clustering. Even for combinatorial circuits, there are several models for the clustering problem. In particular, we consider the problem of clustering without replication in combinatorial circuits with a view towards minimizing delay (CN). The corresponding problem with replication has been well-studied and solvable in polynomial time. However, replication can become expensive when it is unbounded. Consequently, CN is a problem worth investigating. We establish the computational complexities of several variants of CN. Additionally, we obtain approximability and inapproximability results for some NP-hard variants of CN. We also present approximation and exact exponential algorithms for some variants of CN. We prove that for some cases there exists an approximation factor of strictly less than two and that our exact exponential algorithms beat brute force. Furthermore, we provide the first parameterized approximation algorithm in which the approximation ratio is also a parameter. [ABSTRACT FROM AUTHOR]

In this paper, we discuss the design and analysis of polynomial time algorithms for two problems associated with a linearly infeasible system of Unit Two Variable Per Inequality (UTVPI) constraints, viz., (a) the read-once refutation (ROR) problem, and (b) the literal-once refutation (LOR) problem. Recall that a UTVPI constraint is a linear relationship of the form: a i · x i + a j · x j ≤ b ij , where a i , a j ∈ { 0 , 1 , - 1 } . A conjunction of such constraints is called a UTVPI constraint system (UCS) and can be represented in matrix form as: A · x ≤ b . These constraints find applications in a host of domains including but not limited to operations research and program verification. For the linear system A · x ≤ b , a refutation is a collection of m variables y = [ y 1 , y 2 , ... , y m ] T ∈ R + m , such that y · A = 0 , y · b < 0 . Such a refutation is guaranteed to exist for any infeasible linear program, as per Farkas' lemma. The refutation is said to be read-once, if each y i ∈ { 0 , 1 } . Read-once refutations are incomplete in that their existence is not guaranteed for infeasible linear programs, in general. Indeed they are not complete, even for UCSs. Hence, the question of whether an arbitrary UCS has an ROR is both interesting and non-trivial. In this paper, we reduce this problem to the problem of computing a minimum weight perfect matching (MWPM) in an undirected graph. This transformation results in an algorithm that runs in in time polynomial in the size of the input UCS. Additionally, we design a polynomial time algorithm (also via a reduction to the MWPM problem) for a variant of read-once resolution called literal-once resolution. The advantage of reducing our problems to the MWPM problem is that we can leverage recent advances in algorithm design for the MWPM problem towards solving the ROR and LOR problems in UCSs. Finally, we show that another variant of read-once refutation problem called the non-literal read-once refutation (NLROR) problem is NP-complete in UCSs. [ABSTRACT FROM AUTHOR]

This paper discusses the implementation of a new parallel algorithm for the negative cost girth (NCG) problem. The girth of an unweighted graph (directed or undirected) is defined as the length of the shortest cycle in the graph. We extend the notion of girth to networks with arbitrary weights in the following way: The negative cost girth of a network is the number of edges of the shortest negative cost cycle (i.e., the negative cost cycle with the fewest number of edges). The NCG problem has been well-studied, and there exist several polynomial time algorithms for the same. This problem finds applications in several domains, including constraint-solving, real-time scheduling, and program verification. In this paper, our focus is on a parallel implementation for solving the NCG problem that runs in $$O(\log k \cdot \log n)$$ parallel time using $$O(n^3)$$ processors, where $$n$$ is the number of vertices, and $$k$$ is the NCG. We conduct an empirical analysis for both the parallel implementation, using MPI, and the corresponding sequential NCG implementation. Our experiments indicate that as the number of processors doubles, the total execution time reduces by approximately one-half. [ABSTRACT FROM AUTHOR]

This paper is concerned with the design and analysis of algorithms for optimization problems in arc-dependent networks. A network is said to be arc-dependent if the cost of an arc a depends upon the arc taken to enter a. These networks are fundamentally different from traditional networks in which the cost associated with an arc is a fixed constant and part of the input. We first study the arc-dependent shortest path (ADSP) problem, which is also known as the suffix-1 path-dependent shortest path problem in the literature. This problem has a polynomial time solution if the shortest paths are not required to be simple. The ADSP problem finds applications in a number of domains, including highway engineering, turn penalties and prohibitions, and fare rebates. In this paper, we are interested in the ADSP problem when restricted to simple paths. We call this restricted version the simple arc-dependent shortest path (SADSP) problem. We show that the SADSP problem is NP-complete. We present inapproximability results and an exact exponential algorithm for this problem. We also extend our results for the longest path problem in arc-dependent networks. Additionally, we explore the problem of detecting negative cycles in arc-dependent networks and discuss its computational complexity. Our results include variants of the negative cycle detection problem such as longest, shortest, heaviest, and lightest negative simple cycles. 2 2 An extended abstract of this work appeared in Wojciechowski et al. (2020). [ABSTRACT FROM AUTHOR]

A Quantified Linear Implication (QLI) is an inclusion query over two polyhedral sets, with a quantifier string that specifies which variables are existentially quantified and which are universally quantified. Equivalently, it can be viewed as a quantified implication of two systems of linear inequalities. In this paper, we provide a 2-person game semantics for the QLI problem, which allows us to explore the computational complexities of several of its classes. More specifically, we prove that the decision problem for QLIs with an arbitrary number of quantifier alternations is PSPACE-hard. Furthermore, we explore the computational complexities of several classes of 0, 1, and 2-quantifier alternation QLIs. We observed that some classes are decidable in polynomial time, some are NP-complete, some are coNP-hard and some are $\boldsymbol{\Pi}_{\textbf 2}^{\textbf P}$ -hard. We also establish the hardness of QLIs with 2 or more quantifier alternations with respect to the first quantifier in the quantifier string and the number of quantifier alternations. All the proofs that we provide for polynomially solvable problems are constructive, i.e., polynomial-time decision algorithms are devised that utilize well-known procedures. QLIs can be utilized as powerful modelling tools for real-life applications. Such applications include reactive systems, real-time schedulers, and static program analyzers. [ABSTRACT FROM AUTHOR]

In this paper, we discuss certifying algorithms for zero-clairvoyant scheduling (ZCS) problems. ZCS problems are a class of real-time scheduling problems defined in the E-T-C scheduling framework [Subramani, K. (2005) A comprehensive framework for specifying clairvoyance, constraints and periodicity in real-time scheduling. Comput. J., 48, 259–272]. In ZCS, the dispatcher has no knowledge of the execution time of a given job, even after the job has finished executing. A polynomial-time algorithm for ZCS was proposed in previous work of the first author [Subramani, K. (2007) A polynomial time algorithm for zero-clairvoyant scheduling. J. Appl. Logic, 5, 667–680]. However, the algorithm proposed therein is not certifying. The algorithm that we propose in this paper is certifying, in that it provides a structure that certifies the ‘yes’-instances and another structure that certifies the ‘no’-instances of ZCS problems. These structures make the discovery of implementation errors straightforward and greatly simplify the software development cycle. Moreover, the certifying algorithm has the same running time (asymptotically) as its non-certifying counterpart. We also show that the proposed certifying technique can be used to certify a class of mathematical programs called E-Quantified Polyhedral programs (E-QPPs). However, for E-QPPs, the proposed certifying algorithm has a higher asymptotic running time than its non-certifying counterpart. [ABSTRACT FROM AUTHOR]

Abstract: In this paper, we explore the computational complexity of the conjunctive fragment of the first-order theory of linear arithmetic. Quantified propositional formulas of linear inequalities with quantifier alternations are log-space complete in or depending on the initial quantifier. We show that when we restrict ourselves to quantified conjunctions of linear inequalities, i.e., quantified linear systems, the complexity classes collapse to polynomial time. In other words, the presence of universal quantifiers does not alter the complexity of the linear programming problem, which is known to be in . Our result reinforces the importance of sentence formats from the perspective of computational complexity. [Copyright &y& Elsevier]