Operation on trees

[magg]

Hello guys

I'm doing some research and I would like to do some tests with Molly, first I need to leverage the directed bipartite graph or proof tree you talk about on the paper to do some operations on the trees, before passing it to the SAT solver. Is there a representation of the lineage graph before the CNF generation step?

Can you help me with this? I'm not sure this is the right place for this kind of discussion, do you have a mailing list or something?

thanks!

[palvaro]

Hi Miguel,

I'm very curious about the operations you are interested in doing on the trees before encoding. we are probably working on some similar stuff in my lab (we plan to use the same solving machinery on a variety of different inputs, including microservice call graphs and OS-level provenance graphs in addition to dedalus lineage). so we have been exploring a common intermediate representation and a variety of graph simplification techniques that may be relevant to your work.

also, we are just a few weeks away from completing a python port of molly that may be easier to work with and extend.

Peter

[palvaro]

We don't have a mailing list... but we probably should. I will get back to you about this.

[magg]

hi @palvaro

It's just an idea, i'm interested in trying different kind of algorithms instead of ILP or SAT solvers, and also different SAT solving algorithms. So it would be helpful to be able to manipulate the graph before and after enconding. Ok then I will wait for the python port, hopefully it won't take long.

[at15]

@palvaro you can also try gitter