FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Portfolio-Based Algorithm Selection for Circuit QBFs

Authors: Holger Hoos, Tomáš Peitl, Friedrich Slivovsky and Stefan Szeider

Paper Information

Title:Portfolio-Based Algorithm Selection for Circuit QBFs
Authors:Holger Hoos, Tomáš Peitl, Friedrich Slivovsky and Stefan Szeider
Proceedings:QBF Contributed Papers
Editor: Martina Seidl
Keywords:Algorithm selection, Portfolio, QBF, Quantified Circuit
Abstract:

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.

Pages:10
Talk:Jul 08 16:20 (Session 42P)
Paper: