International Workshop on Quantified Boolean Formulas and Beyond

colocated with the
Int. Conf. on Theory and Applications of Satisfiability Testing

News

Important Dates

  • May 25: Submission
  • June 5: Notification
  • June 15: Camera-Ready Version
  • July 7: Workshop

Overview

Quantified Boolean formulas (QBF) are an extension of propositional logic which allows for explicit quantification over propositional variables. The decision problem of QBF is PSPACE-complete compared to NP-completeness of the decision problem of propositional logic (SAT).

Many problems from application domains such as model checking, formal verification or synthesis are PSPACE-complete, and hence could be encoded in QBF. Considerable progress has been made in QBF solving throughout the past years. However, in contrast to SAT, QBF is not widely applied to practical problems in industrial settings. For example, the extraction and validation of models of (un)satisfiability of QBFs and has turned out to be challenging.

The goal of the International Workshop on Quantified Boolean Formulas (QBF Workshop) is to bring together researchers working on theoretical and practical aspects of QBF solving. In addition to that, it addresses (potential) users of QBF in order to reflect on the state-of-the-art and to consolidate on immediate and long-term research challenges.

In particular, the following topics shall be considered at the workshop:

  1. Directions of Solver Development
  2. Certificates
  3. Applications
  4. Community platform and repository

      5. Invited Talks

        Alexander Feldman, PARC

        • Title: Toward Computer-Aided Digital Design
        • Abstract: Circuit design is in the heart of modern computing. Algorithms based on satisfiability have application in functional circuit design, layout, technology mapping, and various optimization techniques. Many problems in digital design, though, belong to higher classes in the computational hierarchy. Encoding those as satisfiability problems is often cumbersome. In this talk we will discuss a class of algorithms that solve problems from digital design by constructing and solving Quantified Boolean Formulas. These encodings are intuitive and can help the designer invent novel circuits. The algorithms we discuss are generic and have use both in design and optimization. The designs computed by our algorithms are compositions of function types specified in component libraries. Our algorithms reduce the design problem to quantified satisfiability and use advanced solvers to find solutions that represent useful systems. The algorithms we present in this talk are sound and complete and are guaranteed to discover correct designs of optimal size, if they exist. We apply our method to the design of digital circuits and discover new and more optimal classical and quantum circuits for common arithmetic functions such as addition and multiplication. The performance of our algorithms is evaluated through extensive experimentation. We have first created a benchmark consisting of specifications of scalable synthetic digital circuits and real-world mirochips. We have then generated multiple circuits functionally equivalent to the ones in the benchmark. Our approach generalizes circuit optimization. It uses arbitrary component libraries and has applications to areas such as digital circuit design, diagnostics, abductive reasoning, test vector generation, and combinatorial optimization.
        • Biographical information: Alexander Feldman is a researcher at PARC (former Xerox PARC). Before that he was a postdoc at University College Cork and a visiting researcher at Ecole Polytechnique Fédérale de Lausanne (EPFL) and Delft University of Technology. He has obtained his Ph.D. (cum laude) in computer science/artificial intelligence and M.Sc. (cum laude) in parallel and distributed systems from the Delft University of Technology. He has more than 50 publications in leading conference proceedings and international journals covering topics from artificial intelligence, model-based diagnosis, computer science, and engineering. In cooperation with NASA Ames Research Center and PARC, Alexander Feldman has co-organized the International Diagnostic Competitions (DXC). Alexander Feldman's interest cover wide spectrum, including topics such as model-based diagnosis, automated problem solving, software and hardware design, quantum computing, logic design, design of diagnostic space applications, digital signal processing, and localization.

        Stefan Mengel, CNRS, CRIL, Lens

        • Title:Width measures for QBF
        • Abstract: Width measures for CNF formulas have been studied extensively to describe tractable classes for SAT but also extensions like #SAT and MaxSAT. In this talk, I will survey results on how and to which extent this line of work can be extended to QBF.
        • Biographical information: Stefan Mengel is a permanent full-time researcher at CNRS currently working at the CRIL lab in Lens, France. Before, he did his PhD in Paderborn, Germany and spent two years as a postdoc at Ëcole Polytechnique, France. His research interest is mostly in artificial intelligence and database theory. Most of his recent work is on the use of techniques and data structures from knowledge compilation in these areas, in particular for QBF and enumeration algorithms.

      Contact

      qbf19@easychair.org

      Previous Editions and Related Events