Alexey Ignatiev

Results 55 comments of Alexey Ignatiev

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

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

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

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, well, I can't say I am surprised. I guess there could be one implemented in C/C++ and interfaced through Python.

Currently, all the randomness is intentionally disabled in PySAT, to ensure deterministic behaviour of the solvers. It could be indeed helpful to have a way to set it in some...

@algebravic, yes, you are right that CaDiCaL may still be using some of the randomness-tweaking parameters. In practice, I tend not to use CaDiCaL a lot because in incremental settings...

Thanks for reporting. No, there was no intention to detect errors while parsing. Parsing of formulas is already a bottleneck, and making it more clever would only slow this functionality...

As far as I understand, nothing should prevent PySAT to be used in parallel using let's say `threading`. I haven't tried it myself, but I remember implementing signal handling to...

That's great to know, @WonJayne! Can you share some concrete recipe with us so that I could probably add it to the [documentation](https://pysathq.github.io/docs/html/index.html)? (Because, as I mentioned before, I haven't...