View: session overviewtalk overviewside by side with other conferences

08:30-09:30 Session 1: Reception desk
Location: Labri Main Entrance
09:00-10:30 Session 2: Presentations I
Location: Room 3 First floor, building A29
Dependency Schemes in QBF Calculi: Semantics and Soundness
SPEAKER: unknown

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.

Dynamic Programming-based QBF Solving

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. 

QBF Encoding of Generalized Tic-Tac-Toe
SPEAKER: Diptarama

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.

10:30-11:00Coffee Break
11:00-12:30 Session 4B: Presentations II
Location: Room 3 First floor, building A29
On Conflicts and Strategies in QBF
Skolem Functions for DQBF

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.

First-Order Logic and Blocked Clauses
SPEAKER: Martin Suda
SPEAKER: Martina Seidl
12:30-14:00Lunch Break
14:00-15:00 Session 5B: Keynote
Location: Room 3 First floor, building A29
Open Problems for Quantified Boolean Formulas

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.

15:00-15:30Coffee Break
15:30-17:30 Session 6B: Competition


Location: Room 3 First floor, building A29
Short Presentations of Submissions to QBF Eval 2016
QBFEval 2016
SPEAKER: Luca Pulina
19:30-22:00 Session : Welcome reception
Location: Palais de la bourse