Parallel solving

[corazza]

Hello, is it possible to utilize more threads/cores when solving a SAT problem? Currently I'm using Glucose4. If not, is it even possible in principle?

[felixvuo]

Glucose comes with glucose-syrup, which uses multiple threads to solve SAT in parallel. For me, it's in GLUCOSEDIR/parallel/glucose-syrup_static.

…

On Mon, 8 Feb 2021 at 07:25, Jan Corazza ***@***.***> wrote: Hello, is it possible to utilize more threads/cores when solving a SAT problem? Currently I'm using Glucose4. If not, is it even possible in principle? — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#70>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ANFAAS357F2HWX5Z6NBXLH3S56GU5ANCNFSM4XIOT63Q> .

-- Felix Ulrich-Oltean PhD Student in Artificial Intelligence, AI Seminars Admin Department of Computer Science, University of York

[corazza]

@felixvuo thanks, any idea how to use it in PySAT? I tried searching the repo, there don't appear to be any references to syrup in the code

[alexeyignatiev]

Hi @corazza,
Nothing prevents you from creating multiple solver objects and running them simultaneously. You can do something along these lines:

#!/usr/bin/env python

import logging
import multiprocessing
from pysat.examples.genhard import PHP
from pysat.solvers import Solver
import time

logger_format = '%(asctime)s:%(threadName)s:%(message)s'
logging.basicConfig(format=logger_format, level=logging.INFO, datefmt="%H:%M:%S")

def run_solver(solver, pigeons):
    """
        Run a single solver on a given formula.
    """

    logging.info(f"starting {solver} for {pigeons} pigeons")
    with Solver(name=solver, bootstrap_with=PHP(pigeons-1)) as s:
        res = s.solve()
    logging.info(f"finished {solver} for {pigeons} pigeons -- {res} outcome")

if __name__ == '__main__':
    logging.info("Main started")
    logging.info("Creating tasks")

    threads = [multiprocessing.Process(target=run_solver, args=(solver, pigeons)) \
            for solver, pigeons in zip(['mpl', 'cd', 'g4', 'g3', 'm22'], [11, 10, 9, 8, 7])]
    for thread in threads:
        thread.start()
    for thread in threads:
        thread.join() # waits for thread to complete its task

    logging.info("Main Ended")

If I run this, I get the following output:

22:11:27:MainThread:Main started
22:11:27:MainThread:Creating tasks
22:11:27:MainThread:starting mpl for 11 pigeons
22:11:27:MainThread:starting g4 for 9 pigeons
22:11:27:MainThread:starting cd for 10 pigeons
22:11:27:MainThread:starting g3 for 8 pigeons
22:11:27:MainThread:starting m22 for 7 pigeons
22:11:27:MainThread:finished m22 for 7 pigeons -- False outcome
22:11:27:MainThread:finished g3 for 8 pigeons -- False outcome
22:11:28:MainThread:finished cd for 10 pigeons -- False outcome
22:11:29:MainThread:finished g4 for 9 pigeons -- False outcome
22:11:40:MainThread:finished mpl for 11 pigeons -- False outcome
22:11:40:MainThread:Main Ended

[alexeyignatiev]

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

[felixvuo]

Ah, apologies for "answering" out of context.

…

On Mon, 8 Feb 2021 at 11:15, Alexey Ignatiev ***@***.***> wrote: @felixvuo <https://github.com/felixvuo>, PySAT does not include the glucose-syrup solver. So please do not spread misinformation. :) — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#70 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ANFAAS56USP3SWSJRZXNZDLS57BUXANCNFSM4XIOT63Q> .

-- Felix Ulrich-Oltean PhD Student in Artificial Intelligence, AI Seminars Admin Department of Computer Science, University of York

[corazza]

@alexeyignatiev Hi, I don't have a lot of experience with SAT solvers and I don't know how they work, but is that really the best that can be done in theory? I don't really see how this would help me solve a single formula faster, which is what I need.

[alexeyignatiev]

@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. On the other hand, if you intend to use a portfolio of solvers or to parallelize a specific problem-solving approach (say by splitting the formula on a bunch of variables) then you can use the idea I outlined above.

[alexeyignatiev]

Having said that, I may consider including some of the parallel solvers into PySAT in the future, time permitting.

[corazza]

Ah right, you mean if I have A(X1, ..., Xn) I could split it into A(0, ..., Xn) and A(1, ..., Xn) and it should be faster

[alexeyignatiev]

Yes, that is what I mean. Also, observe that you can split on more than 1 variable. Say on k variables, which will give you 2 ** k simpler CNF formulas. But notice that although intuitively the formulas should be simpler, they are not guaranteed to be solved much faster than the original formula. Also, in many cases, not all variables are equally good to split on. If your formula encodes a computation process (e.g. a circuit or a program) then it seems better to split on (a subset of) input variables.

[souravsanyal06]

Having said that, I may consider including some of the parallel solvers into PySAT in the future, time permitting.

Is this feature available ?

[alexeyignatiev]

No, there are no parallel solvers in PySAT at this point. You are more than welcome to add some!

[souravsanyal06]

thanks @alexeyignatiev for the quick response!! I have come across some divide and conquer based SAT solvers which uses lookahead techniques in literature. Some of them can be used to partition search spaces. I have noticed some C/C++ based implementations such as the Cube and Conquer....I was wondering if such a lookahead based search space partitioning function exists in python anywhere. Please let me know if you happen to know of some!

[alexeyignatiev]

No worries, @souravsanyal06. To be honest, I haven't come across any lookeahead-like partitioning procedures written in Python. But I've never tried to find one.

[souravsanyal06]

@alexeyignatiev I went ahead and implemented one myself. It was taking too long even for clauses of length 100. That explains why there is no python implementation!

[alexeyignatiev]

@souravsanyal06, well, I can't say I am surprised. I guess there could be one implemented in C/C++ and interfaced through Python.