<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Archiving and Interchange DTD v1.0 20120330//EN" "JATS-archivearticle1.dtd">
<article xmlns:xlink="http://www.w3.org/1999/xlink">
  <front>
    <journal-meta />
    <article-meta>
      <title-group>
        <article-title>Computing the Integer Points of a Polyhedron (Extended Abstract)</article-title>
      </title-group>
      <contrib-group>
        <contrib contrib-type="author">
          <string-name>Rui-Juan Jing</string-name>
          <email>rjing8@uwo.ca</email>
          <xref ref-type="aff" rid="aff0">0</xref>
          <xref ref-type="aff" rid="aff1">1</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Marc Moreno Maza</string-name>
          <email>moreno@csd.uwo.ca</email>
          <xref ref-type="aff" rid="aff1">1</xref>
        </contrib>
        <aff id="aff0">
          <label>0</label>
          <institution>KLMM, UCAS, Academy of Mathematics and Systems Science, Chinese Academy of Sciences</institution>
        </aff>
        <aff id="aff1">
          <label>1</label>
          <institution>University of Western Ontario</institution>
        </aff>
      </contrib-group>
      <abstract>
        <p>Let K be a polyhedron in Rd, given by a system of m linear inequalities, with rational number coe cients bounded over in absolute value by L. We propose an algorithm for computing an irredundant representation of the integer points of K, in terms of \simpler" polyhedra, each of them having at least one integer point. Using the terminology of W. Pugh: for any such polyhedron P , no integer point of its grey shadow extends to an integer point of P . We show that, under mild assumptions, our algorithm runs in exponential time w.r.t. d and in polynomial w.r.t m and L. We report on a software experimentation.</p>
      </abstract>
    </article-meta>
  </front>
  <body>
    <sec id="sec-1">
      <title>Introduction</title>
      <p>
        The integer points of polyhedral sets are of interest in many areas of
mathematical sciences, see for instance the landmark textbooks of A. Schrijver [
        <xref ref-type="bibr" rid="ref25">19</xref>
        ] and
A. Barvinok [
        <xref ref-type="bibr" rid="ref4 ref9">3</xref>
        ], as well as the compilation of articles [
        <xref ref-type="bibr" rid="ref10 ref5">4</xref>
        ]. One of these areas
is the analysis and transformation of computer programs. For instance, integer
programming [
        <xref ref-type="bibr" rid="ref13">7</xref>
        ] is used by P. Feautrier in the scheduling of for-loop nests [
        <xref ref-type="bibr" rid="ref14">8</xref>
        ]
Barvinok's algorithm [
        <xref ref-type="bibr" rid="ref3 ref8">2</xref>
        ] for counting integer points in polyhedra is adapted by
M. Koppe and S. Verdoolaege in [
        <xref ref-type="bibr" rid="ref22">16</xref>
        ] to answer questions like how many memory
locations are touched by a for-loop nest. In [
        <xref ref-type="bibr" rid="ref23">17</xref>
        ], W. Pugh proposes an algorithm,
called the Omega Test, for testing whether a polyhedron has integer points. In
the same paper, W. Pugh shows how to use the Omega Test for performing
dependence analysis [
        <xref ref-type="bibr" rid="ref23">17</xref>
        ] in for-loop nests. Then, in [
        <xref ref-type="bibr" rid="ref24">18</xref>
        ], he uses the Omega Test
for deciding Presburger arithmetic formulas.
      </p>
      <p>
        In [
        <xref ref-type="bibr" rid="ref24">18</xref>
        ], W. Pugh also suggests, without stating a formal algorithm, that the
Omega Test could be used for quanti er elimination on Presburger formulas.
This observation is a rst motivation for the work presented in this paper: we
adapt the Omega Test so as to describe the integer points of a polyhedron via
a projection scheme, thus performing elimination of existential quanti ers on
Presburger formulas.
      </p>
      <p>
        Projections of polyhedra and parametric programming are tightly related
problems, see [
        <xref ref-type="bibr" rid="ref18">12</xref>
        ]. Since the latter is essential to the parallelization of for-loop
nests [
        <xref ref-type="bibr" rid="ref13">7</xref>
        ], which is of interest to the authors [
        <xref ref-type="bibr" rid="ref11 ref6">5</xref>
        ], we had here a second motivation
for developing the proposed algorithm.
      </p>
      <p>
        In [
        <xref ref-type="bibr" rid="ref15">9</xref>
        ], M. J. Fischer and M. O. Rabin show that any algorithm for
deciding Presburger arithmetic formulas has a worst case running time which is a
doubly exponential in the length of the input formula. However, this worst case
scenario is based on a formula alternating existential and universal quanti ers.
Meanwhile, in practice, the original Omega Test (for testing whether a
polyhedron has integer points) can solve \di cult problems" as shown by W. Pugh
in [
        <xref ref-type="bibr" rid="ref24">18</xref>
        ] and others, e.g. D. Wonnacott in [
        <xref ref-type="bibr" rid="ref26">20</xref>
        ]. This observation brings our third
motivation: determining realistic assumptions under which our algorithm, based
on the Omega Test, could run in a single exponential time.
      </p>
      <p>Our algorithm takes as input a system of linear inequalities Ax ≤ b where
A is a matrix over Z with m rows and d columns, x is the unknown vector
and b is a vector of m coe cients in Z. The points x ∈ Rd satisfying Ax ≤ b
form a polyhedron K and our algorithm decomposes its integer points (that
is, K ∩ Zd) into a disjoint union K1 ∩ Zd ⊍ ⋯ ⊍ Ke ∩ Zd, where K1; : : : ; Ke
are \simpler" polyhedra such that Ki ∩ Zd ≠ ∅ holds, for 1 ≤ i ≤ e. To use the
terminology introduced by W. Pugh for the Omega test, for 1 ≤ i ≤ e, no integer
point of the grey shadow of the polyhedron Ki extends to an integer point of
Ki. As a consequence, applying our algorithm to Ki would return Ki itself, for
1 ≤ i ≤ e. Let us present the key principles and features of our algorithm through
an example. Consider the polyhedron K of R4 given below:
⎧⎪ 2x + 3y − 4z + 3w ≤ 1
⎪
⎪⎪⎪⎪⎪ −2x − 3y + 4z − 3w ≤ −1
⎪
⎪⎪⎪⎪⎪−13x − 18y + 24z − 20w ≤ −1 :
⎪⎪⎨−26x − 40y + 54z − 39w ≤ 0
⎪
⎪
⎪⎪⎪⎪−24x − 38y + 49z − 31w ≤ 5
⎪
⎪
⎪⎪⎪ 54x + 81y − 109z + 81w ≤ 2
⎩
A rst procedure, called IntegerNormalize, detect implicit equations and solve
them using techniques based on Hermite normal form, see Sect. 3. In our example
2x+3y−4z+3w = 1 is an implicit equation and IntegerNormalize(Ax ≤ b) returns a
triple (t; x = Pt+ q; Mt ≤ v) where t is a new unknown vector, the linear system
x = Pt+q gives the general form of an integer solution of the implicit equation(s)
and Mt ≤ v is obtained by substituting x = Pt + q into Ax ≤ b. In our example,
the systems x = Pt + q and Mt ≤ v are given by:
⎪⎪⎧⎪ x = −3t1 + 2t2 − 3t3 + 2 ⎪⎪⎧⎪ 3t1 − 2t2 + t3 ≤ 7
⎪⎪⎪⎪ y = 2t1 + t3 − 1 and ⎪⎪⎪⎪−2t1 + 2t2 − t3 ≤ 12 :
⎪⎪⎪⎩⎪⎨⎪⎪⎪wz == tt32 ⎩⎪⎪⎪⎪⎪⎪⎪⎨−4t1 + t2 + −3tt23 ≤≤ 1−525
A second procedure, called DarkShadow, takes Mt ≤ v as input and returns a
couple (t′; ) where t′ stands for all t-variables except t1, and is a linear
system in the t′-variables such that any integer point solving of extends to an
integer point solving Mt ≤ v. In our example, t′ = {t2; t3} and is given by:
The polyhedron D of R2 de ned by , and the inequalities of Mt ≤ v not
involving t1, is called the dark shadow of the polyhedron de ned by Mt ≤ v. On
the left-hand side of Fig. 1, one can see the polyhedron de ned in R3 by Mt ≤ v
together with its dark shadow D (shown in dark blue) as well as its projection on
the (t2; t3)-plane, denoted by R and called real shadow by W. Pugh. The
righthand side of Fig. 1 gives a planar view of D and R. It turns out that, if M′t′ ≤ v′
is the linear system generated by applying Fourier-Motzkin elimination (without
removing redundant inequalities) to Mt ≤ v (in order to eliminate t1), then
is given by a linear system of the form M′t′ ≤ w′. This explains why, on the
right-hand side of Fig. 1, each facet of the dark shadow D is parallel to a facet
of the real shadow R. While this property is observed on almost all practical
problems, in particular in the area of analysis and transformation of computer
programs, it is possible to build examples where this property does not hold.</p>
      <p>On the right-hand side of Fig. 1, one observes that the region R ∖ D, called
grey shadow, contains integer points. Some of them, like (t2; t3) = (29; 9), do
not extend to an integer solution of Mt ≤ v. Indeed, plugging (t2; t3) = (29; 9)
into Mt ≤ v yields 327 ≤ t1 ≤ 3</p>
      <p>56 , which has no integer solutions. However, other
integer points of R ∖ D may extend to integer solutions of Mt ≤ v. In order
to determine them, a third procedure, called GreyShadow, is needed. We give
a disjoint decomposition of grey shadow by negating each inequality of in
turn. Then, compute the integer points in each disjoint part. Details are given
in Sect. 4.</p>
      <p>Returning to our example, the negation of the inequality 2t2 − t3 ≤ 48 from
, combined with the system Mt ≤ v, yields the following</p>
      <p>
        ⎪⎪⎪⎪⎩⎨⎪⎪⎪⎧⎪ttt321 === tt−542+t41+ 2t5 + 1 ; and ⎪⎪⎨⎪⎪⎪⎪⎩⎪⎪⎪⎪⎪⎪⎪⎪⎧−1−0t24t4+−−7tttt5554 ≤≤≤≤ 18−−12448 ;
where t4; t5 are new variables. Continuing in this manner with the GreyShadow
procedure, a decomposition of the integer points of Mt ≤ v is given by:
⎧⎪ 3t1 − 2t2 + t3 ≤ 7
⎪
⎪
⎪⎪⎪⎪−2t1 + 2t2 − t3 ≤ 12
⎪⎪⎪⎪⎪⎪⎪⎪⎪⎪⎪⎨⎪⎪⎪⎪⎪⎪⎪⎪⎪⎪−4t−15+t2t22t+2+1−−33tttt3332 ≤≤≤≤ 146−58725 ; ⎪⎪⎪⎪⎩⎪⎨⎪⎧⎪⎪ttt321 === 121675 ; ⎪⎪⎪⎪⎩⎪⎨⎪⎧⎪⎪ttt321 === 131838 ; ⎪⎪⎪⎪⎩⎪⎨⎪⎧⎪⎪ttt213 === 121554 ; ⎪⎪⎪⎪⎪⎪⎪⎩⎪⎨⎪⎪⎧⎪⎪⎪⎪−25ttt≤321t===6 551≤009−++16t26:t6 :
⎪
⎩⎪⎪⎪ 2 ≤ t3 ≤ 17
Denoting these ve systems respectively by S1; : : : ; S5 the integer points of K are
nally given by the union of the integer points of the systems x = Pt + q ∪ Si,
for 1 ≤ i ≤ 5. The systems S2; : : : ; S5 look simple enough to be considered as
solution sets. What about S1? The system S1, as well as S2; : : : ; S5, satis es a
\back-substitution" property which is similar to that of a regular chain in the
theory of polynomial system solving [
        <xref ref-type="bibr" rid="ref1 ref2 ref7">1</xref>
        ]. This property, when applied to S1, says
that for all 1 ≤ i ≤ 2, every integer point of Ri solving all the inequalities of
i 1 solving all the
S1 involving t1; : : : ; ti only, extends to an integer point of R +
inequalities of S1 involving t1; : : : ; ti+1.
      </p>
      <p>
        With respect to the original Omega Test [
        <xref ref-type="bibr" rid="ref23">17</xref>
        ], our contributions are as follows.
1. We turn the decision procedure of the Omega Test into an algorithm
decomposing all the integer points of a polyhedron.
2. Our decomposition is disjoint whereas the recursive calls in the original
      </p>
      <p>Omega Test may search for integer points in intersecting polyhedral regions.
3. The original Omega Test uses an ad-hoc routine for computing the integer
solutions of linear equation systems, while we rely on Hermite normal form
for this task. Consequently, we deduce complexity estimates for that task.
4. We also provide complexity estimates for the procedures GreySahdow and
DarkShadow under realistic assumptions. From there, we derive complexity
estimates for the entire algorithm, whereas no complexity estimates were
known for the original Omega Test.
Our algorithm is discussed in Sect. 3 and 4 while complexity estimates are stated
in Sect. 5. Sect. 2 gathers background materials on polyhedra.
2</p>
    </sec>
    <sec id="sec-2">
      <title>Polyhedral Sets</title>
      <p>
        This section is a review of the theory of polyhedral sets. It is based on the books
of B. Grunbaum [
        <xref ref-type="bibr" rid="ref16">10</xref>
        ] and A. Schrijver [
        <xref ref-type="bibr" rid="ref25">19</xref>
        ], where proofs of the statements below
can be found.
      </p>
      <p>Given a positive integer d, we consider the d-dimensional Euclidean space Rd
equipped with the Euclidean topology. Let K be a subset of Rd. The dimension
dim(K) of K is a − 1 where a is the maximum number of a nely independent
pointsxin∈ KR.dLSetaTax∈ =Rbd, .leWteb ∈saRy athnadt dtehneotheypbeyrpHlantheeHhyspueprppolratnse Kdeifneeidthbeyr
H = { }
sup{aT x S x ∈ K} = b or inf{aT x S x ∈ K} = b holds, but not both.</p>
      <p>From now on, let us assume that K is convex. A set F ⊆ K is a face if either
F = ∅ or F = K, or if there exists a hyperplane H supporting K such that we
have F = K ∩ H. The set of all faces of K is denoted by F (K). We say that
F ∈ F (K) is proper if we have F ≠ ∅ or F ≠ K. We note that the intersection of
any family of faces of K is itself a face of K.</p>
      <p>We say that K is a polyhedral set or polyhedron if it is the intersection of
nitely many closed half-spaces of Rd. We say that K is full-dimensional, if we
have dim(K) = d, that is, if the interior of K is not empty. The proper faces of
K that are ⊆-maximal are called facets and those of dimension zero are called
vertices. We observe that every face of K is also a polyhedral set.</p>
      <p>Let H1; : : : ; Hm be closed half-spaces such that the intersection ∩ii==1m Hi is
irredundant, that is, ∩ii==1m Hi ≠ ∩i==1m;j≠i Hi for all 1 ≤ j ≤ m. We observe that this
i
intersection is closed and convex. For each i, where 1 ≤ i ≤ m, let ai ∈ Rd and
bi ∈ R such that Hi is de ned by aiT x ≤ bi. We denote by A the m × d matrix
(aiT ; 1 ≤ i ≤ m) and by b the vector (b1; : : : ; bd)T .</p>
      <p>
        From now on, we assume that K = ∩ii==1m Hi holds. Such irredundant
decomposition of a polyhedral set can be computed from an arbitrary intersection of
nitely many closed half-spaces, in time polynomial in both d and m, using linear
programming; see L. Khachian in [
        <xref ref-type="bibr" rid="ref21">15</xref>
        ]. The following property is essential. For
every face F of K, there exists a subset I of {1; : : : ; m} such that F corresponds
to the set of solutions to the system of equations and inequalities
aiT x = bi for i ∈ I; and aiT x ≤ bi for i ∈~ I :
This latter property has several important consequences. For each i 1 ≤ i ≤ m,
the set Fi = K ∩ Hi is a facet of K and the border of K equals ∪ii==1m Fi. In
particular, each proper face of K is contained in a facet of K. Each facet of a
facet of K is the intersection of two facets of K. Moreover, if the m × d-matrix
A has rank d (full column rank) then the ⊆-minimal faces are the vertices. The
set F (K) is nite and has at most 2m elements
      </p>
      <p>For a ∈ Rd and b ∈ R, we say that aT x ≤ b is an implicit equation in Ax ≤ b
if for all x ∈ Rd we have</p>
      <p>
        Ax ≤ b
Ô⇒
aT x = b :
(1)
Following [
        <xref ref-type="bibr" rid="ref25">19</xref>
        ], we denote by A= (resp. A+) and b= (resp. b+) the rows of A
and b corresponding to the implicit equations (resp. inequalities). The following
properties are easy to prove. If K is not empty, then there exists x ∈ K satisfying
both
      </p>
      <p>A=x = b=</p>
      <p>and A+x &lt; b+ :
The facets of K are in 1-to-1 correspondence with the inequalities of A+x ≤
b+. In addition, if K is full-dimensional, then A+ = A and b+ = b both hold;
moreover the system of inequalities Ax ≤ b is a unique representation of K, up
to multiplication of inequalities by positive scalars.</p>
      <p>
        From now on and in the sequel of this paper, we assume that variables are
ordered as x1 &gt; ⋯ &gt; xd. We call initial coe cient, or simply initial, of an
inequality aiT x ≤ bi, for 1 ≤ i ≤ m, the coe cient of aiT x in its largest variable.
Following the terminology of W. Pugh in [
        <xref ref-type="bibr" rid="ref23">17</xref>
        ], if v is the largest variable of the
inequality aiT x ≤ bi, we say that this inequality is an upper (resp. lower) bound
of v whenever the initial c of aiT x ≤ bi is positive (resp. negative); indeed, we
have v ≤ c (resp. v ≥ c ) where = bi − aiT x + c v.
      </p>
      <p>Canonical representation. Recall that we assume that none of the inequalities
of Ax ≤ b is redundant. If K is full-dimensional and if the initial of each inequality
in Ax ≤ b is 1 or −1, then we call Ax ≤ b the canonical representation of K w.r.t.
the variable ordering x1 &gt; ⋯ &gt; xd and we denote it by can(K; x1; : : : ; xd).</p>
      <p>We observe that the notion of canonical representation can also be expressed
in a more geometrical and less algebraic way, that is, independently of any
coordinate system. Assume again that K is full-dimensional and that the
intersection ∩ii==1n Hi = K of closed half-spaces H1; : : : ; Hn is irredundant. Since K
is full-dimensional, the supporting hyperplane of each facet of K must be the
frontier of one half-space among H1; : : : ; Hn. Clearly, two (or more) half-spaces
among H1; : : : ; Hn may not have the same frontier without contradicting one of
our hypotheses (K is full-dimensional, ∩ii==1n Hi is irredundant). Therefore, the
half-spaces H1; : : : ; Hn are in one-to-one correspondence with the facets of K.
This implies that there is a unique irredundant intersection of closed half-spaces
equaling K and we denote it by can(K).</p>
      <p>
        Projected representation. Let again Ax ≤ b be a canonical representation of
the polyhedral set K w.r.t. the variable ordering x1 &gt; ⋯ &gt; xd. We denote by
Ax1 (resp. A&lt;x1 ) and bx1 (resp. b&lt;x1 ) the rows of A and b corresponding to
the inequalities whose largest variable is x1 (resp. less than x1). For each upper
bound cx1 ≤ of x1 and each lower bound −ax1 ≤ − of x1 (where c &gt; 0,
a &gt; 0, ∈ R[x2; : : : ; xd] and ∈ R[x2; : : : ; xd] hold), we have a new inequality
c −a ≤ 0. Augmenting A&lt;x1 with all inequalities obtained in this way, we obtain
a new linear system which represents a polyhedral set which is the standard
projection of K on the d − 1 least coordinates of Rd, namely (x2; : : : ; xd); hence
we denote this latter polyhedral set by x2;:::;xd K and we call it the real shadow
of K, following the terminology of [
        <xref ref-type="bibr" rid="ref23">17</xref>
        ]. The procedure by which x2;:::;xd K
is computed from K is the well-known Fourier-Motzkin elimination procedure,
see [
        <xref ref-type="bibr" rid="ref21">15</xref>
        ]. We call projected representation of K w.r.t. the variable ordering x1 &gt;
⋯ &gt; xd and denote by proj(K; x1; : : : ; xd) the linear system given by Ax1 x ≤ bx1
if d = 1 and, by the conjunction of Ax1 x ≤ bx1 and proj( x2;:::;xd K; x2; : : : ; xd),
otherwise.
3
      </p>
    </sec>
    <sec id="sec-3">
      <title>Integer Solutions of Linear Equation Systems</title>
      <p>
        We review how Hermite normal forms [
        <xref ref-type="bibr" rid="ref12 ref25">6, 19</xref>
        ] can be used to represent the integer
solutions of systems of linear equations. Let A = (ai;j ) and H = (hi;j ) be two
matrices over Z with m rows and d columns, and let b be a vector over Z with
d coe cients. We denote by r the rank of A and by h the maximum bit size of
coe cients in the matrix [A b]. De nition 1 is taken from [
        <xref ref-type="bibr" rid="ref19">13</xref>
        ], see also [
        <xref ref-type="bibr" rid="ref17">11</xref>
        ].
De nition 1. The matrix H is called a column Hermite normal form (abbr.
column HNF) if there exists a strictly increasing map f from [d − r + 1; d] ∩ Z to
[1; m] ∩ Z satisfying the following properties for all j ∈ [d − r + 1; d] ∩ Z:
1. for all integer i such that i &gt; f (j) holds, we have hi;j = 0,
2. for all integer k such that j &lt; k ≤ d holds, we have hf(j);j &gt; hf(j);k ≥ 0,
3. the rst d − r columns of H are equal to zero.
      </p>
      <p>We say that H is the column Hermite normal form of A if H is a column Hermite
normal form and there exists a uni-modular d × d-matrix U over Z such that we
have H = AU . When those properties hold, we call {f (d − r + 1); : : : ; f (d)} the
pivot row set of A.</p>
      <p>Remark 1. The matrix A admits a unique column Hermite normal form. Let H
be this column Hermite normal form and let U be the uni-modular d × d-matrix
given in De nition 1. Let us decompose U as U = [UL; UR] where UL(resp. UR)
consist of the rst d − r (resp. last r) columns of U . Then we de ne HL ∶= AUL
and HR ∶= AUR. We have HL = 0m;d−r, where 0m;d−r is the zero-matrix with
m rows and d − r columns. We observe that UR is a full column-rank matrix.
Moreover, if A is full row-rank, that is, if r = m holds, then UR is non-singular.</p>
      <p>
        Lemma 2 shows how to compute the integer solutions of the system of linear
equations Ax = b when A is full rank. In the general case, one can use Lemma 1
to reduce to the hypothesis of Lemma 2. While the construction of this latter
lemma relies on the HNF, alternative approaches are available. For instance, one
can use the equation elimination procedure of the Omega Test [
        <xref ref-type="bibr" rid="ref23">17</xref>
        ], However, no
running-time estimates is known for that procedure.
      </p>
      <p>Notation 1 For I ⊆ {1; : : : ; m}, we denote by AI (resp. bI ) the sub-matrix
(resp. vector) of A (resp. b) consisting of the rows of A (coe cients of b) with
indices in I.</p>
      <p>Lemma 1. Let I be the pivot row set of A, as given in De nition 1. Assume
that Ax = b admits at least one solution in Rd. Then, for any x ∈ Rd, we have
Ax = b
⇐⇒</p>
      <p>AI x = bI :
Lemma 2. We use the same notations as in De nition 1 and Remark 1. We
assume that HR is non-singular. Then, the system Ax = b has an integer solution
if and only if HR−1b is integral. In this case, all integral solutions to Ax = b are
given by x = P t + q where
1. the columns of P consist of a Z-basis of the space {x ∶ Ax = 0},
2. q is a particular solution of Ax = b, and
3. t = (t1; : : : ; td−r) is a vector of d − r unknowns.</p>
      <p>The maximum absolute value of any coe cient in P (resp. q) can be bounded
over by rr+1L2r (resp. rr+1L2r), where L is the maximum absolute value of a
coe cient in A (resp. in either A or b). Moreover, P and q can be computed
within O(mdr2(log r + log L)2 + r4(log r + log L)3) bit operations.</p>
      <sec id="sec-3-1">
        <title>Example 1. Let A, H and U be as follows:</title>
        <p>The matrix H is the column HNF of A, with unimodular matrix U and pivot
row set [2; 4; 5]. We denote by HR the sub-matrix of H whose coe cients are
in bold fonts. Applying Lemma 1, we deduce that for any vector b such that
Ax = b admits one rational solution, we have:
⎧⎪ 3x1 + 4x2 − 4x3 − x4 = b1
⎪
⎪⎪⎪⎪⎪⎪2x1 − 2x2 + 8x3 + 4x4 = b2 ⎪⎧⎪2x1 − 2x2 + 8x3 + 4x4 = b2
⎪⎨⎪5x1 + 2x2 + 4x3 + 3x4 = b3 ⇔ ⎨⎪⎪3x1 + 5x2 − 5x3 − 2x4 = b4 :
⎪⎪⎪⎪⎪⎪⎪3x1 + 5x2 − 5x3 − 2x4 = b4 ⎪⎪⎪⎪⎩2x1 − 3x2 + 9x3 + 5x4 = b5
⎪⎪⎪2x1 − 3x2 + 9x3 + 5x4 = b5
⎩
We apply Lemma 2: if Ax = b is consistent over Q and if HR−1[b2; b4; b5]T is
integral, then all the integer solutions of the second equation system in Relation (2)
are given by x = Pt + q, where P = [−1; 1; 0; 1]T , q = [ 53 b2 − 139 b4 − 1535 b5; − 1387 b2 +
793 b4 + 5795 b5; − 1189 b2 + 397 b4 + 2996 b5]T , t = (t1) and t1 is a new variable.
4</p>
      </sec>
    </sec>
    <sec id="sec-4">
      <title>Integer Solutions of Inequality Systems</title>
      <p>
        In this section, we present an algorithm for computing the integer points of a
polyhedron K ⊆ Rd, that is, the set K ∩ Zd. As mentioned in the introduction,
we adapt the Omega Test invented by W. Pugh [
        <xref ref-type="bibr" rid="ref23">17</xref>
        ] for deciding whether or not
a polyhedral set has an integer point.
      </p>
      <p>With the notations of Section 2, consider again the polyhedron K:
(2)
⎧ a11x1 + ⋯ + a1dxd ≤ b1
⎪
⎪
⎪⎨ ⋮
⎪⎪⎪ am1x1 + ⋯ + amdxd ≤ bm
⎩
We aim at eliminating x1, so we consider two inequalities in x1:
{ one with ai1 &gt; 0, called upper bound:</p>
      <p>li ∶ ai1x1 + ⋯ + aidxd ≤ bi,
{ another one with aj1 &lt; 0, called lower bound:</p>
      <p>lj ∶ aj1x1 + ⋯ + ajdxd ≤ bj.</p>
      <p>The real projection makes a linear combination rij of li and lj:</p>
      <p>− aj1(ai2x2 + ⋯ + aidxd) + ai1(aj2x2 + ⋯ + ajdxd) ≤ −aj1bi + ai1bj.
The dark projection translates rij towards the center of K into dsij:
−aj1(ai2x2+⋯+aidxd)+ai1(aj2x2+⋯+ajdxd) ≤ −aj1bi+ai1bj−(ai1 − 1)(−aj1 − 1).
Lemma 3. For any integer point (x2; : : : ; xd) ∈ Zd−1 satisfying dsij, there exists
at least one integer x1 ∈ Z satisfying both li and lj.</p>
      <p>Let S&lt;x1 be the subset of the inequalities de ning K in which x1 does not
occur. Combining all the real projections with S&lt;x1 , we obtain the so-called
real shadow of the polyhedron K w:r:t: x1, that we denote by R. Meanwhile,
combining all the dark projections with S&lt;x1 , we obtain the so-called dark shadow
of the polyhedron K w:r:t: x1, that we denote by D. Without loss of generality,
we assume D = S&lt;x1 ∩ ds1 ∩ ⋯ ∩ dst, where t is a positive integer and each
dsi is a dark projection introduced above for 1 ≤ i ≤ t. Obviously, we have
D = R ∩ ds1 ∩ ⋯ ∩ dst since D ⊂ R ⊂ S&lt;x1 .</p>
      <p>We de ne the grey shadow of K w.r.t. x1 as G ∶= R ∖ D. Then, it is easy
to deduce that G = Gi, where " means disjoint union and Gi = R ∩ ds1 ∩
1 "i t
≤ ≤
⋯ ∩ dsi−1 ∩ ¬dsi, here ¬dsi is the negation of dsi for 1 ≤ i ≤ t. We call each Gi
obtained by this way a grey shadow part of K.</p>
      <p>We use the following steps to introduce the ideas of procedure GreyShadow:
1. let result ∶= {};
2. for each lower bound aj1x1 + ⋯ + ajdxd ≤ bj of x1 in K1
3. for each upper bound ai1x1 + ⋯ + aidxd ≤ bi of x1 in K1
4. for each integer ` from 1 to ⌊(−aj1ai1 + aj1 − ai1)~ai1⌋ do
5. let gji` ∶ aj1x1 + ⋯ + ajdxd = bj − `;
6. solving for the integer solutions of gji`, we obtain a solution of the
form x = Pt + q;
7. substitute x = Pt + q into K ∩ ¬dsji, we obtain a new polyhedron K1;
8. let result = result ∪ {x = Pt + q ∩ K1};
9. end for;
10. let K = K ∩ dsji;
11. end for;
12. end for;
13. return result.</p>
      <p>Example 2. Given a polyhedron K:</p>
      <p>,
⎪⎪⎨−4x1 + x2 + 3x3 ≤ 15
⎪
⎪
⎩⎪⎪⎪ −x2 ≤ −25
we have one upper bound and two lower bounds for x1. For the lower bound
−2x1 + 2x2 − x3 ≤ 12 and the upper bound 3x1 − 2x2 + x3 ≤ 7, we have ⌊(−aj1ai1 +
aj1 − ai1)~ai1⌋ = 0. Thus, one recursive call with:
⎧⎪−2x1 + 2x2 − x3 = 12
⎪
⎪
⎪⎪⎪ 3x1 − 2x2 + x3 ≤ 7
⎪ .
⎪⎪⎨−4x1 + x2 + 3x3 ≤ 15
⎪
⎪
⎪⎪⎩⎪ −x2 ≤ −25
Solving −2x1 + 2x2 − x3 = 12 via Hermite normal form leads to:
⎧⎪⎪x1 = x4
⎪
⎪⎨x2 = x5 + 1
⎪
⎪⎪⎪⎩x3 = −2x4 + 2x5 + 1
,
where x4; x5 are new variables. Thus, the grey shadow part G20 is:
⎪⎧⎪ x4 ≤ 8
⎪
⎪⎨−10x4 + 7x5 ≤ 11 .
⎪
⎪⎪⎩⎪ −x5 ≤ −24
Befor compute the other grey shadow parts generated by any other lower bounds,
we add the dark projection 2x2 − x3 ≤ 48 to the polyhedron K. For the lower
bound −4x1 + x2 + 3x3 ≤ 15, we have ⌊(−aj1ai1 + aj1 − ai1)~ai1⌋ = 1, yielding two
other grey shadow parts, which are disjoint with G20.
5</p>
    </sec>
    <sec id="sec-5">
      <title>Complexity Analysis</title>
      <sec id="sec-5-1">
        <title>We use the following gure to illustrate our algorithm:</title>
        <p>Notation 2 Fig. 2 illustrates the tree of recursive calls for the main algorithm,
the IntegerSolve procedure. The root of the tree is labelled with S, which stands
for the input system. The left (resp. right) child of a node, other than a leaf, is
labelled by D (resp. G) which stands for the output of the DarkShadow procedure
(resp. the GreyShadow procedure). Since the DarkShadow procedure generates one
input, we use a simple → arrow as an edge to a D-node. However, the GreyShadow
procedure may generate several inputs, leading to several recursive calls. Thus,
we use a ⇒ arrow as an edge to a G-node. The numbers on the right-hand side
of Fig. 2 stand for the levels in the tree.</p>
        <p>Hypothesis 1 We assume that during the execution of the function call
IntegerSolve(K), for any polyhedral set K′, input of a recursive call, each facet of the
dark shadow of K′ is parallel to a facet of the real shadow of K′.</p>
        <p>D G</p>
        <p>d − 1</p>
        <p>
          To state our main result, we need a notation for the running time of solving
a linear program. Indeed, linear programming is an essential tool for removing
redundant inequalities generated by Fourier-Motzkin elimination, see [
          <xref ref-type="bibr" rid="ref21">15</xref>
          ].
Notation 3 For an input linear program with total bit size H and with d
variables, we denote by LP(d; H) an upper bound for the number of bit operations
required for solving this linear program. For instance, in the case of Karmarkar's
algorithm [
          <xref ref-type="bibr" rid="ref20">14</xref>
          ], we have LP(d; H) ∈ O(d3:5H2 ⋅ log H ⋅ log log H).
        </p>
        <p>Lemma 4. Let 0 ≤ k &lt; d be an integer. Let fd;m;k be the number of k-dimensional
faces of K. Then, we have
m
fd;m;k ≤ d − k:
Therefore, we have</p>
        <p>fd;m;0 + fd;m;1 + ⋯ + fd;m;d−1 ≤ md:
Lemma 5. Any path in Fig. 2 can be implemented within O(m2r+2d3+"r10(log d+
log L)3) + O(rm2r+2LP(d; dmrr3(log d + log L))) bit operations.</p>
      </sec>
      <sec id="sec-5-2">
        <title>Let Tr be the total number of nodes in the r-th level.</title>
        <p>Lemma 6. We have: Tr+1 ≤ mr+1drr2r2 L3r2 Tr for 0 ≤ r ≤ d − 2. Thus, we have
Td−1 ≤ md2 d3d3 L3d3 .</p>
        <p>Theorem 1. Under Hypothesis 1, the call function IntegerSolve(K) runs within
O(m2d2 d4d3 L4d3 LP(d; mdd4(log d + log L))) bit operations.
6</p>
      </sec>
    </sec>
    <sec id="sec-6">
      <title>Experimentation</title>
      <p>We have implemented the algorithm presented in the rst paper within the
Polyhedra library in Maple. This library is publicly available in source on the
download page of the RegularChains library at www.regularchains.org</p>
      <p>In this section, we gather experimental results obtained with our
implementations. Our objectives were two-fold:
Example</p>
    </sec>
  </body>
  <back>
    <ref-list>
      <ref id="ref1">
        <mixed-citation>
          1.
          <string-name>
            <surname>Check</surname>
          </string-name>
          <article-title>on various test-cases whether or not Hypothesis 1 holds,</article-title>
        </mixed-citation>
      </ref>
      <ref id="ref2">
        <mixed-citation>
          <article-title>1. Hypothesis 1 holds for most examples while it ussually does not hold for random ones</article-title>
          .
        </mixed-citation>
      </ref>
      <ref id="ref3">
        <mixed-citation>
          2.
          <article-title>For 16 out of 27 examples, IntegerSolve produces a single component, which means that each such input polyhedron has no integer points in its grey shadow; this is, in particular the case for regular polytopes and for examples from automatic parallelization</article-title>
          .
        </mixed-citation>
      </ref>
      <ref id="ref4">
        <mixed-citation>
          3.
          <string-name>
            <surname>When</surname>
          </string-name>
          <article-title>a decomposition consists of more than one components, most of those components are points; for example, the decomposition of Unbounded 2 has 61 components and 46 of them are points</article-title>
          .
        </mixed-citation>
      </ref>
      <ref id="ref5">
        <mixed-citation>
          4.
          <article-title>Coe cients of the output polyhedra are usually not much larger than the coe cients of the corresponding input polyhedron</article-title>
          .
        </mixed-citation>
      </ref>
      <ref id="ref6">
        <mixed-citation>
          <article-title>5. Among the challnging problems, some of them are solved faster when IntegerNormalize is based on HNF (e.g. Bounded 7) while others are solved faster when IntegerNormalize is based on Pugh's method (e.g. Bounded 9) which suggests that having both approaches at hand is useful</article-title>
          .
        </mixed-citation>
      </ref>
      <ref id="ref7">
        <mixed-citation>
          [1]
          <string-name>
            <given-names>P.</given-names>
            <surname>Aubry</surname>
          </string-name>
          ,
          <string-name>
            <given-names>D.</given-names>
            <surname>Lazard</surname>
          </string-name>
          , and
          <string-name>
            <given-names>M. Moreno</given-names>
            <surname>Maza</surname>
          </string-name>
          .
          <article-title>On the theories of triangular sets</article-title>
          .
          <source>J. Symb. Comput.</source>
          ,
          <volume>28</volume>
          :
          <fpage>105</fpage>
          {
          <fpage>124</fpage>
          ,
          <year>July 1999</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref8">
        <mixed-citation>
          [2]
          <string-name>
            <surname>Alexander</surname>
            <given-names>I. Barvinok.</given-names>
          </string-name>
          <article-title>A polynomial time algorithm for counting integral points in polyhedra when the dimension is xed</article-title>
          .
          <source>Math. Oper. Res.</source>
          ,
          <volume>19</volume>
          (
          <issue>4</issue>
          ):
          <volume>769</volume>
          {
          <fpage>779</fpage>
          ,
          <year>1994</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref9">
        <mixed-citation>
          [3]
          <string-name>
            <surname>Alexander</surname>
            <given-names>I.</given-names>
          </string-name>
          <string-name>
            <surname>Barvinok</surname>
          </string-name>
          . Integer Points in Polyhedra.
          <source>Contemporary mathematics. European Mathematical Society</source>
          ,
          <year>2008</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref10">
        <mixed-citation>
          [4]
          <string-name>
            <given-names>M.</given-names>
            <surname>Beck</surname>
          </string-name>
          . Integer Points in Polyhedra{ Geometry, Number Theory, Representation Theory, Algebra, Optimization, Statistics:
          <string-name>
            <surname>AMS-IMS-SIAM Joint</surname>
          </string-name>
          Summer Research Conference, June 11-15,
          <year>2006</year>
          , Snowbird, Utah.
          <source>Contemporary mathematics - American Mathematical Society. American Mathematical Society</source>
          ,
          <year>2008</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref11">
        <mixed-citation>
          [5]
          <string-name>
            <given-names>Changbo</given-names>
            <surname>Chen</surname>
          </string-name>
          , Xiaohui Chen,
          <string-name>
            <surname>Abdoul-Kader</surname>
            <given-names>Keita</given-names>
          </string-name>
          , Marc Moreno Maza, and Ning Xie.
          <article-title>MetaFork: A compilation framework for concurrency models targeting hardware accelerators and its application to the generation of parametric CUDA kernels</article-title>
          .
          <source>In Proceedings of CASCON 2015</source>
          , pages
          <fpage>70</fpage>
          {
          <fpage>79</fpage>
          ,
          <year>2015</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref12">
        <mixed-citation>
          [6]
          <string-name>
            <given-names>Henri</given-names>
            <surname>Cohen</surname>
          </string-name>
          .
          <article-title>A course in computational algebraic number theory</article-title>
          , volume
          <volume>138</volume>
          . Springer Science &amp; Business
          <string-name>
            <surname>Media</surname>
          </string-name>
          ,
          <year>2013</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref13">
        <mixed-citation>
          [7]
          <string-name>
            <given-names>Paul</given-names>
            <surname>Feautrier</surname>
          </string-name>
          .
          <article-title>Parametric integer programming</article-title>
          .
          <source>RAIRO Recherche Op'erationnelle, 22</source>
          ,
          <year>1988</year>
          . http://citeseerx.ist.psu.edu/viewdoc/download? doi
          <source>=10.1.1.30.9957&amp;rep=rep1&amp;type=pdf.</source>
        </mixed-citation>
      </ref>
      <ref id="ref14">
        <mixed-citation>
          [8]
          <string-name>
            <given-names>Paul</given-names>
            <surname>Feautrier</surname>
          </string-name>
          .
          <article-title>Automatic parallelization in the polytope model</article-title>
          .
          <source>In The Data Parallel Programming Model: Foundations, HPF Realization, and Scienti c Applications</source>
          , pages
          <volume>79</volume>
          {
          <fpage>103</fpage>
          , London, UK, UK,
          <year>1996</year>
          . Springer-Verlag. http://dl. acm.org/citation.cfm?id=
          <volume>647429</volume>
          .
          <fpage>723579</fpage>
          .
        </mixed-citation>
      </ref>
      <ref id="ref15">
        <mixed-citation>
          [9]
          <string-name>
            <given-names>M. J.</given-names>
            <surname>Fischer</surname>
          </string-name>
          and
          <string-name>
            <given-names>M. O.</given-names>
            <surname>Rabin</surname>
          </string-name>
          .
          <article-title>Super-exponential complexity of presburger arithmetic</article-title>
          .
          <source>Technical report</source>
          , Cambridge, MA, USA,
          <year>1974</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref16">
        <mixed-citation>
          [10]
          <string-name>
            <surname>Branko</surname>
            <given-names>Grunbaum. Convex</given-names>
          </string-name>
          <string-name>
            <surname>Polytops</surname>
          </string-name>
          . Springer, New York, NY, USA,
          <year>2003</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref17">
        <mixed-citation>
          [11]
          <string-name>
            <surname>Rui-Juan</surname>
            <given-names>Jing</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Chun-Ming Yuan</surname>
          </string-name>
          , and
          <string-name>
            <surname>Xiao-Shan Gao</surname>
          </string-name>
          .
          <article-title>A polynomial-time algorithm to compute generalized hermite normal form of matrices over Z[x]</article-title>
          .
          <source>CoRR, abs/1601.01067</source>
          ,
          <year>2016</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref18">
        <mixed-citation>
          [12]
          <string-name>
            <given-names>CN</given-names>
            <surname>Jones</surname>
          </string-name>
          , EC Kerrigan, and JM Maciejowski.
          <article-title>On polyhedral projection and parametric programming</article-title>
          .
          <source>Journal of Optimization Theory and Applications</source>
          ,
          <volume>138</volume>
          (
          <issue>2</issue>
          ):
          <volume>207</volume>
          {
          <fpage>220</fpage>
          ,
          <year>2008</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref19">
        <mixed-citation>
          [13]
          <string-name>
            <given-names>Ravindran</given-names>
            <surname>Kannan</surname>
          </string-name>
          and
          <string-name>
            <given-names>Achim</given-names>
            <surname>Bachem</surname>
          </string-name>
          .
          <article-title>Polynomial algorithms for computing the smith and hermite normal forms of an integer matrix</article-title>
          .
          <source>siam Journal on Computing</source>
          ,
          <volume>8</volume>
          (
          <issue>4</issue>
          ):
          <volume>499</volume>
          {
          <fpage>507</fpage>
          ,
          <year>1979</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref20">
        <mixed-citation>
          [14]
          <string-name>
            <given-names>N.</given-names>
            <surname>Karmarkar</surname>
          </string-name>
          .
          <article-title>A new polynomial-time algorithm for linear programming</article-title>
          .
          <source>In Proceedings of the sixteenth annual ACM symposium on Theory of computing, STOC '84</source>
          , pages
          <fpage>302</fpage>
          {
          <fpage>311</fpage>
          , New York, NY, USA,
          <year>1984</year>
          . ACM.
        </mixed-citation>
      </ref>
      <ref id="ref21">
        <mixed-citation>
          [15]
          <string-name>
            <given-names>Leonid</given-names>
            <surname>Khachiyan</surname>
          </string-name>
          .
          <article-title>Fourier-motzkin elimination method</article-title>
          .
          <source>In Christodoulos A. Floudas</source>
          and Panos M. Pardalos, editors,
          <source>Encyclopedia of Optimization, Second Edition</source>
          , pages
          <volume>1074</volume>
          {
          <fpage>1077</fpage>
          . Springer,
          <year>2009</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref22">
        <mixed-citation>
          [16]
          <string-name>
            <given-names>Matthias</given-names>
            <surname>Ko</surname>
          </string-name>
          <article-title>ppe and Sven Verdoolaege</article-title>
          .
          <article-title>Computing parametric rational generating functions with a primal barvinok algorithm</article-title>
          .
          <source>Electr. J. Comb.</source>
          ,
          <volume>15</volume>
          (
          <issue>1</issue>
          ),
          <year>2008</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref23">
        <mixed-citation>
          [17]
          <string-name>
            <given-names>William</given-names>
            <surname>Pugh</surname>
          </string-name>
          .
          <article-title>The omega test: a fast and practical integer programming algorithm for dependence analysis</article-title>
          . In Joanne L. Martin, editor,
          <source>Proceedings Supercomputing '91</source>
          ,
          <string-name>
            <surname>Albuquerque</surname>
            ,
            <given-names>NM</given-names>
          </string-name>
          , USA, November
          <volume>18</volume>
          -
          <issue>22</issue>
          ,
          <year>1991</year>
          , pages
          <fpage>4</fpage>
          <lpage>{</lpage>
          13. ACM,
          <year>1991</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref24">
        <mixed-citation>
          [18]
          <string-name>
            <given-names>William</given-names>
            <surname>Pugh</surname>
          </string-name>
          .
          <article-title>Counting solutions to presburger formulas: How and why</article-title>
          . In Vivek Sarkar, Barbara G. Ryder, and Mary Lou So a, editors,
          <source>Proceedings of the ACM SIGPLAN'94 Conference on Programming Language Design and Implementation</source>
          (PLDI), Orlando, Florida, USA, June 20-24,
          <year>1994</year>
          , pages
          <fpage>121</fpage>
          {
          <fpage>134</fpage>
          . ACM,
          <year>1994</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref25">
        <mixed-citation>
          [19]
          <string-name>
            <given-names>Alexander</given-names>
            <surname>Schrijver</surname>
          </string-name>
          .
          <article-title>Theory of linear and integer programming</article-title>
          . John Wiley &amp; Sons, Inc., New York, NY, USA,
          <year>1986</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref26">
        <mixed-citation>
          [20]
          <string-name>
            <given-names>David</given-names>
            <surname>Wonnacott</surname>
          </string-name>
          .
          <article-title>Omega test</article-title>
          .
          <source>In Encyclopedia of Parallel Computing</source>
          , pages
          <volume>1355</volume>
          {
          <fpage>1365</fpage>
          .
          <year>2011</year>
          .
        </mixed-citation>
      </ref>
    </ref-list>
  </back>
</article>