# Variable Dependencies of QBFs (Research Project)

Funding Organisation: The Austrian Science Fund, FWF

Project Number: FWF P 27721

## Project Team

Friedrich Slivovsky (Postdoc)

Tomas Peitl (Doctoral Student)

Stefan Szeider (Professor, Principal Investigator)

## Topic

The satisfiability problem of Quantified Boolean Formulas (QBF) offers succinct encodings for hard problems arising in areas such as formal verification and planning. This research project explores new ways to leverage independence of variables for QBF. The nesting of existential and universal quantifiers in Quantified Boolean Formulas can generate variable dependencies that are a serious obstacle to lifting successful techniques from propositional satisfiability to QBF. In some cases one can identify a variable dependency as spurious and conclude that the corresponding variables are in fact independent. This information can be used to significantly improve the performance of decision procedures, but deciding whether variables are independent is a highly intractable problem in itself.

The aim of this project is three-fold: (A) to advance the state of the art in detecting variable independence by developing new theory and improved algorithms for currently used methods; (B) to find new approaches to detecting and harnessing variable independence; (C) to extend the scope of successful techniques from QBF to more general problems.

## Software

Research under Theme (B) has lead to the development of **Qute** (GitHub), a dependency learning QBF solver. Qute placed **3rd** in the PCNF track and **4th** in the Prenex non-CNF track of QBFEVAL'17.