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