Search

In this paper, we analyze the copy complexity of unsatisfiable Horn constraint systems, under the ADD refutation system. Recall that a linear constraint of the form ∑ i = 1 n a i · x i ≥ b , is said to be a horn constraint if all the a i ∈ { 0 , 1 , - 1 } and at most one of the a i s is positive. A conjunction of such constraints is called a Horn constraint system (HCS). Horn constraints arise in a number of domains including, but not limited to, program verification, power systems, econometrics, and operations research. The ADD refutation system is both sound and complete. Additionally, it is the simplest and most natural refutation system for refuting the feasibility of a system of linear constraints. The copy complexity of an infeasible linear constraint system (not necessarily Horn) in a refutation system, is the minimum number of times each constraint needs to be replicated, in order to obtain a read-once refutation. We show that for an HCS with n variables and m constraints, the copy complexity is at most 2 n - 1 , in the ADD refutation system. Additionally, we analyze bounded-width HCSs from the perspective of copy complexity. Finally, we provide an empirical analysis of an integer programming formulation of the copy complexity problem in HCSs. (An extended abstract was published in FroCos 2021 [26].) [ABSTRACT FROM AUTHOR]

In this paper, we analyze two types of refutations for Unit Two Variable Per Inequality (UTVPI) constraints. A UTVPI constraint is a linear inequality of the form: $a_{i}\cdot x_{i}+a_{j} \cdot x_{j} \le b_{k}$ , where $a_{i},a_{j}\in \{0,1,-1\}$ and $b_{k} \in \mathbb{Z}$. A conjunction of such constraints is called a UTVPI constraint system (UCS) and can be represented in matrix form as: ${\bf A \cdot x \le b}$. UTVPI constraints are used in many domains including operations research and program verification. We focus on two variants of read-once refutation (ROR). An ROR is a refutation in which each constraint is used at most once. A literal-once refutation (LOR), a more restrictive form of ROR, is a refutation in which each literal ( $x_i$ or $-x_i$) is used at most once. First, we examine the constraint-required read-once refutation (CROR) problem and the constraint-required literal-once refutation (CLOR) problem. In both of these problems, we are given a set of constraints that must be used in the refutation. RORs and LORs are incomplete since not every system of linear constraints is guaranteed to have such a refutation. This is still true even when we restrict ourselves to UCSs. In this paper, we provide NC reductions between the CROR and CLOR problems in UCSs and the minimum weight perfect matching problem. The reductions used in this paper assume a CREW PRAM model of parallel computation. As a result, the reductions establish that, from the perspective of parallel algorithms, the CROR and CLOR problems in UCSs are equivalent to matching. In particular, if an NC algorithm exists for either of these problems, then there is an NC algorithm for matching. [ABSTRACT FROM AUTHOR]

In this paper, we discuss exact and parameterized algorithms for the problem of finding a read-once refutation (ROR) in an unsatisfiable Horn constraint system (HCS). Recall that a linear constraint system |$\mathbf {A \cdot x \ge b}$| is said to be an HCS if each entry in |$\textbf {A}$| belongs to the set |$\{0,1,-1\}$| and at most one entry in each row of |$\textbf {A}$| is positive. In this paper, we examine the importance of constraints in which more variables have negative coefficients than positive coefficients. In particular, we study the impact of the proportion of these 'net-negative' constraints has on the difficulty of finding RORs. There exist several algorithms for checking whether an HCS is feasible. To the best of our knowledge, these algorithms are not certifying, i.e. they do not provide a certificate of infeasibility. Our work is concerned with providing a specialized class of certificates called 'read-once refutations'. In an ROR, each constraint defining the HCS may be used at most once in the derivation of a refutation. The problem of checking if an HCS has an ROR has been shown to be NP-hard. We analyse the HCS ROR problem from three different algorithmic perspectives, viz. parameterized algorithms, exact exponential algorithms and approximation algorithms. In particular, we show that the HCS ROR problem is fixed-parameter tractable (FPT) with respect to the number of constraints in the system that have more variables with negative coefficient than variables with positive coefficient. Additionally, we show that the HCS ROR problem becomes easy when this parameter is both small and large. We also derive an algorithm that runs in time |$O(1.66^{m})$|⁠ , where |$m$| is the number of constraints in the HCS. On the lower-bound side, we derive a lower bound on the algorithmic resources needed for this problem using the Exponential Time Hypothesis. We also establish that the HCS ROR problem does not have a polynomial kernel when the number of constraints with three or more variables in a refutation is used as a parameter. Finally, we show that the problem of approximating the length of the shortest ROR in an HCS is NPO PB-complete 1. [ABSTRACT FROM AUTHOR]

In this paper, we investigate variants of cutting plane proof systems for a class of integer programs called Horn constraint systems (HCS). Briefly, a system of linear inequalities A · x ≥ b is called a Horn constraint system, if each entry in A belongs to the set { 0 , 1 , - 1 } and furthermore there is at most one positive entry per row. Our focus is on deriving refutations, i.e., proofs of unsatisfiability of such programs in variants of the cutting plane proof system. Horn systems generalize Horn formulas, i.e., CNF formulas with at most one positive literal per clause. A Horn system which results from rewriting a Horn clausal formula is called a Horn clausal constraint system (HClCS). The cutting plane calculus (CP) is a well-known calculus for deciding the unsatisfiability of propositional CNF formulas and integer programs. Usually, CP consists of the addition rule (ADD) and the division rule (DIV). We show that the cutting plane calculus with the addition rule only (CP-ADD) does not require constraints of the form 0 ≤ x i ≤ 1 . We also investigate the existence of read-once refutations in Horn clausal constraint systems in the cutting plane proof system. We show that read-once refutations are incomplete. We show that the problem of finding a read-once refutation using only the ADD rule of an HCS is NP-hard even when the right-hand sides of the HCS belong to the set { 0 , 1 } . Additionally, we show that the problem of finding a read-once refutation using only the ADD rule of an HClCS is NP-hard. We then show that these problems remain hard when we can use both the ADD and DIV rules. We then show that the problem of finding a shortest read-once refutation of an HCS whose right-hand sides belong to the set { 0 , 1 } is NPO BP-complete when the refutation can use only the ADD rule or the refutation can use both the ADD and DIV rules. Finally, we provide a parameterized exponential time algorithm for finding a read-once refutation of a system of Horn constraints using only the ADD rule. [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]

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]

In this paper, we discuss a new combinatorial certifying algorithm for the problem of checking linear feasibility in 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. The proposed algorithm runs in $$O(m\cdot n)$$ time and $$O(m+n)$$ space on a UTVPI system with n variables and m constraints. Observe that these resource bounds match the bounds of the fastest strongly polynomial algorithm for difference constraints. Inasmuch as UTVPI constraints subsume difference constraints, it is clear that the resource requirements of our algorithm are optimal. Additionally, our algorithm is certifying, in that it produces a satisfying assignment when presented with a feasible instance, and a refutation, otherwise. At the heart of our algorithm is a new constraint network representation for UTVPI constraints. [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 study linear constraint systems in which each constraint is a fractional Horn constraint. A constraint is fractional Horn, if it can be written in the form: ∑ i = 1 n a i ⋅ x i ≥ c , where each a i is integral, c is integral, at most one of the a i s is positive, and all negative a i s are equal to −1. A conjunction of fractional Horn constraints is called a Fractional Horn Constraint Systems (FHS). FHSs generalize a number of specialized constraint systems such as Difference Constraint Systems (DCS) and Horn Constraint Systems (HCS). We know that the problem of checking lattice point feasibility in DCSs and HCSs is in P. In contrast, we show that the problem of checking lattice point feasibility in FHSs is NP-complete. We then study a sub-class of fractional Horn constraint systems called Binary Fractional Horn Constraint Systems (BFHS). In a BFHS, each constraint has at most two non-zero coefficients. In this case, we show that the problem of checking integer feasibility is in P. Furthermore, we establish several properties of the least integer point and the least linear point of a BFHS, if they exist. [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]