FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Symmetries for QBF

Authors: Manuel Kauers and Martina Seidl

Paper Information

Title:Symmetries for QBF
Authors:Manuel Kauers and Martina Seidl
Proceedings:SAT Proceedings
Editors: Christoph M. Wintersteiger and Olaf Beyersdorff
Keywords:Quantified Boolean Formulas, Symmetries, Symmetry Breaking
Abstract:

ABSTRACT. While symmetries are well understood for Boolean formulas and successfully exploited in practical SAT solving, little is known about symmetries in quantified Boolean formulas (QBF). There are some works introducing adoptions of propositional symmetry breaking techniques for QBF solving, with a theory covering only very specific parts of QBF symmetries. We present a general framework based on symmetric groups that give a concise characterization of symmetries in QBF. Our framework handles universal and existential symmetries in a dual manner and gives rise to a natural generalization of a known symmetry breaking technique from SAT.

Pages:18
Talk:Jul 10 14:30 (Session 55F: QBF I)
Paper: