1 Introduction

This paper examines the problems of finding optimal length refutations of infeasible integer programs (IPs). We study three different types of refutations, each of which is characterized by how the reuse of constraints is permitted.

The first type of refutation examined in this paper is read-once refutation. In a read-once refutation, for the most part, constraints cannot be reused. However, if a constraint can be rederived without reusing constraints from the original system, then it can be used as many times as it can be derived.

The second type of refutation examined is tree-like refutation. In a tree-like refutation, constraints from the original system can be reused, and derived constraints cannot. As with read-once refutations, constraints can be rederived. However, for tree-like refutations, these rederivations can reuse constraints from the original system.

The third type of refutation examined is dag-like refutation. In a dag-like refutation, both constraints in the original system and derived constraints can be reused. This means that constraints do not need to be rederived.

For each refutation type, we are interested in finding the length of the shortest possible refutation of that type. For our purposes, the length of a refutation is equal to the number of inferences in that refutation. For both read-once refutations and tree-like refutations, the rederivation of a constraint increases the length of the refutation. This does not matter in the case of dag-like refutations, since rederivation is unnecessary. Each refutation system is associated with a set of inference rules that can be used to produce refutations of a given type of constraint system. For integer programs, we examine refutations that allow for two types of inferences.

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 IPs, 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 and the problem of finding the shortest dag-like refutation are both NPO-hard. Finally, we show that the problems of finding the shortest tree-like and dag-like refutations are in FPSPACE.

2 Statement of Problems

In this section, we introduce the concepts examined in this paper and define the problems under consideration.

Definition 1

A polyhedral constraint system is a conjunction of constraints in which each constraint in \(\textbf{C}\) is an inequality of the form \(\textbf{a}_j \cdot \textbf{x} \le b_j\) where \(\textbf{a}_j \in \mathbb {Q}^n\) and \(b_j \in \mathbb {Q}\).

Note that \(\textbf{C}\) can be represented in matrix form as \(\mathbf{A \cdot x \le b}\). In the constraint \(\textbf{a}_j \cdot \textbf{x} \le b_j\), \(b_j\) is referred to as the defining constant.

Definition 2

An integer polyhedral constraint system is a polyhedral constraint system in which for each variable \(x_i\), the corresponding domain \(D_i = \mathbb {Z}\).

Such a constraint system is known as an integer program (IP).

Example 1

System (1) is an integer program.

$$\begin{aligned}&3 \cdot x_1 + 5 \cdot x_2 - 4 \cdot x_3 \le -2 \quad -2 \cdot x_2 + 7 \cdot x_3 \le 4&\\&x_1 \in \{0,1\} \quad x_2 \in \{-1,0,1\} \quad x_3 \in \{0,1,2\}&\nonumber \end{aligned}$$
(1)

Refutations are defined by the inference rules that can be used to deduce a contradiction. Refutations of integer programs can use two inference rules.

The first rule corresponds to the summation of two constraints and is defined as follows:

$$\begin{aligned} \textbf{ADD}:\dfrac{ { \sum _{i=1}^n a_i\cdot x_i} \le b_1 \quad {\sum _{i=1}^n a'_i \cdot x_i} \le b_2 }{\sum _{i=1}^n (a_i+a'_i)\cdot x_i \le b_1 + b_2} \end{aligned}$$
(2)

We refer to Rule (2) as the ADD rule.

Example 2

Consider the constraints \(3 \cdot x_1 + 5 \cdot x_2 - 4 \cdot x_3 \le -2\) and \(-2 \cdot x_2 + 7 \cdot x_3 \le 4\). Applying the ADD rule to these constraints results in the constraint \(3 \cdot x_1 + 3 \cdot x_2 + 3 \cdot x_3 \le 2\).

It is easy to see that Rule (2) is sound in that any assignment satisfying the hypotheses must satisfy the consequent.

Refutations of integer programs also use an additional rule. This is referred to as the DIV rule and is defined as follows:

$$\begin{aligned} \textbf{DIV}:\dfrac{ \sum _{i=1}^{n} a_{i} \cdot x_i \le b \quad k \in \mathbb {Z}^+:\frac{a_{i}}{k} \in \mathbb {Z}}{ \sum _{i=1}^{n} \frac{a_{i}}{k} \cdot x_i \le \left\lfloor \frac{b}{k}\right\rfloor } \end{aligned}$$
(3)

Example 3

Consider the constraint \(3 \cdot x_1 + 3 \cdot x_2 + 3 \cdot x_3 \le 2\). Applying the DIV rule to this constraint with \(k=3\) results in the constraint \(x_1 + x_2 + x_3 \le 0\).

Rule (3) corresponds to dividing a constraint by a common divisor of the left-hand coefficients and then rounding the right-hand side. Since each \(\frac{a_{i}}{k}\) is an integer. This inference preserves integer solutions but does necessarily preserve linear solutions. A constraint derived using the DIV rule is also known as a Chvátal-Gomory cut [10].

Definition 3

An integer refutation is a sequence of applications of the ADD and DIV rules that results in a contradiction of the form \(0 \le b\), \(b < 0\).

In this paper, we study several types of refutations. These are read-once refutations, tree-like refutations, and dag-like refutations. Our focus is on determining the optimal number of inferences in a refutation. Note that both the ADD rule and the DIV rule contribute to the length of the refutation.

Definition 4

A read-once refutation is a refutation in which each constraint C can be used in only one inference. This applies to constraints present in the original formula and those derived as a result of previous inferences.

Note that in a read-once refutation, a constraint can be reused if it can be rederived. However, it must be rederived from a different set of input constraints.

Definition 5

A tree-like refutation is a refutation in which each derived constraint can be used at most once.

Note that in tree-like refutations, the input constraints can be used multiple times. Thus any derived constraint can be derived multiple times as long as it is rederived each time it is used. This rederivation can reuse derived constraints. However, those constraints also need to be rederived. Tree-like refutation is a complete refutation system [5].

Definition 6

A dag-like refutation is a refutation in which each constraint can be used multiple times.

It follows that dag-like refutations procedures are complete as well.

We now define the notion of length of a refutation.

Definition 7

The length of a refutation R of a constraint system is the number of inferences (both ADD and DIV) made in R.

For each type of refutation, there are two associated problems. These are the decision problem, asking if a system has the desired type of refutation, and the optimization problem, asking for the length of the shortest refutation of the desired type. Note that every infeasible constraint system has a tree-like refutation and a dag-like refutation. Thus, the decision problems for these two refutation types are trivial. Furthermore, we have shown that the problem of determining if an IP has a read-once refutation is NP-hard even when the constraints are UTVPI (Unit Two Variable Per Inequality) constraints [26, 27].

In this paper, we examine the following optimization problems:

  1. 1.

    The Integer Programming Optimal Length Read-once Refutation (IP-OLRR) problem: Given an infeasible IP \(\textbf{I}\), what is the length of the shortest read-once refutation of \(\textbf{I}\)?

  2. 2.

    The Integer Programming Optimal Length Tree-like Refutation (IP-OLTR) problem: Given an infeasible IP \(\textbf{I}\), what is the length of the shortest tree-like refutation of \(\textbf{I}\)?

  3. 3.

    The Integer Programming Optimal Length Dag-like Refutation (IP-OLDR) problem: Given an infeasible IP \(\textbf{I}\), what is the length of the shortest dag-like refutation of \(\textbf{I}\)?

Note that the problem of determining if an IP has a refutation is only interesting if the IP is infeasible. Thus, the problems studied in this paper are promise problems [17]. That is, the problems are only defined on a subset of possible inputs. Observe that the IP-OLRR, IP-OLTR, and IP-OLDR problems are only defined on infeasible IPs. Additionally, the problem of determining if an integer program is infeasible is coNP-complete. The reductions used in this paper are guaranteed to generate infeasible IPs. Thus, the complexity results we obtain only apply to the set of infeasible IPs. Note that a feasible IP trivially lacks any refutation. Since the set of infeasible IPs is a subset of all IPs, our results can easily be generalized to all IPs. Thus, we can consider the non-promise versions of each problem.

3 Motivation and Related Work

In this section, we motivate our work and describe existing work for related problems.

Constraint systems are heavily used in the field of software verification [11, 12]. Corresponding to a piece of software, a constraint system can be derived and then combined with constraints corresponding to the negation of the specifications. If the resultant system of constraints is infeasible, then the software is consistent with its specifications. Although this approach is intuitive and straightforward, it may become impractical because of the large number of constraints that are generated. A constraint-based approach to program verification has also been attempted for rule-based programming [6]. Rule-based programming has gained interest in the software industry over the past years, because of the growing use of Business Rules Management Systems. Hence, a demand for the verification of rule programs has emerged. Also, in [19] it is shown how the constraint-based approach can be used to model a wide spectrum of program analysis using disjunctions and conjunctions of linear inequalities. Linear programs have also been used as a finer grained abstraction for sequential programs offering an effective model checking procedure [2].

For integer programs, we are interested in cutting plane based refutations. Cutting planes are often used to refute integer programs constructed from CNF formulas [14]. When applied to such systems, cutting plane based refutations can be exponentially more compact than resolution based refutations [7, 15, 20, 25]. Several restricted versions of cutting planes have been examined [28]. These restrictions included limiting addition to cases where a variable is canceled, and replacing the division rule with a saturation rule. It was shown that these restricted versions of cutting planes can be simulated by resolution when the coefficients are small [28]. Every infeasible integer program with m constraints over n variables has a cutting plane refutation of length \(O(n^{3\cdot n})\) that can be computed using polynomial workspace [13]. Workspace is defined as the amount of space used to store the intermediate constraints. Once an intermediate constraint is no longer necessary, it is removed from the workspace [13]. Recently, Cheung et al. discussed the verification of integer programming results using cutting plane refutations, but from an empirical perspective [9]. To the best of our knowledge, our paper is the first of its kind to focus on approximation complexity for the problem of determining optimal length refutations.

Closely related to the problem of finding the length of the shortest refutation of a system S under a proof system P, is the problem of automatizability [1]. A proof system P is automatizable if there exists a deterministic algorithm that, when given an infeasible system S, generates a refutation of S in time polynomial in the length of shortest refutation of S [3]. It was shown that resolution as a proof system is not automatizable, unless P = NP [4]. In the case of integer programming, cutting planes are not automatizable, unless P = NP [18]. In [18] it is also shown that it is NP-hard to approximate the minimum length of a dag-like cutting plane proof length to within \(2^{n^\epsilon }\). In this paper, we show that this problem is NPO-hard for a different proof system.

4 Optimal Length Read-Once Refutations

In this section, we show that the problem of finding the shortest read-once refutation of an IP is NPO PB-complete.

Theorem 1

The IP-OLRR problem is NPO PB-complete.

Proof

A read-once refutation R of an integer program \(\textbf{I}\) is polynomially sized in terms of the size of \(\textbf{I}\). Additionally, the length of a read-once refutation can be computed in polynomial time. Finally, since each constraint in \(\textbf{I}\) is used at most once, the length of the read-once refutation is linear in terms of the size of \(\textbf{I}\). Thus, the IP-OLRR problem is in NPO PB. Now we need to show NPO PB-hardness.

This is accomplished by a reduction from the Minimum 0-1 Programming problem. This problem is formulated as follows:

Given an integer program \(\mathbf{A \cdot x \ge b}\), \(\textbf{x} \in \{0,1\}^n\), find the minimum value of \(\mathbf{c \cdot x}\) for some integer valued vector \(\mathbf{c \ge 0}\).

In the general case, this problem is known to be NPO-complete [24]. However, for this reduction, we are only interested in the case where \(\mathbf{c=1}\). This specific form of Minimum 0-1 Programming is known to be NPO PB-complete [22].

Consider the following instance of the Minimum 0-1 programming problem:

\( \min \sum _{i=1}^n x_i \quad \mathbf{A \cdot x} = \textbf{b} \quad \textbf{x} \in \{0,1\}^n. \) Even in this form, the Minimum 0-1 programming problem is NPO PB-complete [22].

Corresponding to this system, we can construct the following linear program \(\textbf{L}\):

\(\mathbf{y \cdot A} \le \textbf{0} \quad {-\textbf{y}\cdot b} \le -1.\)

From \(\textbf{L}\), we can construct the IP \(\textbf{I}\) as follows:

1. For each variable \(y_i\) in \(\textbf{L}\), add the variable \(y_i\) to \(\textbf{I}\). Additionally, add the new variable \(x_0\) to \(\textbf{I}\). 2. Add all of the constraints in \(\textbf{L}\) to \(\textbf{I}\). 3. Let p, be the first prime larger than \(\max _{i=1 \ldots n} (\sum _{i=1}^m |a_{ij}|)\) where \(a_{ij}\) is an element of the matrix \(\textbf{A}\). 4. Add the term \(p \cdot x_0\) to the constraint in \(\textbf{I}\) with defining constant \(-1\). By construction, there is exactly one such constraint. We will refer to this new constraint as \(I_1\). 5. Add the constraint \(-x_0 \le 0\) to \(\textbf{I}\).

We will now show that \(\textbf{I}\) has a read-once integer refutation of length \((k+2)\) if and only if \(\textbf{L}\) has a read-once linear refutation of length k.

First, assume that \(\textbf{L}\) has a read-once linear refutation of length k. By construction, any read-once refutation of \(\textbf{L}\) corresponds to a read-once derivation of the constraint \(p \cdot x_0 \le -1\). We can then divide this constraint by p and sum the result with the constraint \(-x_0 \le 0\) to obtain a contradiction. Since the original refutation had length k, the new refutation has length \((k+2)\).

Now assume that \(\textbf{I}\) has a read-once integer refutation of length \((k+2)\). As mentioned above, we can assume without loss of generality that the constraint \(I_1\) is the only constraint in \(\textbf{I}\) with negative defining constant. Thus, it must be used in any refutation of \(\textbf{I}\).

The only other constraint in \(\textbf{I}\) with the variable \(x_0\) is \(-x_0 \le 0\). Thus, this constraint must be used to cancel the variable \(x_0\). Since the refutation is read-once, we must first apply the DIV rule to the constraint derived from \(I_1\). By construction, the DIV rule must be applied to this constraint with coefficient p. However, by construction, p is larger than any coefficient in any constraint derived from \(I_1\). Thus, the DIV rule cannot be applied until all other variables are eliminated from \(I_1\). Thus, we must derive the constraint \(p \cdot x_0 \le -1\). This derivation takes k steps and corresponds to a read-once linear refutation of \(\textbf{I}\). This means that \(\textbf{I}\) has a read-once linear refutation of length k. Thus, the IP-OLRR problem is NPO PB-complete.    \(\square \)

Since the IP-OLRR problem is NPO PB-complete, there exists an \(\epsilon >0\) such that the IP-OLRR cannot be approximated to within a factor of \(O(n^\epsilon )\), unless P \(=\) NP [21]. Thus, the IP-OLRR cannot be approximated to within a polylogarithmic factor, unless P \(=\) NP.

5 Optimal Length Tree-Like and Dag-Like Refutations

In this section, we show that the IP-OLTR and IP-OLDR are NPO-hard. Note that for these problems, we are not guaranteed polynomial length refutations. Thus we do not have NPO-completeness.

Theorem 2

The IP-OLTR problem is NPO-hard.

Proof

This will be accomplished by a reduction from the Traveling Salesman Path Problem. This problem is NPO-complete [24].

Let \(\textbf{G}\) be a complete undirected graph with n vertices. From \(\textbf{G}\) we create an IP \(\textbf{I}\) as follows: 1. For each vertex \(v_i\) in \(\textbf{G}\), create the variable \(x_i\). 2. Create the constraint \(x_1 + 2 \cdot x_2 + 2 \cdot x_3 + \ldots + 2 \cdot x_{n-1} + 2 \cdot x_n + p \cdot x_0 \le -1\). Where p is the fist prime such that \(p > 2 \cdot n \cdot \sum _{i=1}^{n-1} \sum _{j=i+1}^n w(e_{i,j})\). Additionally, create the constraint \(-x_0 \le 0\). 3. For each edge \(e_{i,j}\) in \(\textbf{G}\), create the variables \(y_{i,j}\) and \(z_{i,j,l}\) for \(l=1,\ldots , n-1\). Additionally, create the constraint \(-y_{i,j} \le 0\). 4. For each edge \(e_{i,j}\) such that \(i,j \in \{2, \ldots , n\}\), and each \(l=2, \ldots , n-2\), create the constraint \(-x_i - x_j + 2 \cdot n \cdot w(e_{i,j}) \cdot y_{i,j} + 2 \cdot z_{i,j,l} \le 0\). 5. For each edge \(e_{i,n}\), create the constraint \(-x_i - x_n + 2 \cdot n \cdot w(e_{i,n}) \cdot y_{i,n} + z_{i,n,n-1} \le 0\). 6. For each edge \(e_{1,j}\), create the constraint \(-x_1 - x_j + 2 \cdot n \cdot w(e_{1,j}) \cdot y_{1,j} + z_{1,j,1} \le 0\). 7. For each pair of edges \(e_{i,j}\) and \(e_{j,k}\) that share an endpoint, and each \(l =1, \ldots , n-2\), create the constraint \(-z_{i,j,l} - z_{j,k,l+1} \le 0\). This construction forms the function f for our PTAS reduction.

First, assume that \(\textbf{G}\) has a Traveling Salesman Path P of length W from \(x_1\) to \(x_n\). Let P traverse the vertices in the order \(v_{P(1)}\) through \(v_{P(n)}\). We can construct a tree-like refutation R of length \(2 \cdot n \cdot (W+1)\) for \(\textbf{I}\) as follows: 1. Start with the constraint \(x_1 + 2 \cdot x_2 + 3 \cdot x_2 + \ldots + 2 \cdot x_{n-1} + 2 \cdot x_n + p \cdot x_0 \le -1\). 2. Add the constraint \(-x_{1} - x_{P(2)} + 2 \cdot n \cdot w(e_{1,P(2)}) \cdot y_{1,P(2)} + z_{1,P(2),1} \le 0\) to R. 3. For \(i=2 \ldots n-2\), add the constraint \(-x_{P(i)} - x_{P(i+1)} + 2 \cdot n \cdot w(e_{P(i),P(i+1)}) \cdot y_{P(i),P(i+1)} + 2 \cdot z_{P(i),P(i+1),i} \le 0\) to R. 4. Add the constraint \(-x_{P(n-1)} - x_{n} + 2 \cdot n \cdot w(e_{P(n-1),n}) \cdot y_{P(n-1),n} + z_{P(n-1),n,n-1} \le 0\) to R. 5. For \(i=2 \ldots n-2\), add \(2 \cdot n \cdot w(e_{P(i),P(i+1)})\) copies of the constraint \(-y_{P(i),P(i+1)} \le 0\) to R. 6. For \(i=1 \ldots n-2\), the constraint \(-z_{P(i),P(i+1),i} - z_{P(i+1),P(i+2), i+1} \le 0\) to R. Observe that summing the constraints in R results in the constraint \(p \cdot x_0 \le -1\). Applying the DIV rule with \(d=p\) to this constraint results in the constraint \(x_0 \le -1\). Adding the constraint \(x_0 \le 0\) results in the contradiction \(0 \le -1\). Note that, R contains a total of \(2 \cdot n \cdot (W+1)\) inferences. Thus R is a tree-like refutation of length \(2 \cdot n \cdot W\) for \(\textbf{I}\).

Now assume that \(\textbf{I}\) has a tree-like refutation R of length \(2 \cdot n \cdot (W+1)\). We can construct a set of edges P as follows: For each edge \(e_{i,j}\) if R contains the constraint \(-y_{i,j} \le 0\), add \(e_{i,j}\) to P. This forms the function g for our PTAS reduction. Observe the following:

  1. 1.

    The constraint \(x_1 + 2 \cdot x_2 + 3 \cdot x_2 + \ldots + 2 \cdot x_{n-1} + 2 \cdot x_n + p \cdot x_0 \le -1\), is the only constraint in the system with a negative defining constant. Thus, it must be part of R. We will refer to this constraint as C. By construction of \(\textbf{I}\), \(p > 2 \cdot n \cdot (W+1)\). Thus, if the DIV rule is not applied to C, then the constraint \(x_0 \le 0\) will need to be used at least \(p > 2 \cdot n \cdot (W+1)\) times. In this case, the length of R is more than \(2 \cdot n \cdot (W+1)\). Thus, the DIV rule must be applied to C. Due to the value chosen for p, this can only happen after everything else is canceled from C.

  2. 2.

    To cancel \(x_1\) from C, R must include a constraint of the form \(-x_1 - x_j + 2 \cdot n \cdot w(e_{1,j}) \cdot y_{1,j} + z_{1,j,1} \le 0\). Let \(P(2)=j\). Note that this constraint also cancels a copy of \(x_{P(2)}\) from C.

  3. 3.

    To cancel the other copy of \(x_{P(2)}\) from C, R must include a constraint of the form \(-x_{P(2)} - x_j + 2 \cdot n \cdot w(e_{P(2),j}) \cdot y_{P(2),j} + 2 \cdot z_{P(2),j,1} \le 0\). Let \(P(3)=j\). Note that this constraint also cancels a copy of \(x_{P(3)}\) from C.

  4. 4.

    We can continue this process until \(P(h) = n\) for some \(h \le n\). Due to the structure of C, the vertices \(v_1\), \(v_{P(2)}\), \(v_{P(3)}\), \(\ldots \), \(v_{P(h)}\) are all distinct.

  5. 5.

    Consider the constraint \(-x_{P(h-1)} - x_{P(h)} + 2 \cdot n \cdot w(e_{P(h-1),P(h)}) \cdot y_{P(h-1),P(h)} + z_{P(h-1),P(h),1} \le 0\) in R. Since \(P(h)=n\), by construction of \(\textbf{I}\), this constraint must be \(-x_{P(h-1)} - x_{P(h)} + 2 \cdot n \cdot w(e_{P(h-1),P(h)}) \cdot y_{P(h-1),P(h)} + z_{P(h-1),P(h),n-1} \le 0\). Note that this constraint introduces the variable

    \(z_{P(h-1),P(h),n-1}\) to R

  6. 6.

    Consider the constraint \(-x_{P(h-2)} - x_{P(h-1)} + 2 \cdot n \cdot w(e_{P(h-2),P(h-1)}) \cdot y_{P(h-2),P(h-1)} + 2 \cdot z_{P(h-2),P(h-1),1} \le 0\) in R. Recall that R contains the variable \(z_{P(h-1),P(h),n-1}\). To cancel this variable, R must contain a constraint of the form \(-z_{j,P(h-1),n-2} - z_{P(h-1),P(h),n-1} \le 0\). By construction, \(z_{P(h-2),P(h-1),1}=z_{j,P(h-1),n-2}\). Thus, \(l=n-2\).

  7. 7.

    Continuing this process, we see that \(1 = n- (h-1)\). Thus, \(h=n\). As shown previously, the vertices \(v_1\), \(v_{P(2)}\), \(v_{P(3)}\), \(\ldots \), \(v_{P(n)}\) are all distinct. Thus P is a Traveling Salesman Path in \(\textbf{G}\). For each edge \(e_{P(i),P(i+1)}\) in P, R contains \(2 \cdot n w(e_{P(i),P(i+1)})\) copies of the constraint \(-y_{P(i),P(i+1)} \le 0\). From the observations above, R contains an additional \(2 \cdot n\) constraints. Thus, R contains a total of \(2 \cdot n \cdot (W'+1)\) constraints where \(W'\) is the total length of P. Since R has length \(2 \cdot n \cdot (W+1)\), P has length W.

All that remains is to establish that a PTAS reduction exists from the Minimum 0-1 Programming problem to the IP-OLTR problem. This will be done by establishing the existence of the functions f, g, and \(\alpha \).

  1. 1.

    The function f: We provided a method for constructing an integer program \(\textbf{I}\) from a graph \(\textbf{G}\). This forms the function f required for the PTAS reduction.

  2. 2.

    The function g: We provided a method to take a tree-like refutation of \(\textbf{I}\) and construct a Traveling Salesman Path in \(\textbf{G}\). This forms the function g required for the PTAS reduction.

  3. 3.

    The function \(\alpha \): Let \(W^*\) be the shortest Traveling Salesman Path in \(\textbf{G}\). \(\textbf{I}\) has a tree-like refutation of length \(2 \cdot n \cdot (W^*+1)\). Additionally, if \(\textbf{I}\) had a shorter tree-like refutation, then \(\textbf{G}\) would have a shorter path. Thus, the IP-OLTR of \(\textbf{I}\) has length \(2 \cdot n \cdot (W^*+1)\). Let \(\alpha (\epsilon ) = \frac{\epsilon -1}{2}\). Let R be a tree-like refutation of \(\textbf{I}\) of length \(2 \cdot n \cdot (W+1)\). The function g produces a Traveling Salesman Path of length W. If \(\frac{2 \cdot n \cdot (W+1)}{2 \cdot n \cdot (W^*+1)}\le 1 + \alpha (\epsilon ) = \frac{\epsilon +1}{2}\), then

    $$\frac{W}{W^*} \le \frac{2 \cdot W}{2 \cdot W^*} \le \frac{2 \cdot (W+1)}{W^* +1} \le \frac{2 \cdot ( \epsilon +1)}{2} = 1+ \epsilon .$$

Thus, the IP-OLTR problem for linear programs is NPO-hard.    \(\square \)

Since the IP-OLTR problem is NPO-hard, there exists an \(\epsilon >0\) such that the IP-OLTR cannot be approximated to within a factor of \(O(2^{n^\epsilon })\), unless P \(=\) NP [21]. Thus, the IP-OLTR cannot be approximated to within a polynomial factor, unless P \(=\) NP.

Theorem 3

The IP-OLDR problem is NPO-hard.

Proof

This will be accomplished by a reduction from the Minimum Integer Programming problem.

Consider the following instance of the Minimum 0-1 programming problem:

$$\begin{aligned} \min \sum _{i=1}^n (2 \cdot \log c_i +1) \cdot x_i \quad \mathbf{A \cdot x} = \textbf{b} \quad \textbf{x} \in \{0,1\}^n. \end{aligned}$$

Assume without loss of generality that \(\mathbf{c \ge 1}\).

While in general Minimum 0-1 programming is NPO-complete, the values of the coefficients in the optimization function are polynomial in the size of the input. Thus, the final value of the objective function is polynomial in the size of the input. Consequently, this problem is NPO PB-complete [22, 24].

Let \(\textbf{D}\) be the \(n \times n\) matrix such that \(d_{i,i} = c_i-1\) and \(d_{i,j} =0\) for \(i \ne j\). Corresponding to the Minimum 0-1 programming instance, we can construct the following linear program \(\textbf{L}\):

$$\begin{aligned} \mathbf{y \cdot A} +\mathbf{z \cdot D} \le \textbf{0} \quad -\textbf{z} \le 0 \quad {-\textbf{y}\cdot b} \le -1 \end{aligned}$$

From \(\textbf{L}\), we can construct the IP \(\textbf{I}\) as follows:

1. For each variable \(y_i\) in \(\textbf{L}\), add the variable \(y_i\) to \(\textbf{I}\). Additionally, add the variable \(x_0\) to \(\textbf{I}\). 2. Add all of the constraints in \(\textbf{L}\) to \(\textbf{I}\). 3. Let p, be the first prime larger than \(\max _{i=1 \ldots n} (\sum _{i=1}^m |a_{ij}|)\). 4. Add the term \(p \cdot x_0\) to the constraint \(L_1\) in \(\textbf{L}\) with defining constant \(-1\). By construction, there is exactly one such constraint. We will refer to this new constraint as \(I_1\). 5. Add the constraint \(-x_0 \le 0\) to \(\textbf{I}\).

We will now show that \(\textbf{I}\) has a dag-like integer refutation of length \((k+2)\) if and only if \(\textbf{L}\) has a dag-like linear refutation of length k.

First, assume that \(\textbf{L}\) has a dag-like linear refutation of length k. By construction, any dag-like refutation of \(\textbf{L}\) corresponds to a dag-like derivation of the constraint \(c_L \cdot p \cdot x_0 \le -c_L\) where \(c_L\) is the number of times constraint \(L_1\) was used in the dag-like refutation. We can then divide this constraint by \(c_L \cdot p\) and sum the result with the constraint \(-x_0 \le 0\) to obtain a contradiction. Since the original refutation had length k, the new refutation has length \((k+2)\).

Now assume that \(\textbf{I}\) has a dag-like integer refutation of length \((k+2)\). As mentioned previously, we can assume without loss of generality that the constraint \(I_1\) is the only constraint in \(\textbf{I}\) with negative defining constant. Thus, it must be used in any refutation of \(\textbf{I}\).

The only other constraint in \(\textbf{I}\) with the variable \(x_0\) is \(-x_0 \le 0\). Thus, this constraint must be used to cancel the variable \(x_0\). We want to avoid using the constraint \(-x_0 \le 0\) p times. Thus, we must first apply the DIV rule to the constraint derived from \(I_1\). By construction, the DIV rule must be applied to this constraint with a coefficient divisible by p. However, by construction, p is larger than any coefficient in any constraint derived from \(I_1\) by a dag-like derivation of length k. Thus, the DIV rule cannot be applied until all other variables are eliminated from \(I_1\). Thus, we must derive the constraint \(c_L \cdot p \cdot x_0 \le -c_L\). This derivation takes k steps and corresponds to a dag-like linear refutation of \(\textbf{I}\). This means that \(\textbf{I}\) has a dag-like linear refutation of length k. Thus, the IP-OLDR problem is NPO-hard.    \(\square \)

Since the IP-OLDR problem is NPO-hard, there exists an \(\epsilon >0\) such that the IP-OLDR cannot be approximated to within a factor of \(O(2^{n^\epsilon })\), unless P \(=\) NP [21]. Thus, the IP-OLDR cannot be approximated to within a polynomial factor, unless P \(=\) NP.

Note that in general, tree-like and dag-like cutting plane based refutations can be exponentially long [7]. Thus, these problems do not belong to the class NPO. However, we can show that both the IP-OLDR problem and the IP-OLTR problem belong to the class FPSPACE.

Theorem 4

The IP-OLTR problem is in FPSPACE.

Proof

Let \(\textbf{I}\) be an infeasible integer program with m constraints over n variables. We will show that a tree-like integer refutation of \(\textbf{I}\) can be constructed by a non-deterministic Turing Machine using working space polynomial in the size of \(\textbf{I}\). We know that any integer program has a tree-like integer refutation of length at most \(O(n^{3 \cdot n})\) [13]. Additionally, this refutation only needs to store polynomially many constraints at a time. Thus, each inference in a tree-like integer refutation can be identified using a number of bits polynomial in the size of the input integer program.

For each inference in a possible refutation R, we can non-deterministically guess the following:

  1. 1.

    The constraints used by the inference – Note that we can assume without loss of generality that the coefficients in these constraints have an absolute value of at most \((n \cdot C_1 + C_2)\) where \(C_1\) is the largest coefficient of any constraint in \(\textbf{I}\) and \(C_2\) is the largest defining constant [16]. Thus, each constraint can be represented using space polynomial in the size of \(\textbf{I}\).

  2. 2.

    The constraint produced by the inference.

  3. 3.

    The source of each constraint used by the inference – This is either the inference used to derive the constraint or the original integer program \(\textbf{I}\).

  4. 4.

    The inference that will use the derived constraint – Note that since the refutation is tree-like, there is at most one such inference.

Thus, each inference can be generated in polynomial space. Once each inference is generated, the space can then be reused to generate the next inference. Thus, the entire refutation can be generated using at most polynomial space.

The correctness of R can similarly be verified in polynomial space as follows:

  1. 1.

    Non-deterministically guess an inference in the refutation.

  2. 2.

    Verify that the derived constraint is correct for the given input constraints.

  3. 3.

    Verify that the input constraints come from the specified sources.

  4. 4.

    Verify that each source is either \(\textbf{I}\) or a previous inference.

  5. 5.

    For each constraint derived by a previous inference, verify that inference lists the current inference as using its derived constraint. Note that this ensures that derived constraints are not repeated.

This can be easily done in space polynomial in the size of \(\textbf{I}\). Once every inference in the refutation is verified, we know that the constraint derived by the last inference is derivable from the constraints in \(\textbf{I}\). If the last inference of R derives a contradiction, then R is a tree-like integer refutation of \(\textbf{I}\). By performing both the construction and verification procedures for each possible refutation length, the first tree-like integer refutation generated in this way is IP-OLTR of \(\textbf{I}\).    \(\square \)

Note that the refutations generated in the proof of Theorem 4 are tree-like because we ensure that each derived constraint is used by at most one future inference. If we remove this restriction, then the procedure instead generates dag-like integer refutations. This gives us the following corollary.

Corollary 1

The IP-OLDR problem is in FPSPACE.

6 Conclusion

In this paper, we studied the problems of finding optimal length refutations of infeasible integer programs (IPs). We looked at three different types of refutations, namely read-once refutations, tree-like refutations, and dag-like refutations.

Constraint systems are heavily used in the field of software verification [8, 12]. Refutations of these constraint systems provide evidence that the system is infeasible. Thus, refutations, especially short refutations, are also very useful in this field. As a result, the contributions in this paper will provide insights useful in software verification.

Specifically, we showed that the IP-OLRR problem is NPO PB-complete while the IP-OLTR and IP-OLDR problems are NPO-hard and in FPSPACE.

This paper only examined general forms of integer programs. However, restricting the form of the program can change the complexity of the problems examined. For example, in systems of difference constraints, the OLRR, OLTR, and OLDR problems for integer feasibility can be solved in polynomial time. Thus, future work can examine the complexity of these problems for other restricted IPs.