How to set the Solver's verbosity?

[hadipourh]

Dear Pysat developer's team,

Thanks for creating such a useful toolkit. I want to solve a SAT problem encoded as a CNF. I am using the following commands to read the dimacs file containing the obtained CNF:

cnf_formula = formula.CNF(self.cnf_file_path)
sat_solver = solvers.Cadical()
sat_solver.append_formula(cnf_formula)
result = sat_solver.solve()

What is important for me is seeing the outputs generated by the chosen SAT solver, when it is solving the problem, since SAT solvers usually print out useful data, such as the amount of used time, and memory, and some other useful data related to the solving process. So, how can I set the verbosity parameter of a SAT solver to see more details of solving process? Thank you in advance for your help.

Kind regards,
Hosein

[alexeyignatiev]

Hi Hosein,

You can't set verbosity of a solver. At this point, it is completely disabled. You can get some really basic statistics though by using accum_stats().

[hadipourh]

Dear Alexey,

Thanks for your reply. accum_stats() works well. I used it for Cadical as follows:

from pysat.solvers import Cadical
from pysat.examples.genhard import PHP
cnf = PHP(nof_holes=2)
with Cadical(bootstrap_with=cnf.clauses) as C:
    result = C.solve()
    stats = C.accum_stats()
print(result)
print(stats)

False
{'restarts': 0, 'conflicts': 2, 'decisions': 1, 'propagations': 9}

However, it would be very better if we could see the progress report generated by the solver on the fly, when the solver is running in the background. For example when I use Cadical separately, outside of Pysat, it prints out the progress report of solving process including the remaining percentage. Users might need to see the remaining percentage of solving process, especially when it takes too much time. I hope you consider this property in the future releases. Thank you again for your time, and efforts.

Kind regards,
Hosein

[alexeyignatiev]

Hi Hosain,

I agree that it would be great to have this done. But I am not sure when/if I will time for this... Again, any volunteers are more than welcome. :)

Alexey

[hadipourh]

Hello Alexey!

I will try to see how can I add this property, but I am not sure whether I can do it or not. I would be grateful if you let me know where I should start from. It must be related to the solvers module, yes?

[alexeyignatiev]

There are two parts that need to be changed here: (1) the solvers module and (2) the pysolvers C++ extension. Let me be honest: while doing part 1 is easy, the second part is going to be really tough. :) Let me think about how it could be done.