MAX-SAT and MAX-cut

Question

I have been using MAX-SAT solver to obtain the exact ground state of ising spin glass model:

For 1D periodic model, for systems with 50 binary variables and interaction range of 15th nearest neighbor. The best MAX-sat solver requires 20 minutes to solve it. For 100 binary, it then becomes impossible...

However, it seems when people use graph theory max cut methods to solve this problem, they could obtain ground state of much larger scale. But I am wondering if I transform my ising spin glass problem into the format of graph cuts, would graph cut solvers perform in any way better? Is that the case that people who construct theorems for maxsat do not consider its graph cut equivalent method? For your interest, the case of my 50/100 variables problem is as followed:

https://www.dropbox.com/s/23lo7lwgd4otse9/50_softer.wcnf?dl=0 https://www.dropbox.com/s/r2r1yfpb2uzvcrn/100_softer.wcnf?dl=0

(you may see there are 64, 114 variables, but the hard constraints force the equality of the first 15th clauses with the last 15 clauses )

For your information, in most cases, the solver finds the exact ground state fast but the proving process is very slow (e.g. it takes 1 second to get the true solution while using 20 minutes proving that)...

Answer 1

In most cases, when computing graph cuts you are not interested in finding the optimal graph cut. This is true, for example, in domain decomposition of finite element meshes. In such situations, a "good" cut is often good enough. You can then use approximation algorithms and heuristics that will in general not yield the exact answer but one that is close enough. This is what, for example, the METIS package does when computing graph cuts, as well as practically all other similar packages.