Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style

Reports tagged with Q-Resolution:
TR13-097 | 25th June 2013
Mikolas Janota, Joao Marques-Silva

On Propositional QBF Expansions and Q-Resolution

Over the years, proof systems for propositional satisfiability (SAT)
have been extensively studied. Recently, proof systems for
quantified Boolean formulas (QBFs) have also been gaining attention.
Q-resolution is a calculus enabling producing proofs from
DPLL-based QBF solvers. While DPLL has become a dominating technique
for SAT, QBF has been tackled ... more >>>

TR14-036 | 8th March 2014
Mikolas Janota, Leroy Chew, Olaf Beyersdorff

On Unification of QBF Resolution-Based Calculi

Revisions: 1

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

TR14-120 | 16th September 2014
Olaf Beyersdorff, Leroy Chew, Mikolas Janota

Proof Complexity of Resolution-based QBF Calculi

Proof systems for quantified Boolean formulas (QBFs) provide a theoretical underpinning for the performance of important
QBF solvers. However, the proof complexity of these proof systems is currently not well understood and in particular
lower bound techniques are missing. In this paper we exhibit a new and elegant proof technique ... more >>>

TR14-131 | 7th October 2014
Olaf Beyersdorff, Leroy Chew, Karteek Sreenivasaiah

A game characterisation of tree-like Q-Resolution size

We provide a characterisation for the size of proofs in tree-like Q-Resolution by a Prover-Delayer game, which is inspired by a similar characterisation for the proof size in classical tree-like Resolution. This gives the first successful transfer of one of the lower bound techniques for classical proof systems to QBF ... more >>>

TR16-028 | 29th February 2016
Olaf Beyersdorff, Joshua Blinkhorn

Dependency Schemes in QBF Calculi:Semantics and Soundness

Revisions: 1

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

TR16-043 | 23rd February 2016
Mikolas Janota

On Q-Resolution and CDCL QBF Solving

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, ... more >>>

TR17-032 | 17th February 2017
Olaf Beyersdorff, Joshua Blinkhorn

Formulas with Large Weight: a New Technique for Genuine QBF Lower Bounds

We devise a new technique to prove lower bounds for the proof size in resolution-type calculi for quantified Boolean formulas (QBF). The new technique applies to the strong expansion system IR-calc and thereby also to the most studied QBF system Q-Resolution.

Our technique exploits a clear semantic paradigm, showing the ... more >>>

ISSN 1433-8092 | Imprint