Abstract We introduce the global conflict graph of DQCNFs (dependency quantified conjunctive normal forms), recording clashes between clauses on such universal variables on which all existential variables depend (called “global variables”). The biclique covers of this graph correspond to the eligible clause-slices of the DQCNF which consider only the global variables. We show that all such slices yield satisfiability-equivalent variations. This opens the possibility to realise this slice using as few global variables as possible. We give basic theoretical results and first supporting experimental data.

Autarkies for SAT are partial assignments for boolean CNF, which either satisfy a clause or leave it untouched. We introduce the natural generalisation of autarkies for DQCNF (dependency-quantified boolean CNF), by generalising constant boolean functions 0, 1, as used in SAT, to arbitrary boolean functions assigned to existential variables, as allowed by the dependency-specification. We regard here DQCNF as a proper generalisation of QCNF (QBF with CNF), and all results naturally apply also to QCNF. We provide the most basic theory, considering confluence of autarky reduction (removing the clauses satisfied by some autarky), and the Autarky Decomposition Theorem, the unique decomposition of a DQCNF into the lean kernel (free from any autarky) and the clauses satisfiable by some autarky. Finding autarkies is NEXPTIME-hard (or PSPACE-hard, when restricting to QCNF), and so autarky systems are introduced, which allow for more feasible restricted notions of autarkies, while maintaining the basic properties. The two most basic autarky systems restrict either the number of existential variables assigned, or the number of universal variables used in the boolean functions assigned.

The decision problem of quantified Boolean formulas (QBFs) is the archetypical problem for the complexity class PSPACE. Beside such theoretical aspects QBF also provides an attractive framework for encoding and solving various application problems ranging from symbolic reasoning in artificial intelligence to the formal verification and synthesis of computing systems. In this paper, we survey the different application areas that exploit QBF technology for solving their specific problems.