2
$\begingroup$

In the context of my research, I am having a hard time in solving this problem. It resembles the topological ordering problem, but since that the graph can contain cycles, I cannot apply the existing algorithm.

I have a set of initial nodes. Through an iterative process, I can use a pair of distinct nodes (initial or not) to imply a third node (initial or not). Every node, initial or not, can imply 0 or more nodes.

Suppose I have generated a graph with those rules.

Starting from a non-initial node, I want to enumerate all possible implication chains which start from a subset of initial nodes and reach a target node. Each non-initial node in the chain must be implied by exactly one pair of nodes. Each initial node must not be implied by other nodes, as initial nodes are base cases.

In other words, starting from a non-initial node, I must select exactly one pair of nodes which imply the target node, and do this recursively for the nodes of the pair, unless they are initial nodes, as initial nodes are base cases.

Let me give some examples. Initial nodes have an asterisk; non-initial nodes do not.

Example 1:

example 1

Suppose the goal is X. The only solution is:

  • A*, B*, A*+B*=X.

In fact, I cannot use Y+Z=X as Z is only obtainable by first having X.

Example 2:

example 2

Suppose the goal is X. There are two solutions:

  • A*, B*, A*+B*=X
  • B*, Y*, B*+Y*=Z

Suppose the goal is Z. There are two solutions:

  • A*, B*, A*+B*=X, Y*, X+Y*=Z
  • B*, Y*, B*+Y*=Z

Edit, answering to user D.W.:

I am using your suggestion of encoding your problem into a SAT problem, but I don't understand how it can possibly avoid circular dependencies. Let me spell the SAT rules which encode the problem in question and instantiate them for Example 1:

  1. Each non-initial node must be implied by one pair of nodes.
X ⟺ ABX ∨ YZX
Z ⟺ XYZ
  1. For each non-initial node, we can choose at most one implication.
(¬ABX ∨ ¬YZX)
  1. Each implication requires the implicants:
ABX ⟺ (A ∧ B)
XYZ ⟺ (X ∧ Y)
YZX ⟺ (Y ∧ Z)
  1. Each node (with the exception of the target node) can be selected only if it appears in (at least one) implication.
A ⟺ ABX
B ⟺ ABX
Y ⟺ XYZ ∨ YZX
Z ⟺ YZX

(There are probably more rules, but these are okay to start and see what happens).

Using a SAT solver, the solutions to this problem are:

  1. A, B, X, ABX
  2. X, Y, Z, YZX, XYZ

Solution 2 is contains a circular dependency.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
1
$\begingroup$

This is the HornSAT problem, i.e., testing satisfiability of Horn formulas. There is a linear-time algorithm for HornSAT that is documented in many places, so you can apply it directly to your problem.

For example, for example 1, you obtain the following HornSAT formula:

$$[(A \land B) \implies X] \land [(X \land Y) \implies Z] \land [(Y \land Z) \implies X] \land A \land B \land Y.$$

The former 3 clauses come from the 3 implications, and the latter 3 clauses come from the 3 initial nodes. This formula has a satisfying assignment that sends $A,B,X,Y,Z$ to true.

In general, you can find the minimal satisfying assignment to the HornSAT formula (which can be found in linear time), and check whether it sets the target variable to true or not; if it does, there is an implication chain. In this case, the minimal satisfying assignment sets all variables to true, and in particular it sets $X$ to true, so there exists an implication chain that reaches $X$.

Improve this answer
$\endgroup$
3
  • $\begingroup$ First, thanks for your time. I tried your suggestion, but it fails to address the circular dependency problem of Example 1. See the edit to the question. $\endgroup$ Commented Feb 4 at 15:33
  • $\begingroup$ @steddy, See edited answer where I explain in more detail. Circular dependencies are not a problem. $\endgroup$ Commented Feb 4 at 23:50
  • $\begingroup$ The OP says "enumerate all possible implication chains", not "decide if one exists" (or even "find one if it exists"). $\endgroup$ Commented Mar 7 at 17:24

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.