The race for the Kochen-Specker Theorem

- EN - DE
The race for the Kochen-Specker Theorem

A world record in solving satisfiability problems was achieved at the Vienna University of Technology - it is quite abstract, but the technology behind it is extremely important for hardware and software industries.

Suppose Alice, Bob, and Carla answer a question. Each of the three answers is either correct or incorrect. Is it logically possible that at least two of the answers are correct, at least one is incorrect, and furthermore that it is neither true that Bob and Carla are both correct, nor that Alice and Bob are both correct?

This may sound a bit convoluted, but it is a typical example of a satisfiability problem (also SAT problem). Such logical problems are encountered in many different research areas - for example in software engineering, when one wants to prove that a certain computer program is always guaranteed to provide the correct solution. Or in the chip industry, when one has to show that a computer chip is guaranteed to work correctly in every logically possible situation. For this purpose one uses so-called -SAT-Solver- - computer programs, which are to solve such logical tasks as fast and efficiently as possible.

The strangeness of quanta

But also problems from other sciences can be translated into SAT problems, for example the famous Kochen-Specker theorem from quantum physics. Its formulation is somewhat abstract - it involves a list of vectors in three- or higher-dimensional space that have very specific logical relations to each other.

But the implications of the Kochen-Specker theorem are very far-reaching: by finding a list of vectors that actually satisfy this relation in the 1960s, it was possible to prove: The fact that quantum particles behave fundamentally differently from classical objects is not because anything about them is not yet known, but because the quantum world actually works differently from the classical world - an important result for physics and the philosophy of science.

After proving this, however, one can ask the mathematically highly complex question: What is the most compact way to do this proof? How many of these vectors do you need at least?

For computer science, this is a challenging task on which to test the performance of sophisticated SAT solvers.

Trial and error is not enough

In the example above with Alice, Bob, and Carla, one can do a little trial and error and find that the entire statement is true if Alice and Carla are right, and Bob is wrong. But for more complicated SAT problems (such as finding matching vectors for the Kochen-Specker theorem), this is not possible.

It is particularly difficult when one is not only supposed to find a certain solution, but instead to show that a certain case can never occur - that, for example, there is no logically possible input at which a computer program or a computer chip fails. After all, to prove this with absolute certainty, one would have to try all possibilities.

-The space of possibilities then quickly becomes unmanageably large," says Stefan Szeider from the Institute for Logic and Computation at the Vienna University of Technology. -You would then have to try out far more possibilities than there are atoms in the universe - that is practically impossible even for the best computers.

Clever tricks, less computing effort

Therefore, people all over the world are working on improving SAT solvers by using clever tricks. They take advantage of the fact that the question has a very specific structure: Sometimes it is not even necessary to test all logically conceivable possibilities. Sometimes it can be shown that some of them are symmetrical to each other: If one is false, then a whole list of possibilities is also false, which are merely symmetrical images of the first one. In this case, after a single test, one can exclude a whole branch of possibilities without having to try them one by one.

If one cleverly exploits such symmetries, one can solve tasks with a SAT solver that would otherwise be completely unsolvable. And so, step by step, through continuous improvement of the SAT technology, one could also approach the question of how many vectors one needs to solve the famous Kochen-Specker theorem of quantum physics (in three-dimensional space).

-It was clear: There are at most 31 - because a solution with 31 vectors is known-, says Stefan Szeider. -But the question is now: How many vectors are needed at least? For which large number of vectors can one prove without gaps that it does not allow a solution?-.

World record!

Only recently a research group from Canada could show: There must be at least 23 vectors. Stefan Szeider and his team have now been able to break this record: There must be at least 24, according to the new proof. The proof for 25 should also be possible with the method "SAT modulo Symmetries" developed at the Vienna University of Technology, says Stefan Szeider - however, this would probably require 100 to 200 CPU years, which can be done in a few weeks on a powerful parallel computer.

It’s not really worth it - after all, it’s not about the result itself, but rather the technology behind it. SAT solvers have become an indispensable part of modern technology, and they also play a central role in the field of artificial intelligence today.

Often problems from computer science are divided into easy and hard problems - so called P and NP problems. The satisfiability problem is one of the hardest problems of the complexity class NP and therefore in general probably difficult to solve. But recent breakthroughs in SAT technology show: This dichotomy is not the whole story. Even when one is dealing with particularly difficult problems, one can sometimes cleverly exploit their structure to make computable what at first glance seems utterly hopeless.

Free access version of the actual article:

Program and documentation on SAT modulo Symmetries:

review articles on SAT:­023/6/2732­22-the-sil­ent-revolu­tion-of-sa­t/fulltext