DQBF is a CNF formula in succinct representation

31^st January 2023, 13:00 Ashton Lecture Theatre
Dr. Tony Tan
Department of Computer Science and Information Engineering, National Taiwan University

Abstract

The satisfiability of Dependency Quantified Boolean Formulas (DQBFs) recently has attracted a lot of attention in SAT community. Intuitively DQBF is the extension of QBF where for each existentially quantified variable,
one can specify its set of dependent variables.

In this talk we will show that a DQBF is simply a CNF formula in an exponentially more succinct representation.
For a positive integer k, a k-DQBF is a DQBF with k existentially quantified variables.
We show the following.
1) k-DQBF is a succinct representation of a k-CNF formula.
2) The satisfiability of 2-DQBFs and 3-DQBFs is PSPACE-complete and NEXP-complete, resp.
3) A parsimonious polynomial time reduction from DQBFs to 3-DQBFs.
4) Natural explicit reductions from well known NEXP-complete problems to the satisfiability of DQBF.

Results (2)--(4) parallel the following well known classical results for SAT.
*) The satisfiability of 2-CNF and 3-CNF formulas is NLOG-complete and NP-complete, resp.
*) A parsimonious polynomial time reduction from arbitrary boolean formulas to 3-CNF formulas.
*) Natural reductions (in the form of Cook-Levin reductions) from NP-complete problems to SAT.

Biography

To be updated