Over the last years many solvers for quantified Boolean formulas (QBFs) have been developed. While most of these solvers support QDIMACS as a standard input format, exchanging a QBF solver within a reasoning framework is often a challenging task. Many solvers do not provide an API but they can only be used via their executable. Further, incremental solving is only supported to a limited extent. We present PyQBF , a Python-based framework that provides a uniform programmatic interface to state-of-the-art QBF solvers. In this article, we introduce the general architecture of PyQBF , describe the supported features and give a detailed example that illustrates how our framework can be used to implement an enumerative QBF solution counter as well as to solve a bounded model checking problem using a non-CNF representation. Our extensive experimental evaluation shows the efficiency of PyQBF . The experiments indicate that there is only little overhead compared with direct usage of the solvers.

Feature models evolve in multiple iterations over time. When modellers change a model, they enact syntactical changes in order to produce specific semantic differences between model iterations. Many tools have been developed to analyze such syntactical differences, but the changing semantics of models were harder to assess. Tools for semantic differences between feature model iterations rely on Binary Decision Diagrams (BDDs) or encode each change into SAT, the former leading to BDD scaling issues and the latter requiring editor support or other specialized tooling. We contribute the first concise formalization of feature models and their semantic differences into propositional logic and use it to efficiently and scalably classify semantic differences using SAT solvers. We then extend our definition into QSAT in order to quantify the full list of semantic differences between feature models and enumerate them using QBF tools, without needing specialized feature model solvers. We implement a semantic difference classifier using our UVL processing pipeline based on Booleguru (instead of the more widely used FeatureIDE) and evaluate it on industrial feature model instances in the standardized UVL format. We also evaluate our QSAT-based semantic difference enumerator and reproduce prior results. We provide all software and evaluation results in an artifact.

Abstract We present Simsala, an easy-to-install and easy-to-use collection of scripts supporting benchmarking on clusters of compute nodes. While designed with applications for benchmarking solving technologies like SAT and extensions, our solution can be easily transferred to many other application scenarios as well. In this work, we discuss the design objectives behind Simsala, provide some implementation details, and illustrate with case studies how Simsala has been applied in the past for extensive evaluations.

Abstract Modern solvers for quantified Boolean formulas (QBFs) process formulas in prenex form, which divides each QBF into two parts: the quantifier prefix and the propositional matrix. While this representation does not cover the full language of QBF, every non-prenex formula can be transformed to an equivalent formula in prenex form. This transformation offers several degrees of freedom and blurs structural information that might be useful for the solvers. In a case study conducted 20 years back, it has been shown that the applied transformation strategy heavily impacts solving time. We revisit this work and investigate how sensitive recent QBF solvers perform w.r.t. various prenexing strategies.

Abstract Recent approaches on verification and reasoning solve SAT and QBF encodings using state-of-the-art SMT solvers, as it “makes implementation much easier”. The ease-of-use of these solvers make SAT and QBF solvers less visible to users of solvers—who are maybe from different research communities—potentially not exploiting the power of state-of-the-art tools. In this work, we motivate the need to build bridges over the widening solver-gap and introduce Booleguru, a tool to convert between formats for logic formulas. It makes SAT and QBF solvers more accessible by using techniques known from SMT solvers, such as advanced Python interfaces like Z3Py and easily generatable languages like SMT-LIB, integrating them to our conversion tool. We then introduce a language to manipulate and combine multiple formulas, optionally applying transformations for quickly prototyping encodings. Booleguru’s advanced scripting capabilities form a programming environment specialized for Boolean logic, offering a more efficient way to develop novel problem encodings.

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.

Abstract Over the last years, innovative parallel and distributed SAT solving techniques were presented that could impressively exploit the power of modern hardware and cloud systems. Two approaches were particularly successful: (1) search-space splitting in a Divide-and-Conquer (D &C) manner and (2) portfolio-based solving. The latter executes different solvers or configurations of solvers in parallel. For quantified Boolean formulas (QBFs), the extension of propositional logic with quantifiers, there is surprisingly little recent work in this direction compared to SAT. In this paper, we present ParaQooba , a novel framework for parallel and distributed QBF solving which combines D &C parallelization and distribution with portfolio-based solving. Our framework is designed in such a way that it can be easily extended and arbitrary sequential QBF solvers can be integrated out of the box, without any programming effort. We show how ParaQooba orchestrates the collaboration of different solvers for joint problem solving by performing an extensive evaluation on benchmarks from QBFEval’22, the most recent QBF competition.

Developing software systems is inherently subject to errors that can later cause failures in production. While testing can help to identify critical issues, it is limited to concrete inputs and states. Exhaustive testing is infeasible in practice; hence we can never prove the absence of faults. Symbolic execution, i.e., the process of symbolically reasoning about the program state during execution, can inspect the behavior of a system under all possible concrete inputs at run time. It automatically generates logical constraints that match the program semantics and uses theorem provers to verify the existence of error states within the application. This paper presents a novel symbolic execution engine called SymJEx, implemented on top of the multi-language Java Virtual Machine GraalVM. SymJEx uses the Graal compiler's intermediate representation to derive and evaluate path conditions, allowing GraalVM users to leverage the engine to improve software quality. In this work, we show how SymJEx finds non-trivial faults in existing software systems and compare our approach with established symbolic execution engines.