1. Introduction
Finite partial orders or posets have numerous applications, including scheduling [1-8], molecular evolution [9-12], data mining [13-17], graph theory [18-23], and algebra [24-27]. Many applications implicitly or explicitly involve linear extensions of posets. For example, the solution of many scheduling problems requires a linearization of the jobs being scheduled consistent with some precedence constraints given by a poset. As the number of linear extensions of a poset may be exponential in the number of elements of the base set, many computational problems related to linear extensions are not solvable in polynomial time. Ruskey [28], West [29], Pruesse and Ruskey [30], Canfield and Williamson [31], Korsh and LaFollette [32], and Ono and Nakano [33] provide algorithms to generate all of the linear extensions of a finite poset. As the size of a solution may be exponentially large, these algorithms emphasize the ability to generate each successive linear extension in polynomial time, at least on average. Sampling the linear extensions of a poset is easier. Bubley and Dyer [34] use a rapidly mixing Markov chain to generate a random linear extension of a finite poset, sampled almost uniformly.
Problems in mining order information from databases of sequences (see, e.g., [16,17,35,36]) have an inverted character from that of many computational problems involving posets. Here, a problem instance is a set of linear orders of items from some universal set, while a solution is one or more posets that well explain, through their linear extensions, a significant number of the linear orders. An example from computational neuroscience [37] might go as follows. Each item is the firing of a neuron, while each linear order is a sequence of neuronal firings, ordered in time from an experiment. The solution is a neural circuit that explains a set of such linear orders. These novel problems are ripe for mathematical formalization and study. In this paper, we define and study one such problem. A problem instance is a set of permutations of a base set, and a solution covers the instance with linear extensions (Section 2). We prove that the Poset Cover problem (a decision problem) is NP-complete in Section 3. In Section 4, we explore how cover relations relate to poset covers. Finally, we develop a polynomial-time algorithm to find a partial cover in Section 5.
2. Preliminaries
In this section, we establish terminology and notation and prove some basic results.
A partial order or poset 
is an irreflexive, antisymmetric, and transitive binary relation 
defined on a finite set 
of cardinality
. We write 
as the ordered pair
. Equivalently, poset 
is a transitive directed acyclic graph (DAG), namely,
. If G is a DAG, then its transitive closure is a poset by this equivalence. The rank function 
is given by
. The empty poset is
.
Let 
be distinct. Then 
and 
are comparable in
, written
, if 
or
, while x and 
are incomparable, written
, otherwise. Moreover, x is covered by y or y covers x, written
, if 
and there is no 
such that
. In this case, the ordered pair 
is a cover relation for
. It is well-known that a (finite) poset is uniquely determined by its set of cover relations (see [38]).
If 
and 
are posets on the same set
, then 
is an extension of
, written
, if, for all 
implies
. The relation 
on posets of 
is reflexive, antisymmetric, and transitive.
A linear order 
on X is a poset L such that, for
, either 
or 
holds. If 
is a linear order, then the rank function 
is a bijection. Setting
, 
can be written as the sequence
, which is a permutation of
. Also, we write 
for the element of rank 
in
. A linear extension 
of a poset 
is a linear order such that
. The set of all linear extensions of 
is
. Note that 
is the set of all linear orders on
. Brightwell and Winkler [39] prove that the problem of determining 
for a poset 
is #P-complete.
Let 
be a set of 
posets on
. This set covers the set of linear orders
A poset 
is maximal in 
if 
and there is no poset 
of 
such that
, and
. Let 
be a set of posets on
, and let 
be a set of linear orders on
. 
blankets 
if
Lemma 1 Let 
be the set of linear orders that is covered by a set 
of posets of cardinality
. Then, there exists a cover 
of cardinality 
that also covers 
such that every poset in 
is maximal in
.
Proof. We construct 
by examining each poset in
. Let
. If 
is maximal in
, then add 
to
. Otherwise, let 
be a poset of minimum cardinality (as a set of ordered pairs) such that 
and
. Since 
is not maximal,
. Moreover, any poset 
contained in 
of smaller cardinality will have
. Add 
to
.
The constructed 
has cardinality
. Moreover, 
also covers 
and every poset in 
is maximal in
. The lemma follows.
In this paper, we are interested in reversing the cover relationship by addressing the problem of finding a minimum set of posets that covers a given set of linear orders. As a decision problem, this is Poset Cover INSTANCE: A base set 
of cardinality
; a nonempty set 
of linear orders over
; and an integer
.
QUESTION: Is there a set 
of posets on 
of cardinality 
that covers
?
This problem is shown to be NP-complete in Section 3.
Let 
be a linear order on
. For each 
satisfying
, the i-swap of 
is the linear order
.
Let
. Evidently, 
, so the
-swap relation is symmetric, written
. For pairs 
that are 
-swaps of each other, for some
, we define the function
. Note that the set differences of 
and
, namely
and
, each consist of a single ordered pair. In this case, the swap pair for 
and 
is the unordered pair
; otherwise,
. Two linear orders 
and 
differ by a swap, written
, if
, for some
. Since 
if and only if
, the
relation is also symmetric. If
, 
and
, then we write 
to mean that 
for some
, where the elements swapped are 
and
.
Let 
be a set of linear orders on
. The swap graph of 
is the undirected graph
. An edge 
of
is labeled
. Let 
be a poset on
, and let
. Then, 
is a partial cover of 
including 
if 
and
. The swap graph is the same as the adjacent transposition graph of Pruesse and Ruskey [30]. The swap graph of 
is bipartite, since every edge connects an even permutation to an odd permutation. Moreover, the swap graph 
of the linear extensions of a single poset is connected (see [30]).
Let 
be the set of all posets on
. Let 
be a set of ordered pairs. The up-set of 
is
is empty if and only if the directed graph 
contains cycles. Let
be a set of unordered pairs. The down-set of 
is
, and we always have the empty poset
.
If
, then define the minimal element in 
to be
The following properties of 
follow directly from the definitions.
Lemma 2 
and
.
We have the following properties of up-sets and downsets.
Lemma 3 Let
. If
, then
. Let
. If
, then
.
Proof. Suppose that
. By the definition of upsets,
Now, suppose that
. Then,
by the definition of down-sets.
3. NP-Completeness of Poset Cover
In this section, we show that PosetCover is NP-complete, in the process using the following known NP-complete decision problem [40].
Cubic Vertex Cover INSTANCE: A nonempty undirected graph 
that is cubic, that is, in which every vertex has degree 3; and an integer
.
QUESTION: Is there a subset 
of cardinality 
such that every edge in 
is incident on at least one vertex in
?
Theorem 4 Poset Cover is NP-complete.
Proof. We show that Poset Cover is in NP and that Cubic Vertex Cover reduces to Poset Cover in polynomial time.
We first show that Poset Cover is in NP. Let
, 
, and 
constitute an instance of Poset Cover, and let 
be a set of posets on
. First, it is easy to check whether 
in time polynomial in 
and
; if
, then return No. Second, if the cardinality check succeeds, check whether 
covers 
as follows. For each poset 
in turn, use the Korsh and LaFollette [32] algorithm to generate all the linear extensions of
, one at a time, in constant time per linear extension. As each linear extension 
is generated, check whether
. If not, then return No. If so, then mark that element of 
Covered. Note that the number of linear orders generated by a run of the Korsh and LaFollette algorithm before completion or returning No is at most
. Hence, the worst-case time for one run of the algorithm, including the checking, is
. Once all the posets and their linear extensions are processed, check whether every element of 
is marked Covered. If so, then return Yes; otherwise, return No. We find that the worstcase time to check whether 
covers 
is 
, since
. This is polynomial in the size of the original instance. We conclude that Poset Cover is in NP.
Now, let 
and 
constitute an instance of Cubic Vertex Cover . Without loss of generality, assume that 
and that
. Let 
, and let 
be an arbitrary labeling of the 
edges of
. As a running example of our reduction, we provide the cubic graph in Figure 1, with 
vertices and 
edges. To complete the instance of Cubic Vertex Cover , set
.
Let
, and let 
be a base set of 
elements. Let
, the base order, be the linear order on 
specified by
We view the elements of 
as consisting of 
adjacent, non-overlapping pairs. Specifically, the pairs are 
and
, where
. All elements of 
are obtained by a small set of swaps of such pairs, applied to
.
Figure 1. A cubic graph as part of an instance of cubic vertex cover.
The first s pairs correspond to the s edges in a natural way. In particular, edge 
is associated with the edge order
. Continuing the example, we set
,
and, for example,
For each vertex
, there are three edges incident on
; let the indices of those edges be
, and
. For each pair 
and 
of these edges, we define the pair edge order to be
For the running example, there are 18 pair edge orders. For each triple
, and
, we define the triple edge order to be
For the running example, there are 6 triple edge orders.
The primary orders are the base, edge, pair edge, and triple edge orders. For primary pair edge order
, there is a corresponding secondary pair edge order obtained by swapping 
and
, which is
For primary triple edge order
, there is a corresponding secondary triple edge order obtained by swapping 
and
, which is
For the running example, there are 18 secondary pair edge orders and 6 secondary triple edge orders.
Collect the various orders into five sets, as follows:
We can now complete our instance of Poset Cover by setting
and setting the integer parameter
. Note that
. For the running example, 
and
.
It remains to show that an instance of Cubic Vertex Cover is a Yes instance if and only if the corresponding instance of Poset Cover is a Yes instance.
Fix an instance 
and 
of Cubic Vertex Cover . Let
, and 
constitute the corresponding instance of Poset Cover, as constructed above. By Lemma 1, we may assume that every element of a cover 
of 
is maximal in
. Since the elements of 
must be blanketed by any cover, we may assume that the set
is a subset of
. Similarly, since the elements of 
must be blanketed by any cover, we may assume that the set
is a subset of
. Note that 
and that 
blankets
.
First, assume that 
is a vertex cover of 
of cardinality at most
. Define
Note that 
and that, by previous observations, it suffices to demonstrate that 
blankets 
and
. Since 
is nonempty, 
, and
. Therefore, 
is blanketed by each of the posets 
in 
corresponding to a vertex
. For an edge
, there is a 
incident on
. Then, 
is blanketed by the poset
in
, and hence every linear order in 
is blanketed by
. We conclude that 
covers
, as desired.
Now, assume that 
is a cover of 
of cardinality at most
. By previous observations, we must have
, for some set 
of cardinality at most
. Since 
covers
, 
must blanket 
and
. Let 
be any edge of
, incident on vertices 
and
. Without loss of generality, we may assume that
. There are two maximal posets that blanket 
and
. One of these posets must be in
.
Moreover, we may assume that 
contains only orders of this form, since each such order blankets
, and the only other orders for 
to blanket are the
’s. Define
Because 
blankets all of the
’s, we conclude that 
is a vertex cover of G of cardinality 
, as desired.
The theorem follows.
4. Cover Relations
In this section, we examine properties of cover relations in linear orders and their consequences for poset covers.
Let 
be a poset, thought of as a transitive DAG. Then, a topological sort of 
yields an order 
on 
such that 
implies
. Assume that 
is not a linear order. Then there exist 
such that
. There exists at least one topological sort of 
in which 
appears to the left of
, and there exists at least one topological sort of 
in which 
appears to the left of
. (This follows from alternate choices available to the depth-first search used to construct a topological sort. See [41].) Select a topological sort that makes 
and
, where
. In that case, we obtain a proper extension 
of 
in which 
by adding 
to the DAG and taking the transitive closure. Moreover, we have
, since the existence of 
such that 
contradicts
. We have just demonstrated the following.
Lemma 5 Let 
be a poset, and let 
satisfy
. Let
Then 
is a poset, 
, and
.
Theorem 6 Let 
be a poset that is not a linear order, and let 
satisfy
. Then there exists a proper extension 
of 
such that
.
Proof. First, suppose that there exists a 
that is incomparable to
. By Lemma 5, there exists a poset 
such that 
and
. Moreover, 
, so, by the definition of
.
Second, the case of there being a 
that is incomparable to 
is handled analogously.
Finally, we have the case that no element is incomparable either to 
or to
. Let 
be such that 
and
. (Such a pair 
must exist, since 
is not a linear order.) If either 
and 
or 
and
, then adding 
to the DAG for 
and taking the transitive closure gives us the desired poset. The case 
and 
(or vice versa) is impossible, since 
and
. There are no other cases, since
.
The theorem follows.
Theorem 7 Let 
be a poset, and let 
satisfy
. Then there exists a linear order 
such that 
and
. Moreover, for every linear extension 
of 
in which
, there exists a unique linear extension
of 
such that 
and
.
Proof. By Lemma 5, there exists a poset 
such that 
and
. By applying Theorem 6 iteratively to
, we ultimately obtain a linear order 
that is an extension of 
(and hence of
) such that
.
Now, let 
be a linear extension of 
in which
. Let
; then
. Let
. Let
. Then 
is a poset on 
such that 
and such that 
and 
are incomparable in
. Moreover, 
, so 
is a linear extension of 
in which
.
The theorem follows.
Theorem 8 Let 
be a set of linear orders on
. Let 
be an element of
. Let 
satisfy
. Let 
be a partial cover of 
including
. If
, then 
and 
are comparable in 
and
.
Proof. Suppose that
. First assume that 
and 
are comparable in
. Then it must be true that
, since 
covers 
in
. For the same reason, there is no 
such that
. Hence,
.
It remains to show that 
and 
are comparable in
. To obtain a contradiction, assume that 
and 
are incomparable in
. By Theorem 7, there exists a unique linear extension 
of 
such that 
and
. Necessarily,
. Since 
but
, we have a contradiction to the fact that 
is a partial cover of 
including
. The contradiction establishes that 
and 
are comparable in
. The theorem follows.
We next characterize a set 
of linear orders that is covered by a single poset. The ordered pair 
is a cover relation for 
if there exists an 
and an 
such that
, 
, and
. If 
is a cover relation for
, then any poset P that partially covers 
including 
must satisfy
. An 
cover sequence of length 
for 
is a sequence 
such that 
is a cover relation for
, for
. If there is an 
cover sequence for
, then any poset 
that covers 
must satisfy
.
Theorem 9 A set 
of linear orders is the set of linear extensions of a single poset if and only if, for every 
for which
, exactly one of the following holds: 1) 
for some
; 2) there is an 
cover sequence for
; or 3) there is a 
cover sequence for
.
Proof. For one direction, assume that there exists a poset 
such that 
is the set of linear extensions of
. Let 
satisfy
.
First, suppose
. By Theorem 7, there exists a linear extension 
of 
for which 
and another linear extension 
of 
for which 
and
. Then, 1) holds. Neither 2) nor 3) holds, since those imply that 
and 
are comparable in
.
Now suppose that
. (The case 
is symmetric). Then 1) does not hold, since that implies that
. Also 3) does not hold, since that implies that
. To demonstrate 2), it remains to construct an 
cover sequence for
. The first case is
. Then, by repeated application of Theorem 6, there exists a linear extension 
of 
such that
. Let
. Then,
. Hence, 
is an 
cover sequence for
. More generally, we can write 
for some 
such that 
for
. Then 
is also an 
cover sequence for
.
For the other direction, assume that, for every 
for which
, exactly one of 1), 2), or 3) holds. Take 
to be the poset generated by all the ordered pairs 
such that 
is a cover sequence for
. We need to show that 
equals the set of linear extensions of
. There are two cases to consider for each linear order
. Let
.
Case 1.
. To obtain a contradiction, assume that 
is not a linear extension of
. Then there exist 
and 
such that
. Let 
satisfy
. Then, 
is an 
cover sequence for 
and hence 2) holds for 
and
, but not 1) or 3). Let
. Since 1) does not hold, we have
. But then 
is a cover sequence for
, a contradiction to the fact that 3) does not hold. In this case, we conclude that 
is a linear extension of
.
Case 2.
. Without loss of generality, we may assume that there exist 
and 
such that 
and 
. Since
, we have that 
is a cover sequence for
. Hence, 
and 
cannot be a linear extension of
.
We conclude that 
is precisely the set of linear extensions of
.
The theorem follows.
5. A Partial Cover Algorithm
In this section, we present an algorithm for finding a poset that is a partial cover with a maximal set of linear extensions.
5.1. Some Intuition
Intuition for designing an algorithm to find a partial poset cover for a set 
of linear orders is developed first. It suffices to take a single 
and identify a single poset 
that is a partial cover of 
including
. Observe that 
is such a poset but is not satisfactory if we can construct a poset 
that covers more of
. We use the swap graph 
to direct construction of a more satisfactory
.
During the process of constructing
, we maintain a specification for a set of posets, each of which covers a constructed set
. We also maintain a set 
consisting of linear orders, including
, that have already been chosen to be covered by the final constructed poset. This specification consists of two kinds of information: some 
relations and some 
relations. These relations must be consistent, that is, there must be at least one poset that satisfies them all. A bit more formally, the 
relations can be specified by a set 
of ordered pairs, while the 
relations can be specified by a set 
of unordered pairs. The specified set of posets is then
.
will be maintained to satisfy the following property. Let 
be arbitrary, and let 
be any cover relation of
. Let
. If
, then we require that
. The rational for this requirement is that every poset 
that covers 
and does not cover 
satisfies the relation
. As a side effect, every 
for which 
can be eliminated from further consideration for inclusion in
.
will be maintained to satisfy the following property. Again, let 
be arbitrary, and let 
be any cover relation of
. Let
. If
, then we require that
. The rational for this requirement is that every poset 
that covers both 
and 
satisfies the relation
. As a side effect, every 
for which the 
adjacency is not in 
can be eliminated from further consideration for inclusion in
.
We will need these definitions. Let 
be distinct, and let 
be a linear order. The 
-interchange of L is the linear order that is the same as 
except a and b have been exchanged. Let 
be a sequence of linear orders such that
, for
, so that the sequence is a path 
in
. Let 
be a subset of
. 
is 
-labeled if, for
. A path
in 
is the 
-mirror path of 
if, for
, 
is the 
-interchange of
.
5.2. The Algorithm
Figure 2 contains pseudocode for the algorithm PartialCover
. It works by adding linear orders from 
to 
one at a time, while maintaining the required properties for A and B. The subroutine Trim in Figure 3 is used to ensure that the required property for 
is maintained. The addition of a linear order to 
(Step 9) can add at most one new unordered pair to B (Step 10).
We illustrate the algorithm with the example having
and
. Figure 4 contains the swap graph.
The call to Trim in Step 5 finds that 
is not in
, so any linear orders in 
for which 4 is less than 3 should be deleted. In this case, there is no such linear order in
. After Step 6, 
and
.
The first time that Step 8 is executed in Partial-Cover, 
and
. (There are three choices for
. This is just one of them.) Then
(Step 9) and 
(Step 10). The call to Trim in Step 11 finds that 
is not in
. The resulting cover relation 
is not new, so 
remains
. The while loop from Steps 13 to 21 has only the swap pair 
to work with. Linear order 32154 is missing its 
swap partner, 31254. Hence, 32154 is deleted from
, which is now
The second time that Step 8 is executed, 
and L2 = 23145. Then 
(Step 9) and 
(Step 10). The call to Trim in Step 11 finds that 23415 is not in
. The resulting cover relation 
is new, so A is extended to 
. None of the linear orders in 
has 4 less than 1, so the call to Trim does not change
. The while loop from Steps 13 to 21 now has the swap pair 
to work with. Linear order 
is missing its 
swap partner,
. Hence, 
is deleted from
, which is now
The third time that Step 8 is executed, 
and
. Then
(Step 9) and
(Step 10). The call to Trim in Step 11 finds that 
is not in
. The resulting cover relation 
is new, so 
is extended to
. None of the linear orders in 
has 5 less than 3, so the call to Trim does not change
. The while loop from Steps 13 to 21 now has the swap pair 
to work with. Linear orders 32145, 31245, and 13245 are missing their 
swap part-
ners. Hence, they are deleted from
, which is now
The fourth time that Step 8 is executed, 
and
. Then
(Step 9) and
(Step 10). The call to Trim in Step 11 finds that 
and 
are not in
. The resulting cover relations are 
and
, so 
is extended to
. None of the linear orders in 
has 3 less than 2, so the call to Trim does not change
. The while loop from Steps 13 to 21 has no new swap pairs to work with. Hence, there are no further linear orders to delete from
, which remains
The fifth and last time that Step 8 is executed, 
and
. Then
(Step 9) and
(Step 10). The call to Trim in Step 11 finds that 
and 
are not in
. The resulting cover relations are
, which is not new, and
, which is new, so 
is extended to
. None of the linear orders in 
has 3 less than 2 or 5 less than 1, so the call to Trim does not change
. The while loop from Steps 13 to 21 has no new swap pairs to work with. Hence, there are no further linear orders to delete from
, which remains
At this point,
.
The resulting poset 
has the cover relations in
, namely, 
, and
. The set of linear extensions of 
is exactly the final value of
, namely, 
.
5.3. Proof of Correctness
We assume that the following loop invariants hold each time that the test at the top of the while loop body (Step 7) is executed.
1)
.
2) 
is a connected graph, and 
is a connected graph.
3) The directed graph 
contains no cycles.
4) Every element of 
is a linear extension of
, that is,
.
5) The set 
equals the set of ordered pairs
for which there exists 
such that
.
6) 
and consequently 
.
7) The set 
equals the set of unordered pairs 
such that 
and such that there exist 
satisfying
.
8) Let 
be a 
-labeled path of linear orders such that 
and 
and such that 
is a shortest 
-labeled path from 
to
. Let 
be the 
-mirror path for
. Then, all of the 
's are in
, and either all of the
’s are in 
or none of them are.
Together, these invariants suffice to demonstrate the correctness of Partial-Cover, culminating in Theorem 11.
Every execution of subroutine Trim enforces Invariant 5.
Invariant 2 is guaranteed by Steps 6 and 22 and by the way that linear orders are selected for addition to 
(Step 8).
Invariants 1 and 2 guarantee that, whenever Step 8 is reached, there is a suitable 
pair to select.
The fact that 
is guaranteed through the initialization in Step 3 and the fact that any change to 
always selects a subset of
.
Initialization. After initialization (Steps 2 through 6), all invariants are true for the first execution of Step 7, for the following reasons. We have 
and
. The execution of Trim (Step 5) ensures that Invariants 4 and 5 hold, while maintaining 
(Invariant 1). Step 6 guarantees Invariant 2. Invariant 3 holds because the only order relations in 
are cover relations in
. The fact that 
makes Invariants 6, 7, and 8 true vacuously.
Execution of the loop body. The fact that 
requires that the algorithm never deletes an element of 
from 
in Step 19 or in Trim. That fact also implies
, since 
is initially put in 
(Step 2) and could only be deleted in Step 19 or in Trim.
The algorithm never deletes an element of 
from 
in Trim. To obtain a contradiction, assume that 
is deleted in Step 12 of Trim and that it is the first element of 
deleted. The deletion of 
is caused by a sequence 
such that
, for
, and
. For each 
satisfying
, there exists an 
such that
, and
. There is a path in 
from 
to 
that does not contain an edge with swap pair
, since 
contradicts
. Consequently, 
and 
are in the same order in 
and in
, which implies that
. Taken together, these relations imply that
, a contradiction to
. We conclude that 
is, in fact, not deleted in Trim.
The algorithm never deletes an element of 
from 
in Step 19. The deletion of an element 
depends on the swap pairs in
. More particularly, such a deletion would require a 
-labeled path in 
labeled from 
from 
to some 
that has a swap pair from 
that goes to a linear order outside
. This cannot happen because of Invariant 8. We conclude that 
is, in fact, not deleted in Step 19.
Invariant 3 is maintained because the existence of a cycle in A implies that A and B are inconsistent.
Invariants 4 and 5 are maintained by Trim.
The consistency of A and B (Invariant 6) is maintained by Trim and the loop at Steps 15 through 21.
Invariant 7 is maintained by the way that elements are added to B (Step 10).
It remains to show that Invariant 8 holds; this is demonstrated in the following lemma.
Lemma 10 Each time that Step 8 is about to be executed, Invariant 8 holds.
Proof. Let 
be a 
-labeled path of linear orders such that
, 
, and 
and such that 
is a shortest 
-labeled path from 
to
. Let 
be the 
-mirror path for
.
To obtain a contradiction, assume that there is some 
that is not in
. Let 
be the first such. Then
, so
. Let
. Since
, 
cannot be in
, since it would have been deleted in a previous iteration due to the swap pair 
being in
. This is a contradiction. We conclude that all of the
’s are in
.
We next show that 
is not just a shortest 
- labeled path but is also a shortest path in
. Let
. For any path from 
to 
in
, every 
must be the swap pair for some edge in the path. Consequently,
. Moreover, there is a path in 
that uses swap pairs only from 
and each only once, so the length of every shortest path from 
to 
is
. (Think about the swaps done by bubble sort; these give one such shortest path.) Since 
is a shortest 
- labeled path from 
to
, it must be a 
-labeled path having
. Note that, therefore, no swap pair occurs more than once in
.
We next show that 
is a 
-labeled path. Since 
contains no swap pair more than once and since 
and
, if there is a swap pair 
labeling an edge of
, we must also have the swap pair 
labeling another edge of
, and vice versa. More succinctly, 
if and only if
. Let
, for some 
satisfying
. If
, then
. If
, then
, which is in 
by the argument above. Similarly, if
, then
, which is in 
by the argument above. We conclude that 
is a 
-labeled path and hence a 
-labeled path.
Finally, we show that either all of the
’s are in 
or none of them are. To obtain a contradiction, suppose that 
and that
, for some 
satisfying
. (The case 
and 
will yield a contradiction by an analogous argument.) But, in this case, 
would have been deleted from 
in an earlier iteration, a contradiction. From this contradiction, we conclude that either all of the
’s are in 
or none of them are.
Hence, Invariant 8 holds.
The correctness and time complexity of the algorithm are now in view.
Theorem 11 Algorithm Partial-Cover
returns a set 
such that 
is a partial cover of 
including
. The algorithm has time complexity
.
Proof. The correctness of the algorithm follows from the prior discussion of the loop invariants.
For the time complexity, we first note that
and
.
We examine the subroutine Trim. Trim is executed once in Step 5; once for each addition to 
(Step 11; 
times in total); and once for each deletion in Step 19 (Step 20; 
times in total). Hence, Trim is executed 
times. The loop in Steps 5 through 9 requires 
time for one execution. The time complexity to test coverage in Step 11 requires 
time. Hence, the loop in Steps 10 through 13 requires 
time for one execution. The while loop is executed 
times, since each additional iteration of the loop because 
requires the reduction of the cardinality of 
by at least one. We conclude that the total time spent in trim is
.
It is easy to check that the complexity bound for all calls to Trim dominates the time complexity of the algorithm. Hence, the time complexity of Partial-Cover is
, as required.