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 @ https://github.com/QuMuLab/python-nnf/issues/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 [email protected] 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 https://github.com/pysathq/pysat/issues/58#issuecomment-674045520, 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.

[kuldeepmeel]

Hi @mvcisback: it would be great if you can help with integration. Let me check with @msoos if he can point to what needs to be done.

[alexeyignatiev]

@kuldeepmeel, regarding CMS, there is quite an extensive list of features required for full integration of CMS into PySAT, which I shared with @msoos in July 2020. As far as I recall, some of easy to do, some others are not so.

[mvcisback]

@alexeyignatiev is there a stable protocol/api that a solver needs to follow in order to be a "drop in" replacement for a pysat object? Is this more or less what you're referring to or more specific to being merged in with pysat?

[alexeyignatiev]

Hi @mvcisback,

First and foremost, as PySAT is compiled on the fly when running pip install, we should make sure that CMS can be compiled with no dependencies to other libraries that pip doesn't have access to. That means no use of boost, m4ri, zlib, et cetera. As far as I recall our email exchange with @msoos last year, this should not be hard to achieve.

Regarding the interface, the following functionality is expected to get the full support of the solver:

1. Adding clauses
2. Adding xor-clauses (since this is an important distinct feature of CMS)
3. Solving and also limited solving (MiniSat-like solve_limited())
4. Setting conflict or propagation budgets for limited solving
5. Deletion of previously imposed budgets
6. Getting an unsatisfiable core (final conflict)
7. Getting a proof trace (text-based)
8. Getting a model
9. Getting the number of clauses and variables
10. Setting preferred phases for branching
11. Non-deterministic solver interruption: https://pysathq.github.io/docs/html/api/solvers.html#pysat.solvers.Solver.interrupt
12. Doing just propagation: https://pysathq.github.io/docs/html/api/solvers.html#pysat.solvers.Solver.propagate

The more is supported the better for us.

[msoos]

Hi,

After quite a bit of work, I finally managed to make pycryptosat, pyapproxmc, and pyunigen all work, with PyPi, building wheels, etc. It can just be compiled with python -m build and the resulting package used as-is. They are now all on pypi:

https://pypi.org/project/pycryptosat/ https://pypi.org/project/pyapproxmc/ https://pypi.org/project/pyunigen/

I think the most interesting addition to PySAT would likely be ApproxMC & Unigen. They are a very fast approximate model counter, and a fast almost uniform sample generator, respectively. These two are, I think, rather unique. So, I'd suggest we work on integrating ApproxMC, first, then if that works, UniGen, and finally, CMS. It'd likely the most beneficial to the users this way.

What do you think? Do you have some bandwidth to help me integrate? I think I'll need some hand-holding...

Thanks and sorry for the delay,

Mate

[alexeyignatiev]

Thanks, Mate! This is great news! Let me finish my semester-related stuff here and I will get back to PySAT afterwards. I will surely prioritise this!

[msoos]

Thanks a lot! Would be nice :) Looking forward!

[msoos]

@alexeyignatiev Hey! About half a year has passed :) Would you be available now-ish? Would be nice to integrate AppMC into PySAT! Also, we should get Arjun in there :) It's a CNF simplifier like no other!

[alexeyignatiev]

My apologies, @msoos! I seem to be underdelivering on all my promises these days. I am happy to provide callable API to these external tools. But I will need to know what is accessible of these tools. I will also most likely need some tangible help if possible. Unfortunately, time is my biggest issue these days.

[alexeyignatiev]

By the way, I tried to install the 3 tools you listed. I can install pyapproxmc and pycryptosat with ease with pip but for some reason pyunigen fails to compile as the compiler reports fatal error: 'gmp.h' file not found. Note that gmp is installed through Homebrew but the compiler invoked by pip does not seem to know where to find it.

[msoos]

Hi,

Okay, thanks! I'll try to check what I can do, I'm pushing a new version now, I'll let you know how it goes.

In the meanwhile, we can try to integrate ApproxMC! :) Can you please help me how/where to start so I can see how could I integrate? I'd love to have a go at it!

Thanks,

Mate

[msoos]

Hey @alexeyignatiev ,

Can you please check if pyunigen installs for you now? Regarding integration of pyapproxmc, what tips can you give me where to start? I don't want to make a mess :laughing: Maybe we could start by integrating pyapproxmc, it should be a lot easier, and likely would give the most benefit. We can also add GANAK after (so as to have 2 counters), should not be a big deal, either. But let's have a go at ApproxMC first!

Thanks in advance,

Mate

[alexeyignatiev]

Hi @msoos,

Thanks for the update. This is what I get now when trying to compile pyunigen:

      In file included from python/cryptominisat/src/bva.cpp:24:
      python/cryptominisat/src/occsimplifier.h:35:10: fatal error: 'boost/serialization/vector.hpp' file not found
      #include <boost/serialization/vector.hpp>
               ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
      1 error generated.
      error: command '/usr/bin/clang' failed with exit code 1
      [end of output]

So now pip's installer fails to find where boost is installed. I honestly have no idea how this normally works as different people may have it installed differently. For instance, mine is installed through Homebrew. Is there a way to let pip know where third-party dependencies are stored?

Best, Alexey

[msoos]

Hi,

I see. Let's concentrate on pyapproxmc then! Can you please tell me where we can start?

Thanks,

Mate

[alexeyignatiev]

Well, we will need to create a module called, say, pysat.allies (or .foreign, .external, or .alien or whatnot) where we put a Python file approxmc providing a well-documented API to the functionality of your tool pyapproxmc. I presume when we are done with this file, we can do the same with unigen and some other tools you mentioned (Ganak, Arjun, etc.)

I believe CMS should be treated differently since it's a SAT solver, i.e. its API should be provided directly from the module pysat.solvers, to keep it unified with the rest of the solvers.

As for the documentation of the module, I use Sphinx and normally write down all the documentation in the doc-strings of all the classes and methods. After compiling the documentation for the entire project (including the new module allies), we will get a separate module listed here.

I guess the examples module should serve as a demonstration of how I see it could be done. It has plenty of tools provided there, including RC2, an existing widely used MaxSAT solver.

[msoos]

Oh, okay, I'll try to see how to do that, python is a bit foreign to me :) I'll let you know if and when I get stuck :) In the meanwhile, do you have any good pointers how to make such a pysat.allies? Is this some kind of well-known format? Where can I find some documentation how to do it?

Thanks again,

Mate