RC2-MaxSAT-Solver cannot solve the instances from MaxSAT-Evaluation2012 (unweighted random track)?

[silent567]

Hi,

Thank you very much for providing such a clean interface to the state-of-the-art SAT solvers in python. It does save a lot of time of mine.

I am new to this field and want to find a MaxSAT solver that performs well and that is easy to use. Your RC2-MaxSAT-solver in the pysat.examples.rc2 module seems to be a good choice. The solver performs perfectly on simple instances. However, when I evaluate the solver on the benchmark provided by MaxSAT-Evaluation2012 (unweighted-random-track), it seems that the solver cannot solve even one single instance. My program just won't stop.

This seems really unnormal. Could you please help me solve this problem? Thank you very much! (One potential problem that I identify is that the solver only utilizes one single CPU core, which seems to be irregular for an optimization tool?)

The core of my codes is as follows:

def compute_solution(path):                                                                                                        
    if '.cnf' in path:                                                                                                             
        sat = CNF(path).weighted()                                                                                                 
    elif '.wcnf' in path:                                                                                                          
        sat = WCNF(path)                                                                                        
    else:                                                                                                       
        raise ValueError("Wrong format of the formula file: %s"%path)                                           
    cost, solutions = sat.topw, []                                                             
    with RC2Stratified(sat) as rc2:                                        
        for m in rc2.enumerate():
            print(m, rc2.cost, cost)                                          
            if rc2.cost > cost:                                  
                break                               
            else:                       
                cost = rc2.cost                                                  
                solutions.append(m)                                
    return sum(sat.wght)-cost, solutions

[alexeyignatiev]

Hi @silent567,

First of all, thanks for using PySAT!

Several comments:

• RC2 is one of the best-performing solvers. It won MaxSAT competitions in 2018 and 2019 and is still ranked among the best solvers in 2020. :) I mean it should be able to deal not only with "simple instances". :)
• Which instance exactly are you trying to solve? Can you attach it here?
• Note that you are enumerating MaxSAT solutions here - not just solving a MaxSAT instance. And the number of models may be exponential...
• Core-guided MaxSAT solvers (which RC2 is an example of) are known to work best on industrial instances - not the random ones.
• In order to get better performance, it may be a good idea to use one of the competition configurations (RC2-A or RC2-B). Here you are using the baseline version.
• Finally, RC2 is installed as an executable with PySAT. So if the PATH is set correctly, you should be able to run the solver simply by doing $ rc2.py [options] instance.wcnf.

[silent567]

Hi @alexeyignatiev ,

Thank you very much for your quick response!

Which instance exactly are you trying to solve? Can you attach it here?

• As for the dataset, I just randomly choose instances from the MaxSAT-Competition-2016 benchmarks (random unweighted track). The benchmark can be downloaded using this link: http://www.maxsat.udl.cat/16/benchmarks/ms_random.tgz . I also randomly choose one instance and attach it here. s2v120c1400-9.txt (This is in the CNF format) Note that you are enumerating MaxSAT solutions here - not just solving a MaxSAT instance. And the number of models may be exponential...
• I also notice this about 2 hours ago. And I change the enumeration to compute(). However, the solver haven't stopped in two hours... Core-guided MaxSAT solvers (which RC2 is an example of) are known to work best on industrial instances - not the random ones.
• This is also one of my concerns. But I am not familiar with the SAT field. Would you like to suggest other solvers (for the random instances) or some related materials (e.g., distincation between random and industrial for the MaxSAT problem)? Thanks! In order to get better performance, it may be a good idea to use one of the competition configurations (RC2-A or RC2-B). Here you are using the baseline version.
• I will then try those competition configurations!! Finally, RC2 is installed as an executable with PySAT. So if the PATH is set correctly, you should be able to run the solver simply by doing $ rc2.py [options] instance.wcnf.
• Thanks for the suggestion. But I need to save the results. So, I may still need to use it within python. The interface is already clear enough~

[alexeyignatiev]

I can confirm that none of the core-guided solvers I have access to performs well on this random instance. In general, MaxSAT solvers based on the use of CDCL SAT oracles (including core-guided solvers) do not perform well on random instances. So if you want to specifically target random instances, you may want to try using incomplete solvers, e.g. based on local search. On the contrary, local search solvers perform poorly on industrial instances (those that encode a real practical problem) while CDCL-based solvers normally do a great job solving them (e.g. see https://maxsat-evaluations.github.io/ for benchmarks, solvers and results).

[silent567]

Thank you very much for the resources! I will then learn more about the difference among instances (random VS industrial etc.). Hoping I can find one solver that best suits my own problem~ Thanks!