{"id":8640,"date":"2023-06-07T15:11:02","date_gmt":"2023-06-07T13:11:02","guid":{"rendered":"https:\/\/www.ftf.or.at\/?p=8640"},"modified":"2023-06-07T15:11:05","modified_gmt":"2023-06-07T13:11:05","slug":"beyond-np-reasoning-with-quantified-boolean-formulas","status":"publish","type":"post","link":"https:\/\/www.ftf.or.at\/?p=8640","title":{"rendered":"Beyond NP: Reasoning with Quantified Boolean Formulas"},"content":{"rendered":"\n<p><strong>Friday, June 16, 2023 | 12:30 pm (CET) | Room: S.2.69 | Alpen-Adria Universit\u00e4t Klagenfurt<\/strong><\/p>\n\n\n\n<p><strong>Univ.-Prof.in Dr.in Martina Seidl | Institute for Symbolic Artificial Intelligence | JKU Linz<\/strong><\/p>\n\n\n\n<p><strong>Abstract<\/strong>: As the prototypical NP-complete problem SAT, the decision problem of propositional logic, is considered to be hard. Despite this hardness, SAT is very successfully applied in many practical domains, because very powerful reasoning techniques are available. There are, however, problems that cannot be efficiently encoded in SAT. For such problems, formalisms with decision problems beyond NP are necessary. One of such formalisms are quantified Boolean formulas (QBFs), the extension of propositional logic with existential and universal quantifiers over the Boolean variables. The QBF decision problem is PSPACE-complete, making QBF well suitable for encoding and solving many problems from formal verification, synthesis, and artificial intelligence. In this talk, we give a short tour through recent developments in QBF solving.<\/p>\n\n\n<div class=\"wp-block-image\">\n<figure class=\"alignright size-medium\"><a href=\"https:\/\/www.ftf.or.at\/wp-content\/uploads\/2023\/06\/MartinaSeidl1_12-small.jpg\"><img loading=\"lazy\" decoding=\"async\" width=\"197\" height=\"300\" src=\"https:\/\/www.ftf.or.at\/wp-content\/uploads\/2023\/06\/MartinaSeidl1_12-small-197x300.jpg\" alt=\"\" class=\"wp-image-8641\" srcset=\"https:\/\/www.ftf.or.at\/wp-content\/uploads\/2023\/06\/MartinaSeidl1_12-small-197x300.jpg 197w, https:\/\/www.ftf.or.at\/wp-content\/uploads\/2023\/06\/MartinaSeidl1_12-small.jpg 499w\" sizes=\"auto, (max-width: 197px) 100vw, 197px\" \/><\/a><\/figure>\n<\/div>\n\n\n<p><strong>Bio<\/strong>: Martina Seidl is a full professor of artificial intelligence at the Johannes Kepler University (JKU) in Linz. She obtained her PhD from TU Wien where she worked several years in the Business Informatics Group. In 2010, \u00a0she became assistant professor and in 2016 associate professor at the Institute for Formal Models and Verification of the JKU. \u00a0Since 2020 she is head of the Institute for Symbolic Artificial Intelligence. In her research, she develops symbolic reasoning techniques based on computational logic. She especially focuses on the theory and practice of quantified Boolean formulas (QBFs) and their applications in the context of formal verification and artificial intelligence.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Friday, June 16, 2023 | 12:30 pm (CET) | Room: S.2.69 | Alpen-Adria Universit\u00e4t Klagenfurt Univ.-Prof.in Dr.in Martina Seidl | Institute for Symbolic Artificial Intelligence | JKU Linz Abstract: As the prototypical NP-complete problem SAT, the decision problem of propositional &hellip; <a href=\"https:\/\/www.ftf.or.at\/?p=8640\">Continue reading <span class=\"meta-nav\">&rarr;<\/span><\/a><\/p>\n","protected":false},"author":3,"featured_media":0,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"sfsi_plus_gutenberg_text_before_share":"","sfsi_plus_gutenberg_show_text_before_share":"","sfsi_plus_gutenberg_icon_type":"","sfsi_plus_gutenberg_icon_alignemt":"","sfsi_plus_gutenburg_max_per_row":"","footnotes":""},"categories":[1],"tags":[],"class_list":["post-8640","post","type-post","status-publish","format-standard","hentry","category-tewi-kolloquium"],"_links":{"self":[{"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=\/wp\/v2\/posts\/8640","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=\/wp\/v2\/users\/3"}],"replies":[{"embeddable":true,"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=8640"}],"version-history":[{"count":1,"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=\/wp\/v2\/posts\/8640\/revisions"}],"predecessor-version":[{"id":8642,"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=\/wp\/v2\/posts\/8640\/revisions\/8642"}],"wp:attachment":[{"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=8640"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=8640"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=8640"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}