2020-04-03 10:2:10 (GMT)
I have been thinking about implementing (simplified version of) Immediate Simplification that we have discussed yesterday and I realized that there is no reason why I should not implement lazy orphan deletion
2020-04-03 10:4:2 (GMT)
The idea is as in E: When the clause is chosen, we go through its derivation tree and check if there is any dead clause in the tree (e.g. it was subsumed)
2020-04-03 10:6:4 (GMT)
If so, we delete it and try to choose a clause again
2020-04-03 10:8:26 (GMT)
And as for Immediate simplification -- I think the idea can be improved -- generated clauses do not have to subsume the parent clause, but they can simplify it somehow.
Then, only the simplified parent clause and children that took part in simplification can be moved to passive and the original parent is removed from active
2020-04-03 10:15:45 (GMT)
@Simon Cruanes : Was this how you implemented orphan check before?
2020-04-03 13:5:27 (GMT)
It never worked great, but I think it was something like that: look at given clause's ancestors through simplifications and if any was subsumed/marked redundant, throw this one away too.
2020-04-03 13:13:1 (GMT)
Yeah I have implemented this and now I will evaluate it.
For some cases I get gave up (?) when orphan check is on, but the problem is proved when it is off
2020-04-03 13:13:8 (GMT)
I will check it further
2020-04-03 13:36:29 (GMT)
In an incomplete mode, it seems plausible that not deleting an orphan makes the mode a bit more complete.
2020-04-03 15:33:7 (GMT)
haha, true :slight_smile: but I still think I made an overlook somewhere
2020-04-03 16:8:24 (GMT)
I have just checked in E and Stephan deletes clauses only if immediate parents are subsumed
2020-04-03 16:9:6 (GMT)
Not even looking through simplifications.
2020-04-03 16:9:22 (GMT)
Except for efficiency, I cannot see why something like would be done.
2020-04-03 16:11:39 (GMT)
Well I guess it's the perfect time to ask @Stephan Schulz :stuck_out_tongue_wink:
2020-04-03 16:11:47 (GMT)
:slight_smile:
2020-04-03 16:22:27 (GMT)
I changed from aggressive orphan deletion to lazy orphan deletion a while back, because it is much simpler. In E, a clause is orphaned of one of the generating parents is simplified or subsumed. I doubt that you can safely remove clauses if only one of the side conditions of a rewrite step becomes redundant. If done naively, lazy orphan deletion changes search behaviour if you have multiple queues (with eager deletion, orphaned clauses never are are picked). I think I hacked around this in E (orphaned clauses do not count as picked), but that is somewhat ugly. It's just a way of keeping the accumulated but unexpressable dark knowledge that has accumulated over time....
2020-04-03 16:26:46 (GMT)
Ok let's try to systemaize this dark knowledge:
2020-04-03 16:27:29 (GMT)
From what I have (just now) check in E, version 2 is implemented with the line 344 of the file che_hcb.c
2020-04-03 16:36:33 (GMT)
You mean here ? :p
The power of URLs!
2020-04-03 20:34:52 (GMT)
Even for eager deletion, only unprocessed clauses have been deleted. E is fairly aggressive with simplification of unprocessed clauses, and I think I get away with it, because I don't delete processed orphans....
2020-04-04 9:59:31 (GMT)
Ok. Thanks for this clarification.
2020-04-04 10:0:15 (GMT)
Did you read the superposition in iProver paper?
What do you think about the altered loop, and the immediate simplification step?
2020-04-04 10:0:49 (GMT)
Some form of it can be easily implemented in E, I suppose.
2020-04-04 11:33:10 (GMT)
There's a point that arises in Stephan's first comment that I would like to emphasize. If a clause (whatever set it is in) has been used to simplify or delete (subsume) another clause, it should not be considered an orphan and should not be deleted in a refutationally complete mode.
2020-04-04 11:34:46 (GMT)
Which means that the only good candidates for orphan deletions (in a complete mode) are either those that belong to a set that's guaranteed to have not been used to process other clauses (that would be unprocessed in E I guess) or you annotate each clause with a boolean flag indicating if they've been used to process other clauses, or even pointers to these clauses.
2020-04-04 11:36:20 (GMT)
I'm not sure if any prover implements the latter (presumably in an Otter loop) -- I seem to recall Uwe mentioning something about it (Waldmeister??), but each time I mention this approach, he goes "urgh! igitt!" That's why it's not in our IJCAR 2020 paper (Section 4).