Alexey Ignatiev

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...

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...

Hi @you-li-nu, This is a very good question. Unfortunately, I don't know of any MaxSAT solvers that support incrementality in the manner of MiniSat-like assumptions interface. Actually, implementing one efficiently...

I can't say that I understand much. Is it correct that your p's are just unconstrained variables used in F's and the (unweighted) soft clauses are pairs (yi, yj)? Also,...

Hi Guannan, Well, I am afraid the best option for you may be to recreate a solver from scratch, just like what you already do. Alternatively, you can try to...

Hi @yxliang01, I agree that it would be great. This feature would help a lot in many use cases. Therefore, PRs are welcome! :) Otherwise, I will take a look...

Unfortunately, I cannot estimate when this could be done. BTW, what kind of simplification do you mean? Two-level minimization or formula preprocessing?

Hi @corazza, Nothing prevents you from creating multiple solver objects and running them simultaneously. You can do something along these lines: ```python #!/usr/bin/env python import logging import multiprocessing from pysat.examples.genhard...

@felixvuo, PySAT does not include the glucose-syrup solver. So please do not spread misinformation. :)

@corazza, if you want to use a standalone parallel SAT solver dealing with a single CNF formula then you should consider something like Glucose-syrup, or plingeling, or whatever solvers exist....