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 TR16-028 | 28th April 2016 13:21

Dependency Schemes in QBF Calculi: Semantics and Soundness

RSS-Feed




Revision #1
Authors: Olaf Beyersdorff, Joshua Blinkhorn
Accepted on: 28th April 2016 13:21
Downloads: 249
Keywords: 


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 exhibition 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.



Changes to previous version:

We include a proof that the reflexive resolution path dependency scheme is fully exhibited; the previous version contained the weaker result that the standard dependency scheme is fully exhibited.


Paper:

TR16-028 | 29th February 2016 20:02

Dependency Schemes in QBF Calculi:Semantics and Soundness





TR16-028
Authors: Olaf Beyersdorff, Joshua Blinkhorn
Publication: 5th March 2016 16:20
Downloads: 404
Keywords: 


Abstract:

We study the parametrization 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 define a property of dependency schemes called `full exhibition'. We prove that all CDCL-based resolution calculi, including Q-resolution, universal and long-distance Q-resolution, are sound when parametrized by a fully exhibited dependency scheme. To illustrate proof of concept, we show that the standard dependency scheme is fully exhibited.



ISSN 1433-8092 | Imprint