'PortfolioPRS is only available on dist mode for now' in multithreaded mode

[olegzaikin]

Hello, dear Painless developers! Thank you for you solver!

Given a CNF problem.cnf and 16 CPU cores, I run Painless as follows

./painless_release -v=1 -shr-strat=4 -shr-sleep=100000 -sbva-count=12 -ls-after-sbva=2 -sbva-timeout=1000 -c=16 -t=5000 ./problem.cnf

and

./painless_release -v=1 -shr-strat=3 -shr-sleep=100000 -sbva-count=12 -ls-after-sbva=2 -sbva-timeout=1000 -c=16 -t=5000 ./problem.cnf

As far as I understand, these are two configurations from SAT Competition 2024.
In both cases Painless gives an error 'PortfolioPRS is only available on dist mode for now'
When I add -simple to the command line, both variants run without errors.
I have the following questions.

1. Is it correct to use -simple like I do?
2. Could you please add an example of a multithreaded launch on a PC (i.e. not in dist mode) to the documentation at the github page?
3. Do I run Painless in the SAT competition 2024 configurations correctly (taking into account added -simple)?

[S-Mazigh]

Hello, I apologize, for the massive delay, I didn't get the notification.

For the 2024 version, there are not a PortfolioPRS, I think you are on the TACAS release(v1.24.10), where I changed the main(). In the main function (painless.cpp) we choose between the two strategies PortfolioPRS and PortfolioSimple using the "-simple" option.

Thus in order to have a classical portfolio with all the integrated solvers you use the -simple option, if you want to use the PortfolioSBVA (the one in, you would need to change the main function where the "working" pointer is initialized.

For instance, we have in the v1.24-isc24 (the SAT Competition Release) the following code:

// Init working
   if (dist)
      working = new PortfolioPRS();
   else
      working = new PortfolioSBVA();

I will do my best to enhance the documentation when I get the time. In the mean time, please tell me if your issue was resolved, and you can contact me by email at "mazigh.saoudi@epita.fr", since github notifications don't appear to be working for me.

Sincerely,
Mazigh