Approximate model counters/Probabilistic solvers

[jpsety]

Thanks for creating this library, it's helped a lot in my work.

Any chance you would consider integrating work such as:
https://github.com/meelgroup/ApproxMC
or
http://fmv.jku.at/yalsat/
?
I feel like they would fit nicely with the package.

[alexeyignatiev]

Thanks for the kind words. I completely agree that adding more SAT-related technology in PySAT would be great. In particular, integrating some effective approximate model counting algorithms would be amazing. But, unfortunately, that would require a significant time investment into something I am not an expert on. So I can't guarantee that it will be added any time soon, sorry.

Having said that, volunteers are more than welcome! :)

@kuldeepmeel, any chance that you have people to do that? ;)

[yxliang01]

I think this is going to be a very useful feature!

[haz]

@alexeyignatiev I might be able to help with this (I've authored a previous SoA knowledge compiler, have student projects upcoming to work on items like this, etc). We already have dsharp (knowledge compiler built on the sharpSAT model counter) included in the nnf package (which makes sense, as it converts from CNF to d-DNNF). It also implements AMC (so weighted model counting and the like).

I think a more important question is what functionality we'd like to see split among the two packages.

[alexeyignatiev]

@haz thanks a lot! It would be great to have it working here!

[haz]

What would the general interface/requirement be? Originally I considered not a big leap, but notions of incremental interaction seem to open a can of worms -- especially when it comes to knowledge compilation/model counting techniques.

Also, feel free to open up a general issue here or join the discussion @ QuMuLab/python-nnf#10 to see how we might bridge the two initiatives (e.g., just have a pysat backend to nnf functionality, or something more sophisticated?).

[alexeyignatiev]

Hm, I don't see an obvious way to go here. Do you need any functionality of PySAT for that? If not, we could create something on PySAT's side to interface with python-nnf. Otherwise (and I presume this is the case as you guys are looking into using SAT solvers from PySAT), we may need a more sophisticated interaction.

[haz]

I think it's important to keep the two threads separate: I piped up on this thread since I authored DSHARP and am still familiar with the internals there. But if incremental aspects are central to the project, I'm not sure I could swing that without finding a student to focus on the project.

As for pysat<->python-nnf interaction, the latter would certainly make use of the former (entailment, equivalence, satisfiability, etc are all functionality on the interface with naive implementations that could be improved using a SAT backend). As you point out, with AIGER support native to pysat, I'm not sure what else you might want -- if there is something you think would be useful, then we can consider how best to make that work.

[alexeyignatiev]

OK, sure.

[kuldeepmeel]

Sorry for delay in getting back to it. Yes, it would be nice to do the integration; we just released ApproxMC as library, so it should be doable. We will put it on the stack of things to do; what do you think @msoos ?

[msoos]

Hi, I'm on vacation :) I'll get back to this in 10 days. It should be pretty easy to integrate. I wanted to do CMS too, sorry for the delay, lots of things came up! Mate

…

On Fri, Aug 14, 2020, 14:15 Kuldeep S. Meel ***@***.***> wrote: Sorry for delay in getting back to it. Yes, it would be nice to do the integration; we just released ApproxMC as library, so it should be doable. We will put it on the stack of things to do; what do you think @msoos <https://github.com/msoos> ? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#58 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAKF4ONXFW7NQ6KNBYIF2F3SAUTFDANCNFSM4OXCJR2A> .

[alexeyignatiev]

Thanks for the comments, @kuldeepmeel and @msoos. Again, it would be great to see it working in Python and in PySAT. :) The same holds for CMS!

[alexeyignatiev]

@msoos, any news on CMS + PySAT? :)

[mvcisback]

@msoos @kuldeepmeel @alexeyignatiev Was wondering if there was any news on this? I'm using CMS by subprocesses, but would much rather operate through PySAT if possible. Happy to help with integration if I get pointed in the right direction.

[alexeyignatiev]

@mvcisback, sorry for the late response! I am not sure if this will ever happen. Unfortunately, I don't have time for this in any foreseeable future. I guess @msoos might have a similar problem. But let's see what/if he replies.