John just raised the point that the size problem would be solved by using a 'full' adjacency matrix on the usable set (instead of all clauses). This would indeed give us a square of n size, with the triangular half of it filled. It might also be interesting in that it would allow us to, more easily, represent numerical statistics. These might include the number of clauses that were subsumed by a particular set of clauses, the number of children or the distance from the proof.
On the less positive side, it is possible that the plot might tend toward completeness. This may be a boon however as there may be some relation between its tendency toward completeness and the likelihood of finding a proof. Also, with a denser graph it may be reasonable (though probably quite naive) to assume that any blank space will be more meaningful.
These issues need, and deserve, to be addressed by implementing this idea. Sounds like I'm going to be trying to get a lot of little things done tomorrow.
Subscribe to:
Post Comments (Atom)
No comments:
Post a Comment