Suppose Alice, Bob, and Carla answer a question. Each of the three answers is either right or wrong. Is it 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 (or 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 solvers" - computer programs that are supposed to solve such logical tasks as quickly and efficiently as possible.

The weirdness of quantum physics

But also problems from other sciences can sometimes 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 far-reaching: by finding a list of vectors that actually satisfy this relation in the 1960s, it was possible to prove: The weirdness of quantum particles cannot be explained by assuming that they contain some sort of information that we just do not know. The reason is that the quantum world actually works differently from the classical world in a fundamental way - an important result for physics and the philosophy of science.

Having proved this, however, one can ask the mathematically highly complex question: What is the most compact way to do this proof? What is the minimum number of these vectors needed? For computer science, this is a challenging task on which to test the power of sophisticated SAT solvers.

Trial and error is not enough

In the example above with Alice, Bob, and Carla, it can simply be found by trial and error 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 appropriate vectors for the Kochen-Specker theorem), this is not possible.

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

"The space of possibilities then quickly becomes unmanageably large," says Prof. Stefan Szeider of the Institute of Logic and Computation at TU Wien. "You would then have to try through far more possibilities than there are atoms in the universe - that's practically impossible even for the best computers."

Clever tricks, less computational effort

That's why researchers around the world are working to improve 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 family of other 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 use a SAT solver to solve tasks that would otherwise be completely unsolvable. And so, step by step, by continuously improving the SAT technology, it was also possible to 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 now is: How many vectors do you need at least? For which largest possible number of vectors can you prove that no solution exists?"

World record!

Only recently, a research group from Canada was able to 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 "SAT modulo Symmetries" method developed at TU Wien, says Stefan Szeider -- but it would probably take 100 to 200 CPU years, which can be done in a few weeks on a powerful parallel computer.

That is 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.

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

Additional Links

Free version of the article:
https://arxiv.org/abs/2306.10427, opens an external URL in a new window

Code and documantation on SAT modulo Symmetries:
https://sat-modulo-symmetries.readthedocs.io/en/latest/, opens an external URL in a new window

General article about SAT:
https://cacm.acm.org/magazines/2023/6/273222-the-silent-revolution-of-sat/fulltext, opens an external URL in a new window

Contact

Prof. Stefan Szeider
Institute for Logic and Computation
TU Wien
+43 1 58801 192100
stefan.szeider@tuwien.ac.at