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 that it is neither true that Bob and Carla are right nor that Alice and Bob are right?

This may sound convoluted, but it is a typical example of a satisfiability (SAT) problem. Such logical issues are encountered in many different research areas. In software engineering, when one wants to prove that a particular computer program is always guaranteed to provide the correct solution. Or in the chip industry, when showing that a computer chip is guaranteed to work correctly in every logically possible situation. For this purpose, we use so-called “SAT solvers” - computer programs that solve such logical tasks as quickly and efficiently as possible.

The weirdness of quantum physics

Problems from other scientific fields can be translated into SAT problems. For example, quantum physics’s famous Kochen-Specker theorem. Its formulation is abstract: It involves a list of vectors in three- or higher-dimensional space that have very specific logical relations to each other.

The implications of the Kochen-Specker theorem are far-reaching. In the 1960s, a list of vectors that satisfy this relation was found. Through this extraordinary discovery, it was possible to prove that the weirdness of quantum particles cannot be explained by assuming they contain information we do not know. Instead, scientists learned that the quantum world works fundamentally differently than anything we have experienced before – a significant result for physics and the philosophy of science alike.

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 to test the power of sophisticated SAT solvers.

Trial and error is not enough

In the example with Alice, Bob, and Carla, we can use trial and error to learn that the entire statement is true if Alice and Carla are correct and Bob is wrong. But this is impossible for more complicated SAT problems – such as finding appropriate vectors for the Kochen-Specker theorem.

Even more so, if one is asked not only to find a particular solution but to show that a particular case can never occur – meaning that there is no logical 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 possibilities.

“The space of possibilities then quickly becomes unmanageably large,” says Stefan Szeider, Board Member of CAIML, Co-Chair of the Vienna Center for Logics and Algorithms VCLA and Professor at the Research Unit for Algorithms and Complexity of TU Wien. “You would then have to try through far more possibilities than there are atoms in the universe, which is practically impossible even for the best computers.”

If you watch this video, data may be transmitted to third parties.

Clever tricks, less computational effort

Researchers worldwide 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 otherwise unsolvable tasks. 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. With their new proof, Stefan Szeider and his team have broken this record: There must be at least 24. The proof for 25 should also be possible with the “SAT modulo Symmetries” method developed at TU Wien, says Stefan Szeider. But it probably takes 100 to 200 CPU years, which can be done on a powerful parallel computer in a few weeks.

Such a lengthy and costly proof is not sustainable – 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 play a central role in the field of artificial intelligence today.

Problems from computer science are often divided into easy and hard problems – 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 challenging 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.

World record!

Only recently, a research group from Canada was able to show: There must be at least 23 vectors. With their new proof, Stefan Szeider and his team have broken this record: There must be at least 24. The proof for 25 should also be possible with the “SAT modulo Symmetries” method developed at TU Wien, says Stefan Szeider. But it probably takes 100 to 200 CPU years, which can be done on a powerful parallel computer in a few weeks.

Such a lengthy and costly proof is not sustainable – 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 play a central role in the field of artificial intelligence today.

Problems from computer science are often divided into easy and hard problems – 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 challenging 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.

Learn more

Here you’ll find the team’s paper on “Co-Certificate Learning with SAT Modulo Symmetries”.

If you’re interested in Code and Documentation on SAT Modulo Symmetries, they have got you covered.

Want to learn more about SAT problems in general? Check out the corresponding article to the explanation video above: “The Silent (R)evolution of SAT”.