2026-07-26T21:31:41Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20550 2024-08-19T06:03:43Z ddc:004 open_access

Strategy Extraction by Interpolation Slivovsky, Friedrich QBF Expansion Strategy Extraction Interpolation In applications, QBF solvers are often required to generate strategies. This typically involves a process known as strategy extraction, where a Boolean circuit encoding a strategy is computed from a proof. It has previously been observed that Craig interpolation in propositional logic can be seen as a special case of QBF strategy extraction. In this paper we explore this connection further and show that, conversely, any strategy for a false QBF corresponds to a sequence of interpolants in its complete (Herbrand) expansion. Inspired by this correspondence, we present a new strategy extraction algorithm for the expansion-based proof system Exp+Res. Its asymptotic running time matches the best known bound of O(mn) for a proof with m lines and n universally quantified variables. We report on experiments comparing this algorithm with a strategy extraction algorithm based on combining partial strategies, as well as with round-based strategy extraction. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Friedrich Slivovsky 2024 Is Part Of LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2024.28 urn:nbn:de:0030-drops-205509 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.28 eng https://creativecommons.org/licenses/by/4.0/legalcode