Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR16-043 | 23rd February 2016 18:11

On Q-Resolution and CDCL QBF Solving

RSS-Feed




TR16-043
Authors: Mikolas Janota
Publication: 21st March 2016 13:41
Downloads: 1152
Keywords: 


Abstract:

Q-resolution and its variations provide the underlying proof
systems for the DPLL-based QBF solvers. While (long-distance) Q-resolution
models a conflict driven clause learning (CDCL) QBF solver, it is not
known whether the inverse is also true. This paper provides a negative
answer to this question. This contrasts with SAT solving, where CDCL
solvers have been shown to simulate resolution.



ISSN 1433-8092 | Imprint