ABSTRACT. We study the parametrisation of QBF resolution calculi by dependency schemes. One of the main problems in this area is to understand for which dependency schemes the resulting calculi are sound. Towards this end we propose a semantic framework for variable independence based on `exhibition' by QBF models, and use it to express a property of dependency schemes called `full exhibition' that is known to be sufficient for soundness in Q-resolution. Introducing a generalised form of the long-distance resolution rule, we propose a complete parametrisation of classical long-distance Q-resolution, and show that full exhbition remains sufficient for soundness. We demonstrate that our approach applies to the current research frontiers by proving that the reflexive resolution path dependency scheme is fully exhibited.

ABSTRACT. Solving Quantified Boolean Formulas (QBFs) is a challenging problem due to its high complexity. Many successful methods have been proposed, including extensions of DPLL/CDCL procedures and expansion-based approaches. In this paper, we present a novel method that is inspired by concepts from the field of parameterized complexity. More specifically, we develop a dynamic programming algorithm that traverses a tree decomposition of the QBF instance. We implemented our method using Binary Decision Diagrams as key ingredient to compactly represent the partial solutions computed during dynamic programming. Experiments indicate that our prototype shows promising results for instances with few quantifier alternations and where the treewidth of the propositional formula does not exceed 50. In fact, treewidth can be understood as a measurement of structure within the formula, and to the best of our knowledge has not been used explicitly in QBF solvers yet. 
 

ABSTRACT. Harary’s generalized Tic-Tac-Toe is an achievement game for polyominoes, where two players alternately put a stone on a grid board, and the player who first achieves a given polyomino wins the game. It is known whether the first player has a winning strategy in the generalized Tic-Tac-Toe for almost all polyominoes except the one called Snaky. GTTT(p,q) is an extension of the generalized Tic-Tac-Toe, where the first player places q stones in the first move and then the players place　q stones in each turn. In this paper, in order to attack GTTT(p,q) by　QBF solvers, we propose a QBF encoding for GTTT(p,q). Our encoding　is based on Gent and Rowley’s encoding for Connect-4. We modify three　parts of the encoding: initial condition, move rule and winning condition　of the game. The experimental results show that some QBF solvers can　be used to solve GTTT(p,q) on 4 × 4 or smaller boards.

ABSTRACT. We consider the problem of computing Skolem functions for satisfied dependency quantified Boolean formulas (DQBFs). We show how Skolem functions can be obtained from an elimination-based DQBF solver and how to take preprocessing steps into account. The size of the Skolem functions is optimized by don't-care minimization using Craig interpolants and rewriting techniques. Experiments with our DQBF solver HQS show that we are able to effectively compute Skolem functions with very little overhead compared to the mere solution of the formula.

ABSTRACT. The talk adresses three classes of open problems for quantified Boolean formulas (QBFs). The first class of problems is related to questions of minimal falsity under the restriction of fixed deficiency. The second class deals with the satisfiability problem for quantified Horn formulas and related problems. Concluding, we will discuss the expressive power of QBFs and the size of mimimal equivalence models for some subclasses.