Martina Seidl

TACAS Conference 2026 Conference Paper

QSOLE: Automatic QBF Equivalence Checking

• Peter Pfeiffer
• Mark Peyrer
• Daniel Große
• Martina Seidl

SAT Conference 2025 Conference Paper

QRP+Gen: A Framework for Checking Q-Resolution Proofs with Generalized Axioms

• Mark Peyrer
• Martina Seidl

Q-resolution is a proof system for quantified Boolean formulas (QBFs) that forms the foundation for search-based QBF solvers with clause and cube learning. To derive stronger clauses and cubes, Q-resolution was extended with so-called generalized axioms. The derivation of such generalized axioms relies on solving oracles that could be, for example, SAT solvers or even QBF solvers. While the correctness of results obtained with classical QCDCL-based solving can be efficiently certified by an independent checker, until now, proof generation had to be turned off to benefit from generalized axioms. Consequently, the results obtained with reasoning under generalized axioms could not be certified independently. To overcome this restriction, we present QRP+Gen, a novel framework to automatically generate and check Q-resolution proofs that contain generalized axioms. To this end, we extended the Q-resolution format QRP such that all necessary information is included to verify the correctness of generalized axioms. Our extension allows to integrate certificates produced by any oracle which can produce automatically checkable proofs. Furthermore, we developed a proof checker that orchestrates the proof checking of the core Q-resolution proof and the proofs produced by the oracles. As a case study, we equipped the search-based QBF solver DepQBF with proof-producing oracles for the SAT-based techniques trivial truth and trivial falsity.

IJCAI Conference 2024 Conference Paper

A Top-Down Tree Model Counter for Quantified Boolean Formulas

• Florent Capelli
• Jean-Marie Lagniez
• Andreas Plank
• Martina Seidl

This paper addresses the challenge of solution counting for Quantified Boolean Formulas (QBFs), a task distinct from the well-established model counting problem for SAT (\#SAT). Unlike SAT, where models are straightforward assignments to Boolean variables, QBF solution counting involves tree models that capture dependencies among variables within different quantifier blocks. We present a comprehensive top-down tree model counter capable of handling diverse satisfiable QBF formulas. Emphasizing the critical role of the branching heuristic, which must consider variables in the correct order according to quantification blocks, we further demonstrate the importance of addressing connected components, free variables, and caching. Experimental results indicate that our proposed approach for counting tree models of QBF formulas is highly efficient in practice, surpassing existing state-of-the-art methods designed for this specific purpose.

SAT Conference 2024 Conference Paper

Models and Counter-Models of Quantified Boolean Formulas (Invited Talk)

• Martina Seidl

Because of the duality of universal and existential quantification, quantified Boolean formulas (QBF), the extension of propositional logic with quantifiers over the Boolean variables, have not only solutions in terms of models for true formulas like in SAT. Also false QBFs have solutions in terms of counter-models. Both models and counter-models can be represented as certain binary trees or as sets of Boolean functions reflecting the dependencies among the variables of a formula. Such solutions encode the answers to application problems for which QBF solvers are employed like the plan for a planning problem or the error trace of a verification problem. Therefore, models and counter-models are at the core of theory and practice of QBF solving. In this invited talk, we survey approaches that deal with models and counter-models of QBFs and identify some open challenges.

SAT Conference 2023 Conference Paper

QMusExt: A Minimal (Un)satisfiable Core Extractor for Quantified Boolean Formulas

• Andreas Plank
• Martina Seidl

In this paper, we present QMusExt, a tool for the extraction of minimal unsatisfiable sets (MUS) from quantified Boolean formulas (QBFs) in prenex conjunctive normal form (PCNF). Our tool generalizes an efficient algorithm for MUS extraction from propositional formulas that analyses and rewrites resolution proofs generated by SAT solvers. In addition to extracting unsatisfiable cores from false formulas in PCNF, we apply QMusExt also to obtain satisfiable cores from Q-resolution proofs of true formulas in prenex disjunctive normal form (PDNF).

SAT Conference 2023 Conference Paper

Validation of QBF Encodings with Winning Strategies

• Irfansha Shaik
• Maximilian Heisinger
• Martina Seidl
• Jaco van de Pol

When using a QBF solver for solving application problems encoded to quantified Boolean formulas (QBFs), mainly two things can potentially go wrong: (1) the solver could be buggy and return a wrong result or (2) the encoding could be incorrect. To ensure the correctness of solvers, sophisticated fuzzing and testing techniques have been presented. To ultimately trust a solving result, solvers have to provide a proof certificate that can be independently checked. Much less attention, however, has been paid to the question how to ensure the correctness of encodings. The validation of QBF encodings is particularly challenging because of the variable dependencies introduced by the quantifiers. In contrast to SAT, the solution of a true QBF is not simply a variable assignment, but a winning strategy. For each existential variable x, a winning strategy provides a function that defines how to set x based on the values of the universal variables that precede x in the quantifier prefix. Winning strategies for false formulas are defined dually. In this paper, we provide a tool for validating encodings using winning strategies and interactive game play with a QBF solver. As the representation of winning strategies can get huge, we also introduce validation based on partial winning strategies. Finally, we employ winning strategies for testing if two different encodings of one problem have the same solutions.

SAT Conference 2021 Conference Paper

QBFFam: A Tool for Generating QBF Families from Proof Complexity

• Olaf Beyersdorff
• Luca Pulina
• Martina Seidl
• Ankit Shukla 0003

Abstract We present QBFFam, a tool for the generation of formula families originating from the field of proof complexity. Such formula families are used to investigate the strength of proof systems and to show how they relate to each other in terms of simulations and separations. Furthermore, these proof systems underlie the reasoning power of QBF solvers. With our tool, it is possible to generate informative and scalable benchmarks that help to analyse the behavior of solvers. As we will see in this paper, runtime behavior predicted by proof complexity is indeed reflected by recent solver implementations.

SAT Conference 2019 Conference Paper

Local Search for Fast Matrix Multiplication

• Marijn J. H. Heule
• Manuel Kauers
• Martina Seidl

Abstract Laderman discovered a scheme for computing the product of two \(3\times 3\) matrices using only 23 multiplications in 1976. Since then, some more such schemes were proposed, but nobody knows how many such schemes there are and whether there exist schemes with fewer than 23 multiplications. In this paper we present two independent SAT-based methods for finding new schemes using 23 multiplications. Both methods allow computing a few hundred new schemes individually, and many thousands when combined. Local search SAT solvers outperform CDCL solvers consistently in this application.

SAT Conference 2019 Conference Paper

QRAT Polynomially Simulates ∀ \text -Exp+Res

• Benjamin Kiesl
• Martina Seidl

Abstract The proof system \(\forall \text {-Exp+Res}\) formally captures expansion-based solving of quantified Boolean formulas (QBFs) whereas the \(\mathsf {QRAT}\) proof system captures QBF preprocessing. From previous work it is known that certain families of formulas have short proofs in \(\mathsf {QRAT}\) but not in \(\forall \text {-Exp+Res}\). However, it was not known if the two proof systems were incomparable (i. e. , if there also existed QBFs with short \(\forall \text {-Exp+Res}\) proofs but without short \(\mathsf {QRAT}\) proofs), or if \(\mathsf {QRAT}\) polynomially simulates \(\forall \text {-Exp+Res}\). We close this gap of the QBF-proof-complexity landscape by presenting a polynomial simulation of \(\forall \text {-Exp+Res}\) in \(\mathsf {QRAT}\). Our simulation shows how definition introduction combined with extended-universal reduction can mimic the concept of universal expansion.

AIJ Journal 2019 Journal Article

The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)

• Luca Pulina
• Martina Seidl

After a break of about five years, in 2016 the classical QBFEVAL has been revived. QBFEVAL is a competitive evaluation of solvers for quantified Boolean formulas (QBF), the extension of propositional formulas with existential and universal quantifiers over the propositional variables. Due to the enormous interest in QBFEVAL'16, more recently, QBFEVAL'17 was organized. Both competitions were affiliated to the respective editions of the International Conference on Theory and Applications of Satisfiability Testing (SAT'16 and SAT'17), the major conference in research on SAT and related areas. In this paper we report about the 2016 and 2017 competitive evaluations of QBF solvers (QBFEVAL'16 and QBFEVAL'17), the two most recent events in a series of competitions established with the aim of assessing the advancements in reasoning about QBFs. This report gives an overview of the setup of these two events, on their participants and on the results of the experiments that were performed for evaluating the participating systems.

SAT Conference 2018 Conference Paper

Symmetries of Quantified Boolean Formulas

• Manuel Kauers
• Martina Seidl

Abstract While symmetries are well understood for Boolean formulas and successfully exploited in practical SAT solving, less is known about symmetries in quantified Boolean formulas (QBF). There are some works introducing adaptions of propositional symmetry breaking techniques, with a theory covering only very specific parts of QBF symmetries. We present a general framework that gives a concise characterization of symmetries of QBF. Our framework naturally incorporates the duality of universal and existential symmetries resulting in a general basis for QBF symmetry breaking.

SAT Conference 2017 Conference Paper

A Little Blocked Literal Goes a Long Way

• Benjamin Kiesl
• Marijn J. H. Heule
• Martina Seidl

Abstract Q-resolution is a generalization of propositional resolution that provides the theoretical foundation for search-based solvers of quantified Boolean formulas (QBFs). Recently, it has been shown that an extension of Q-resolution, called long-distance resolution, is remarkably powerful both in theory and in practice. However, it was unknown how long-distance resolution is related to \(\mathsf {QRAT}\), a proof system introduced for certifying the correctness of QBF-preprocessing techniques. We show that \(\mathsf {QRAT}\) polynomially simulates long-distance resolution. Two simple rules of \(\mathsf {QRAT}\) are crucial for our simulation— blocked-literal addition and blocked-literal elimination. Based on the simulation, we implemented a tool that transforms long-distance-resolution proofs into \(\mathsf {QRAT}\) proofs. In a case study, we compare long-distance-resolution proofs of the well-known Kleine Büning formulas with corresponding \(\mathsf {QRAT}\) proofs.

LPAR Conference 2017 Conference Paper

Blocked Clauses in First-Order Logic

• Benjamin Kiesl
• Martin Suda 0001
• Martina Seidl
• Hans Tompits
• Armin Biere

Blocked clauses provide the basis for powerful reasoning techniques used in SAT, QBF, and DQBF solving. Their definition, which relies on a simple syntactic criterion, guarantees that they are both redundant and easy to find. In this paper, we lift the notion of blocked clauses to first-order logic. We introduce two types of blocked clauses, one for first-order logic with equality and the other for first-order logic without equality, and prove their redundancy. In addition, we give a polynomial algorithm for checking whether a clause is blocked. Based on our new notions of blocking, we implemented a novel first-order preprocessing tool. Our experiments showed that many first-order problems in the TPTP library contain a large number of blocked clauses whose elimination can improve the performance of modern theorem provers, especially on satisfiable problem instances.

IJCAI Conference 2017 Conference Paper

Blockedness in Propositional Logic: Are You Satisfied With Your Neighborhood?

• Benjamin Kiesl
• Martina Seidl
• Hans Tompits
• Armin Biere

Clause-elimination techniques that simplify formulas by removing redundant clauses play an important role in modern SAT solving. Among the types of redundant clauses, blocked clauses are particularly popular. For checking whether a clause C is blocked in a formula F, one only needs to consider the so-called resolution neighborhood of C, i. e. , the set of clauses that can be resolved with C. Because of this, blocked clauses are referred to as being locally redundant. In this paper, we discuss powerful generalizations of blocked clauses that are still locally redundant, viz. set-blocked clauses and super-blocked clauses. We furthermore present complexity results for deciding whether a clause is set-blocked or super-blocked.

SAT Conference 2016 Conference Paper

Q-Resolution with Generalized Axioms

• Florian Lonsing
• Uwe Egly
• Martina Seidl

Abstract Q-resolution is a proof system for quantified Boolean formulas (QBFs) in prenex conjunctive normal form (PCNF) which underlies search-based QBF solvers with clause and cube learning (QCDCL). With the aim to derive and learn stronger clauses and cubes earlier in the search, we generalize the axioms of the Q-resolution calculus resulting in an exponentially more powerful proof system. The generalized axioms introduce an interface of Q-resolution to any other QBF proof system allowing for the direct combination of orthogonal solving techniques. We implemented a variant of the Q-resolution calculus with generalized axioms in the QBF solver DepQBF. As two case studies, we apply integrated SAT solving and resource-bounded QBF preprocessing during the search to heuristically detect potential axiom applications. Experiments with application benchmarks indicate a substantial performance improvement.

AIJ Journal 2016 Journal Article

The QBF Gallery: Behind the scenes

• Florian Lonsing
• Martina Seidl
• Allen Van Gelder

Over the last few years, much progress has been made in the theory and practice of solving quantified Boolean formulas (QBF). Novel solvers have been presented that either successfully enhance established techniques or implement novel solving paradigms. Powerful preprocessors have been realized that tune the encoding of a formula to make it easier to solve. Frameworks for certification and solution extraction emerged that allow for a detailed interpretation of a QBF solver's results, and new types of QBF encodings were presented for various application problems. To capture these developments the QBF Gallery was established in 2013. The QBF Gallery aims at providing a forum to assess QBF tools and to collect new, expressive benchmarks that allow for documenting the status quo and that indicate promising research directions. These benchmarks became the basis for the experiments conducted in the context of the QBF Gallery 2013 and follow-up evaluations. In this paper, we report on the setup of the QBF Gallery. To this end, we conducted numerous experiments which allowed us not only to assess the quality of the tools, but also the quality of the benchmarks.

JAIR Journal 2015 Journal Article

Clause Elimination for SAT and QSAT

• Marijn Heule
• Matti Järvisalo
• Florian Lonsing
• Martina Seidl
• Armin Biere

The famous archetypical NP-complete problem of Boolean satisfiability (SAT) and its PSPACE-complete generalization of quantified Boolean satisfiability (QSAT) have become central declarative programming paradigms through which real-world instances of various computationally hard problems can be efficiently solved. This success has been achieved through several breakthroughs in practical implementations of decision procedures for SAT and QSAT, that is, in SAT and QSAT solvers. Here, simplification techniques for conjunctive normal form (CNF) for SAT and for prenex conjunctive normal form (PCNF) for QSAT---the standard input formats of SAT and QSAT solvers---have recently proven very effective in increasing solver efficiency when applied before (i.e., in preprocessing) or during (i.e., in inprocessing) satisfiability search. In this article, we develop and analyze clause elimination procedures for pre- and inprocessing. Clause elimination procedures form a family of (P)CNF formula simplification techniques which remove clauses that have specific (in practice polynomial-time) redundancy properties while maintaining the satisfiability status of the formulas. Extending known procedures such as tautology, subsumption, and blocked clause elimination, we introduce novel elimination procedures based on asymmetric variants of these techniques, and also develop a novel family of so-called covered clause elimination procedures, as well as natural liftings of the CNF-level procedures to PCNF. We analyze the considered clause elimination procedures from various perspectives. Furthermore, for the variants not preserving logical equivalence under clause elimination, we show how to reconstruct solutions to original CNFs from satisfying assignments to simplified CNFs, which is important for practical applications for the procedures. Complementing the more theoretical analysis, we present results on an empirical evaluation on the practical importance of the clause elimination procedures in terms of the effect on solver runtimes on standard real-world application benchmarks. It turns out that the importance of applying the clause elimination procedures developed in this work is empirically emphasized in the context of state-of-the-art QSAT solving.

LPAR Conference 2015 Conference Paper

Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination

• Florian Lonsing
• Fahiem Bacchus
• Armin Biere
• Uwe Egly
• Martina Seidl

Abstract Among preprocessing techniques for quantified Boolean formula (QBF) solving, quantified blocked clause elimination (QBCE) has been found to be extremely effective. We investigate the power of dynamically applying QBCE in search-based QBF solving with clause and cube learning (QCDCL). This dynamic application of QBCE is in sharp contrast to its typical use as a mere preprocessing technique. In our dynamic approach, QBCE is applied eagerly to the formula interpreted under the assignments that have been enumerated in QCDCL. The tight integration of QBCE in QCDCL results in a variant of cube learning which is exponentially stronger than the traditional method. We implemented our approach in the QBF solver DepQBF and ran experiments on instances from the QBF Gallery 2014. On application benchmarks, QCDCL with dynamic QBCE substantially outperforms traditional QCDCL. Moreover, our approach is compatible with incremental solving and can be combined with preprocessing techniques other than QBCE.

SAT Conference 2014 Conference Paper

MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing

• Charles Jordan
• Lukasz Kaiser
• Florian Lonsing
• Martina Seidl

Abstract Inspired by recent work on parallel SAT solving, we present a lightweight approach for solving quantified Boolean formulas (QBFs) in parallel. In particular, our approach uses a sequential state-of-the-art QBF solver to evaluate subformulas in working processes. It abstains from globally exchanging information between the workers, but keeps learnt information only locally. To this end, we equipped the state-of-the-art QBF solver DepQBF with assumption-based reasoning and integrated it in our novel solver MPIDepQBF as backend solver. Extensive experiments on standard computers as well as on the supercomputer Tsubame show the impact of our approach.

SAT Conference 2012 Conference Paper

Resolution-Based Certificate Extraction for QBF - (Tool Presentation)

• Aina Niemetz
• Mathias Preiner
• Florian Lonsing
• Martina Seidl
• Armin Biere

Abstract A certificate of (un)satisfiability for a quantified Boolean formula (QBF) represents sets of assignments to the variables, which act as witnesses for its truth value. Certificates are highly requested for practical applications of QBF like formal verification and model checking. We present an integrated set of tools realizing resolution-based certificate extraction for QBF in prenex conjunctive normal form. Starting from resolution proofs produced by the solver DepQBF, we describe the workflow consisting of proof checking, certificate extraction, and certificate checking. We implemented the steps of that workflow in stand-alone tools and carried out comprehensive experiments. Our results demonstrate the practical applicability of resolution-based certificate extraction.

ECAI Conference 2006 Conference Paper

A Solver for QBFs in Nonprenex Form

• Uwe Egly
• Martina Seidl
• Stefan Woltran

Various problems in artificial intelligence (AI) can be solved by translating them into a quantified boolean formula (QBF) and evaluating the resulting encoding. In this approach, a QBF solver is used as a black box in a rapid implementation of a more general reasoning system. Most of the current solvers for QBFs require formulas in prenex conjunctive normal form as input, which makes a further translation necessary, since the encodings are usually not in a specific normal form. This additional step increases the number of variables in the formula or disrupts the formula's structure. Moreover, the most important part of this transformation, prenexing, is not deterministic. In this paper, we focus on an alternative way to process QBFs without these drawbacks and describe a solver, qpro, which is able to handle arbitrary formulas. To this end, we extend algorithms for QBFs to the non-normal form case and compare qpro with the leading normal-form provers on problems from the area of AI.

JELIA Conference 2006 Conference Paper

ccT: A Correspondence-Checking Tool for Logic Programs Under the Answer-Set Semantics

• Johannes Oetsch
• Martina Seidl
• Hans Tompits
• Stefan Woltran

Abstract In recent work, a general framework for specifying correspondences between logic programs under the answer-set semantics has been defined. The framework captures different notions of equivalence, including well-known ones like ordinary, strong, and uniform equivalence, as well as refined ones based on the projection of answer sets where not all parts of an answer set are of relevance. In this paper, we describe an implementation to verify program correspondences in this general framework. The system, called cc⊤, relies on linear-time constructible reductions to quantified propositional logic and uses extant solvers for the latter language as back-end inference engines.

SAT Conference 2003 Conference Paper

Comparing Different Prenexing Strategies for Quantified Boolean Formulas

• Uwe Egly
• Martina Seidl
• Hans Tompits
• Stefan Woltran
• Michael Zolda

Abstract The majority of the currently available solvers for quantified Boolean formulas (QBFs) process input formulas only in prenex conjunctive normal form. However, the natural representation of practicably relevant problems in terms of QBFs usually results in formulas which are not in a specific normal form. Hence, in order to evaluate such QBFs with available solvers, suitable normal-form translations are required. In this paper, we report experimental results comparing different prenexing strategies on a class of structured benchmark problems. The problems under consideration encode the evaluation of nested counterfactuals over a propositional knowledge base, and span the entire polynomial hierarchy. The results show that different prenexing strategies influence the evaluation time in different ways across different solvers. In particular, some solvers are robust to the chosen strategies while others are not.