> Crudely their proof works as follows. First, the two scientists note that the up-or-down Ising spin resembles the true-or-false character of a logical statement such as "the car is white." They then prove that any particular 2D Ising model—i.e., with a particular set of coupling and external fields -- is equivalent to an instance of a logical problem called the satisfiability, or SAT, problem, in which the goal is to come up with a set of logical statements, A,B,C, … that satisfy a long logical formula such as "A and not (B or C) …" The theorists present a way to map the SAT problem onto the 2D Ising model.
> Next, they show how any other spin model can also be translated into a SAT problem. That SAT problem can then be translated onto the 2D Ising model, thus making the two spin models equivalent. There is a price to pay, however. The 2D Ising model must have more spins than the original spin model. But De las Cuevas says that the computational demands of the Ising model are only modestly bigger than those of the original model.