I have 4 possible properties of a kind of mathematical object, and I want to prove their implications. I've proved $P_1 \rightarrow P_2$, $P_2 \rightarrow P_3$, and thus also $P_1 \rightarrow P_3$.

Now, I think no other implications are possible between them, and in fact can disprove all other implications. What is the least number of implications I need to disprove to disprove all of them?

Is there a general algorithm for such question? Given a directed graph of implications between properties, and asking how many implications must be disproved in order to show that no other arrows exist in the graph? Well, yes, if the algorithm simply checks all possibilities exhaustively. But is there a more efficient one?

In response to bof, Here I only ask about disproving the arrows of the form $P_n \rightarrow P_m$, not of the more general form $P_n \wedge P_m \rightarrow P_k$, though that could make a nice extension to the problem.

After some looking, I think a formal way to state the question is: given a directed graph $G$ with vertices $V$, denote its transitive closure to be $G_t$. Find a minimal (smallest in number) set of "forbidden" directed edges, such that $G_t$ is the unique transitive directed graph with vertices $V$, that contains $G$, and does not contain any of the forbidden directed edges.

  • $\begingroup$ Nice problem, are you the author? $\endgroup$ – dtldarek Feb 14 '17 at 8:25
  • $\begingroup$ @dtldarek The question came to me when I was actually trying to do exactly what I said in the problem: I have 4 properties of functions, and wanted to completely prove/disprove their implication relations. $\endgroup$ – MaudPieTheRocktorate Feb 14 '17 at 13:47

We may assume that equivalent statements have been identified, so that the relation of implication is antisymmetric as well as being reflexive and transitive, i.e., it's a partial order. Thus the problem may be stated as follows:

Let $V$ be a finite set partially ordered by a relation $R.$ What is the smallest set $D\subseteq(V\times V)\setminus R$ such that every transitive relation $T\subseteq V\times V,$ which contains $R$ and is disjoint from $D,$ is equal to $R?$

Clearly, any such set $D$ must contain any pair $(a,b)\in(V\times V)\setminus R$ such that $R\cup\{(a,b)\}$ is a transitive relation; otherwise $T=R\cup\{(a,b)\}$ would be a transitive relation containing $R$ and disjoint from $D$ and unequal to $R.$ Let $D_0$ be the set of all such pairs:

$$D_0=\{(a,b)\in(V\times V)\setminus R:R\cup\{(a,b)\}\text{ is transitive}\}.$$

I claim that $D_0$ is the desired set. Let $T\subseteq V\times V$ be a transitive relation such that $R\subseteq T$ and $T\cap D_0=\emptyset;$ I have to show that $T=R.$ Assume for a contradiction that $T\setminus R\ne\emptyset.$ Choose a minimal (with respect to the partial order $R$) element $a\in V$ such that $(a,y)\in T\setminus R$ for some $y,$ and then choose a maximul element $b\in V$ such that $(a,b)\in T\setminus R.$ It is easy to see that $R\cup\{(a,b)\}$ is transitive, whence $(a,b)\in D_0,$ contradiction our assumption that $T\cap D_0=\emptyset.$

In other words, writing $x\le y$ for $(x,y)\in R,$ we can describe $D_0$ as the set of ordered pairs $(a,b)\in(V\times V)$ satisfying the conditions:

$$a\not\le b$$ $$\forall x\in V\ (x\lt a\implies x\le b);$$ $$\forall x\in V\ (b\lt x\implies a\le x.$$

For $a\in V$ let $F(a)$ be the set of all maximal elements of $\{x:x\lt a\},$ and let $G(a)$ be the set of all minimal elements of $\{x:b\lt x\}.$ If we wish to compute $D_0,$ we might start by computing the sets $F(a)$ and $G(a)$ for each $a\in V;$ then, for each ordered pair $a\not\le b,$ we just have to check the inequalities $x\le b$ for $x\in F(a),$ and $a\le x$ for $x\in G(b).$

Example. If $V=\{v_0,v_1,v_2,v_3\}$ and $R=\{(v_0,v_0),(v_0,v_1),(v_1,v_1),(v_2,v_2),(v_2,v_3),(v_3,v_3)\},$ then $D_0=\{(v_0,v_3),(v_1,v_0),(v_2,v_1),(v_3,v_2)\}.$

  • $\begingroup$ $D_0=\{(v_0,v_3),(v_1,v_0),(v_2,v_1),(v_3,v_2)\}.$ $\endgroup$ – bof Feb 17 '17 at 23:25
  • $\begingroup$ Thanks. Now I see how it works. $\endgroup$ – Fabio Somenzi Feb 18 '17 at 0:10
  • $\begingroup$ Good answer. I think this allows for an algorithm in polynomial time... Can it be done in quadratic time? $\endgroup$ – MaudPieTheRocktorate Feb 18 '17 at 10:40

Let $X$ be the set of our mathematical objects. To show that $P_4$ is not implied by all of them, we would like to find an example $x$ such that $\alpha(x) \land \neg P_4(x)$ where $\alpha$ is $P_1, P_2, P_3$. However, due to the implications you have proved, it's enough to show $x$ such that $P_1(x) \land \neg P_4(x)$, that is $P_1 \not\to P_4$.

Yet, this is not all, to show that $P_4$ is independent we also need to find $x$ such that $P_4(x) \land \neg \alpha(x)$. Observe that you also have proved $\neg P_3(x) \to \neg P_2(x)$ and $\neg P_2(x) \to \neg P_1(x)$ for all $x \in X$, so it's enough to find $x$ with $P_4(x) \land \neg P_3(x)$, i.e. $P_4 \not\to P_3$.

That might seem like all, but it's not. We are forgetting $P_2 \not\to P_1$ and $P_3 \not\to P_2$ and $P_3 \not\to P_1$. For these we need an $x$ such that $P_2(x) \land \neg P_1(x)$ and some different $x$ such that $P_3(x) \land \neg P_2(x)$.

As for whether such an algorithm exists, definitely yes: for all subsets of possible implications you can check if that subset is enough to prove status of every implication. Nevertheless, that would be rather slow, so now the question is, can we make it faster? My guess is yes, but currently I have no proof.

I hope this helps $\ddot\smile$

Edit: Thanks to @bof for spoting a flaw in the algorithm I suggested.

Edit 2:

Here is a second attempt at an algorithm. I will start with a change in terminology, so that it is more concrete, and thus perhaps simpler.

Let $V = \{1,2,3,\ldots,n\}$ be the set of vertices and add a directed edge $i \to j$ if $P_i \to P_j$. Furthermore, for each vertex $v \in V$ create sets $A_v = \{i \in V \mid P_i \to P_v\}$, in particular $v \in A_v$. These sets have the property that $$P_i \to P_j \iff A_i \subseteq A_j,$$ that is $$P_i \not\to P_j \iff A_i \not\subseteq A_j \iff \exists v \in V.\ v \in A_i \land v \notin A_j.$$

Moreover, let us say that $A_i$ is a successor of $A_j$ iff $A_j \subsetneq A_i$ and for all $k$ such that $A_j \subseteq A_k \subseteq A_i$ we have $k = j$ or $k = i$ (intuitively, $A_i$ is one step ahead of $A_j$). Similarly, $A_i$ is a predecessor of $A_j$ iff $A_j$ is a successor of $A_i$ (intuitively $A_i$ is one step before $A_j$).

The algorithm:

  1. Let $D$ be the set of all the pairs that were not settled yet, i.e. $$D \gets \{ (i,j) \in V \times V\mid A_i \not\subseteq A_j \land A_j \not\subseteq A_i\}$$
  2. Pick any such pair $$(i,j) \gets \operatorname{any}(D)$$ Observe that $i \in A_i$, but $i \notin A_j$. We will not try to find an alternate pair with similar property.
  3. Let $i'$ be any predecessor of $i$ such that $i' \notin A_j$ or $i$ if no such predecessor exists and assign $i'$ to $i$ \begin{align} &i' \gets \operatorname{any}\{k\in \operatorname{pred}(i) \mid k \notin A_j \}\\ &\mathtt{if}\ i' \neq \bot:\\ &\quad i\gets i' \end{align}
  4. Do similarly with $j$, i.e. find an appropriate successor: \begin{align} &j' \gets \operatorname{any}\{k\in \operatorname{succ}(j) \mid i \notin A_k \}\\ &\mathtt{if}\ j' \neq \bot:\\ &\quad j\gets j' \end{align}
  5. Repeat steps $4$ or $5$ until no further change is possible.
  6. Prove $P_i \not\to P_j$ (i.e., output that pair as one of those that we need to prove).
  7. Remove from $D$ any pair that is implied by $P_i \not\to P_j$.
  8. Repeat from step $2$ until $D$ gets empty.

A few important points:

  • Because the graph is a DAG, steps 3 and 4 cannot repeat infinitely.
  • If $(i,j) \in D$, then after steps $3$ and $4$ the new pair $(i,j)$ is still in $D$.

    • Suppose otherwise and let $(i',j')$ be the new pair. Please remember that $i' \in A_{i'} \subseteq A_i$ and $i' \notin A_{j'} \supseteq A_j$ because that is how that new pair was constructed. If $(i',j')\notin D$, then it had to be removed from $D$ at some point and there had to be a pair $(i'',j'')$ such that $i'' \in A_{i''} \subseteq A_{i'} \subseteq A_i$ and $i'' \notin A_{j''} \supseteq A_{j'} \supseteq A_j$, but that implies $(i,j) \notin D$.
  • Thus, every time we get to step 7 at least one pair gets removed, so the algorithm finishes in finite time.

  • When we finish step $5$, the pair $(i,j)$ has property that no statement $P_{i'} \not\to P_{j'}$ for some other pair $(i',j')$ could imply $P_i \not\to P_j$.
    • Suppose otherwise that there is such a pair $(i', j')$. That means $i' \in A_{i'} \subseteq A_i$ and $i' \notin A_{j'} \supseteq A_j$, but that implies step $5$ could not finish because $(i',j)$ or $(i,j')$ is a valid change.
  • Therefore, every pair that the algorithm outputs has to be proven.
  • As the algorithm finishes only when $D$ is empty, all necessary pairs will get printed.

I hope I didn't miss anything this time.

  • $\begingroup$ @bof I agree, I missed that case (and I shouldn't $\ddot\frown$). Sadly I have not enough time right now to think about it some more. Thank you for your comments! $\endgroup$ – dtldarek Feb 14 '17 at 10:36
  • $\begingroup$ I added a formal statement of the problem, so that it might be easier to explain to mathematicians and computer scientists. $\endgroup$ – MaudPieTheRocktorate Feb 15 '17 at 4:19
  • $\begingroup$ @bof Perhaps this one works ;-) $\endgroup$ – dtldarek Feb 15 '17 at 14:49

Here is the exhaustive algorithm implemented in Mathematica:

exhaustiveAlgorithm[vertices_, inEdges_] := 
 Module[{v = vertices, i = inEdges, g, e},
  g = Graph[v, i];
  e = EdgeList@GraphComplement@TransitiveClosureGraph@g;
     a \[Function] 
      AllTrue[Complement[e, a], 
       l \[Function] 
         EdgeQ[TransitiveClosureGraph@EdgeAdd[g, l], #] &]]]@Subsets@e}


exhaustiveAlgorithm[{P1, P2, P3, P4}, {P1 -> P2, P2 -> P3}]

will return

{{P1 -> P2, P2 -> P3}, {P1 -> P4, P2 -> P1, P3 -> P2, P4 -> P3}}

telling you that you must show

$$P_1 \to P_2, P_2 \to P_3, \lnot(P_1 \to P_4), \lnot(P_2 \to P_1), \lnot(P_3 \to P_2), \lnot(P_4 \to P_3).$$

I know this doesn't answer your question, but I hope it helps. I would have written this as a comment but it did not fit in the character limit.

  • $\begingroup$ It does work but is as inefficient as I feared. I tried the algorithm on a graph with 6 vertices and it used up my computer memory. $\endgroup$ – MaudPieTheRocktorate Feb 15 '17 at 4:44
  • $\begingroup$ @KopaLeo You're right that it's highly inefficient. I don't have time at the moment, but I believe I can optimize this algorithm quite a lot. If it would be helpful, I can return in a few days with a better program that will handle 6 vertices easily. $\endgroup$ – diracdeltafunk Feb 15 '17 at 9:23
  • 1
    $\begingroup$ It's just a puzzle. I don't really need an answer. I do feel it should have some connection with boolean satisfiability problems so maybe somehow there's an efficient algorithm that can be adapted for this. $\endgroup$ – MaudPieTheRocktorate Feb 15 '17 at 14:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.