[Matryoshka-devel] [paper] superposition + induction at Frocos 17

Giles Reger giles.reger at manchester.ac.uk
Tue Jun 27 01:19:25 CEST 2017


Hi again,

>> Thanks for the reply. I am not sure I fully understand what you have implemented. Without the freezing/unfreezing it sounds more like splitting without backtracking [1,2] depending on how you introduce the assertions… but I now cannot see a discussion of this in the current version. Indeed it is not clear how superposition is lifted to clauses with assertions, or are the assertions treated as propositional symbols? If the labels are separated how do reductions deal with them? If they are treated as propositional symbols then they are likely to get in the way of reductions.
> 
> I have clauses with assumptions, same as in AVATAR (i.e. a set of
> boolean literals which are not part of the clause itself).
> The clauses are really of the form C ← A, and there is no overhead
> at the level of superposition.
> 
> Inferences inherit the union of the assumptions of the premises (if
> compatible); reductions only work if the rewriting clause's assumptions
> subsume the rewrited one (so I support branch-aware
> demodulation/subsumption/clc).
> 
>> Of course AVATAR was directly inspired by splitting without backtracking but separating the assertions from the first-order reasoning AVATAR is the way that the assertion-reasoning is performed exclusively by a SAT solver and how the labels do not get in the way of first-order reasoning (which they do in splitting without backtracking).
> 
> I do the same, the SAT solver is used to find UNSAT in the end, and
> prune clauses whose assumptions are false at level 0.
> 
> The thing I did not implement is to disable clauses whose assumptions
> are false in the current model, because it would require a lot of work
> on term indices (if I understood correctly the AVATAR paper).
> 
>> My inference is that you only use the SAT solver in one direction i.e. to collect constraints not to assert a model, am I right?

Thank you for the clarification. 

So my final statement seems correct and my early observation that this might be more in the direction of splitting without backtracking is not.

For me there is one last question, which is how you introduce the clauses with assumptions. Do you immediately split a clause on creation and replace the clause by its components? Our Playing with AVATAR paper explored different variations of this choice and others. I might play with this idea of keeping all branches live at once, but my immediate feeling is that it would not have a distinct advantage (I guess you’re not claiming it does, just that you didn’t want to implement the branch assertion bit).

You are correct that the disabling requires quite a bit of book-keeping. The most complicated part is handling “conditional reductions” where a clause depending on A,B is reduced by a clause depending on A and then A is retracted but B is not so the reduction must be undone. There is also a very horrible special case within a special case within a special case in the Vampire code that makes Martin Suda angry whenever we discuss it.

I do feel that some of these things are not clear in the current version of the paper (probably something you don’t want to hear). Although I don’t remember having such thoughts the first time I read it!

>> By the way, would you like a version of Vampire to allow you to add it to Figure 5? ;)
> 
> Heh, thanks, but that would make the horizontal axis far too wide ;)
> 
>> 
>> I can also recommend using StarExec for such experiments as Geoff maintains a set of solvers that you can borrow for your own experiments without the hassle of installing them yourself.
> 
> Indeed, that's a good point. I run my own script for collecting results
> but it's not very scalable.

StarExec allows us to run experiments with millions of comparisons to compare various heuristics. Without it we’d find it difficult to understand how various combinations perform.

> Thanks for all the comments! If you have further questions I'm glad to
> discuss with fellow superposition prover authors!

It is nice to see that some of the AVATAR ideas are being used elsewhere.

Cheers, Giles


More information about the matryoshka-devel mailing list