Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Revision(s):

Revision #1 to TR14-036 | 21st April 2014 23:22

On Unification of QBF Resolution-Based Calculi

RSS-Feed




Revision #1
Authors: Olaf Beyersdorff, Leroy Chew, Mikolas Janota
Accepted on: 21st April 2014 23:22
Downloads: 1482
Keywords: 


Abstract:

Several calculi for quantified Boolean formulas (QBFs) exist, but
relations between them are not yet fully understood.
This paper defines a novel calculus, which is resolution-based and
enables unification of the principal existing resolution-based QBF
calculi, namely Q-resolution, long-distance Q-resolution and the expansion-based
calculus $\forall$Exp+Res. All these calculi play an important role in QBF solving.
This paper shows simulation results for the new calculus and some of its
variants. Further, we demonstrate how to obtain winning strategies for the universal
player from proofs in the calculus.
We believe that this new proof system opens new avenues for further
research and provides a suitable formalism for certification of existing solvers.



Changes to previous version:

Improved presentation of the calculi as well as increased flexibility thereof.


Paper:

TR14-036 | 8th March 2014 01:18

On Unification of QBF Resolution-Based Calculi





TR14-036
Authors: Mikolas Janota, Leroy Chew, Olaf Beyersdorff
Publication: 15th March 2014 02:16
Downloads: 2665
Keywords: 


Abstract:

Several calculi for quantified Boolean formulas (QBFs) exist, but
relations between them are not yet fully understood.
This paper defines a novel calculus, which is resolution-based and
enables unification of the principal existing resolution-based QBF
calculi, namely Q-resolution, long-distance Q-resolution and the expansion-based
calculus $\forall$Exp+Res. All these calculi play an important role in QBF solving.
This paper shows simulation results for the new calculus and some of its
variants. Further, we demonstrate how to obtain winning strategies for the universal
player from proofs in the calculus.
We believe that this new proof system opens new avenues for further
research and provides a suitable formalism for certification of existing solvers.



ISSN 1433-8092 | Imprint