FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
QBF ON SUNDAY, JULY 8TH

View: session overviewtalk overviewside by side with other conferences

09:00-10:30 Session 34L: Joint QBF / Proof Complexity session (joint with PC)
Location: Maths L5
09:00
Lower Bound Techniques for QBF Proof Systems
10:00
Towards the Semantics of QBF Clauses

ABSTRACT. Towards the Semantics of QBF Clauses

10:30-11:00Coffee Break
11:00-12:30 Session 38N: Joint QBF / Proof Complexity session (joint with PC)
Location: Maths L5
11:00
Size, Cost and Capacity: A Semantic Technique for Hard Random QBFs
11:30
Short Proofs in QBF Expansion
11:50
The Symmetry Rule for Quantified Boolean Formulas
SPEAKER: Martina Seidl
12:10
Discussion
12:30-14:00Lunch Break
14:00-15:30 Session 40P
Chair:
Location: Maths L5
14:00
Preprocessing for (D)QBF
SPEAKER: Ralf Wimmer
14:20
Initial study on the effect of different QBF solvers and preprocessors on link-information sensitive QBF encodings for Abstract Dialectical Frameworks
SPEAKER: Uwe Egly
14:40
Tractability results for structured quantified CNF-formulas via knowledge compilation

ABSTRACT. We show how knowledge compilation can be used as a tool for QBF. More precisely, we show that certain one can apply quantification on certain data structures used in knowledge compilation which in combination with the fact that restricted classes of CNF-formulas can be compiled into these data structures can be used to show fixed-parameter tractable results for QBF.

15:00
A Grounder From Second-Order Logic To QBF

ABSTRACT. Recent solver research has developed powerful QBF solvers. Alas, we know of few tools that provide a modelling language on a higher level, translating this to QBF. This is surprising, as in the closely related field of SAT solvers, research has gone hand in hand with the develop- ment of such systems. This extended abstract on work in progress reports on a system that allows the use of second-order logic as a high-level modelling language and that grounds (translates) models written in such a language to a QBF formula. We provide an example encoding, outline the grounding process and propose further research and experiments.

15:20
PrideMM: QBFEVAL Benchmarks (QBFEval18 Contribution)
SPEAKER: Radu Grigore
15:25
Chess Solving and Composing (QBFEval18 Contribution)
15:30-16:00Coffee Break
16:00-18:00 Session 42P
Location: Maths L5
16:00
Understanding and Extending Incremental Determinization for 2QBF
SPEAKER: Markus Rabe
16:20
Portfolio-Based Algorithm Selection for Circuit QBFs
SPEAKER: Tomáš Peitl

ABSTRACT. Quantified Boolean Formulas (QBFs) are a generalization of propositional formulae that admits succinct encodings of verification and synthesis problems. Given that modern QBF solvers are based on different architectures with complementary performance characteristics, a portfolio-based approach to QBF solving is particularly promising.

We define a natural set of features of circuit QBFs and show that they can be used to construct portfolio-based algorithm selectors of state-of-the-art circuit QBF solvers that are close to the virtual best solver. We further demonstrate that most of this performance can be achieved using surprisingly small subsets of cheaply computable and intuitive features.

16:40
DepQBF (QBFEval'18 Contribution)
16:45
RAReQS, QFUN, QESTO (QBFEval'18 Contribution)
16:50
Qute (QBFEval'18 Contribution)
16:55
QBFEval 2018
17:20
Discussion
SPEAKER: Hubie Chen