Fast software lolz

Re the last post, quest for propositional logic validation in O(N)

Firstly, since this post contains algorithms, I'd better say:

The algorithms described in this post, are copyright John Morrice, 2010, under the GNU Free Documentation License. http://www.gnu.org/licenses/gpl.html


.......where were we?
Unfortunately, the input will certainly NOT be well formed.

But I think I have such an algorithm. First, a concrete example.

First, a key.
P->Q
or similar arrows
means P implies Q

That is, Q must be true when P is true.

P-!>Q means P implies not Q. That is, Q must not be true when P is true.

Now the example:
What we will receive is a graph. It's simple, but has enough sophistry.

A-!>C
|   ^
|   |
v   |
B----

So what can we do?
Well first, it's fairly efficient to find which atoms are not implicated. In my particular application, I reference counting works well, since the graphs are created by user input. If each atom counts the number of other atoms which implicate it, the overhead of this would be constant. Which is good.

So we find A is not implicated. IMPORTANTLY, this means it has an empty implication set.

We see A->B. And A-!>C. We ALWAYS look at implications first.

B gets A's empty implication set, and adds A to it.

We see B->C. C gets B's implication set, and adds B to it.

Now we try the other path, A-!>B. We see that B has A in its implication set, and note that there is a contradiction.

What just happened?!

The algorithm:
Find unimplicated atoms, As.
For each A in As, validate(A, empty).

Validate(A, implication_set):
Set A.implication_set to a clone of implication_set
Get Is, the atoms implicated by A.
Get NIs, the atoms implicated to not be true by A.
For each I in Is, validate(I, insert A into implication_set)
For each NI in NIs, Contradiction?(NI, A)

Contradiction?(C, A):
if A is member of C.implication_set
then there is a contradiction

Comments:

This algorithm works along sequences of implications. For instance, if we started with:
A-!>B
|   ^
|   |
v   |
C   |
|   |
|   |
v   |
D----

Then when we arrive at C->D and D's implication set would be C's implication set, with C added. Then we arrive at B, and all is as it was before.

Also notice, that either C or D above, could imply not B and the contradiction would still be detected.

Furthermore, assigning an implication set to each atom memoizes the result of the computation. We could take the atoms A B C and D and run them as a part of another graph, without having to recompute the relationships between the atoms A B C and D.

Also note that as a side affect of the memoization, each relationship only needs to be visited once. This means that an optimum implementation of this algorithm will run in O(N) time, where N is the number of relationships in the graph.

However, this algorithm is presented in pseudo code. If you were to try and visualize how it would run on a stack-based machine, you would find it would grow the stack.
What I need is a better implementation of it ;)