Reasoning with SAT and Beyond
Institute for Symbolic Artificial Intelligence – Johannes Kepler University, Austria
One of the biggest success stories of symbolic artificial intelligence is written by SAT solvers, i.e., by tools that answer the question if a given propositional formula is satisfiable or not. Despite the NP-hardness of SAT, modern solvers are able to decide huge formula instances from industrial application domains like formal verification. The performance boost of SAT solvers we have seen over the last 20 years only became possible by cleverly exploiting the problem structure of the formula, by a tight integration of powerful search and inference techniques, and advanced heuristics. Because of their power, SAT solvers are nowadays also the backend reasoning engines for solving decision problems beyond NP like QBF, SMT, and MaxSAT.
In this talk, we shortly trace the story of SAT solving and show how SAT helps to solve problems beyond NP. We identify open challenges related to other branches of symbolic reasoning and artificial intelligence.
Prof. Martina Seidl is head of the Institute for Symbolic Artificial Intelligence at the Johannes Kepler University (JKU) in Linz, Austria. She obtained her PhD from the Vienna Technical University and her habilitation in computer science from JKU. Before becoming a full professor, she was associate professor at the Institute for Formal Models and Verification at JKU. Her research focuses on symbolic reasoning techniques with special emphasis on quantified Boolean formulas and applications in formal verification and symbolic artificial intelligence. https://www.jku.at/sai/seidl