Search code examples
graphdependenciesconflictboolean-logicboolean-operations

Resolving graphs (possibly containing cycles) of dependancies and conflicts


Given a graph where each node may contain arbitrary dependencies or conflicts with other nodes leading to any possible arrangement including circular and contradictory references.

I'm trying to compute a stable result list maximally containing a list of nodes able to respect all of their constraints. I just need to find one possible solution if there is one to be had.

In the examples below "A depends on B" means for A to be true B must be true. "B conflicts with A" means for B to be true A must not be true. There is no precedence both dependencies and conflicts with have equal weight and apply concurrently.

On 3rd example 'A' does not appear because it depends on D which conflicts with B. Since A also requires B .. A cannot exist as D's conflict and A's dependencies forbid it.

A depends on B
B conflicts with A
= B

A depends on B
B depends on A
= A and B

A depends on B
A depends on D
B depends on C
D conflicts with B
D conflicts with C
= B and C or D

A conflicts with B
B conflicts with C
C conflicts with D
D conflicts with A
= A and C or B and D

I've been trying to come up with an algorithm that works but so far my efforts resemble heuristical gobblygook which fail spectacularly on non-trivial graphs. Any insights, pointers to reading material or names of algorithms would be much appreciated.


Solution

  • I assume that

    • "A depends on B" means A implies B and
    • "B conflicts with A" means B implies not A.

    Now, you have A implies B = not A or B and B implies not A = not B or not A. This means that the problem boils down to finding a solution for a conjunction of disjunctions (also known as clauses) where each clause has two arguments (A, not A, B, or not B).

    This problem is known as 2-satisfiability. You find polynomial time algorithms in the web, e.g., start at http://en.wikipedia.org/wiki/2-satisfiability.

    As far as I understand resolution in modern SAT solvers, there is no need to write your own algorithm. A SAT solver should be able to solve such instances automatically in polynomial time.