Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving

DOI10.1007/978-3-642-45221-5_21zbMath1406.68106OpenAlexW54881092MaRDI QIDQ2870136

Florian Lonsing, Uwe Egly, Magdalena Widl

Publication date: 17 January 2014

Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-45221-5_21

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items (24)

Backdoors to Normality for Disjunctive Logic Programs ⋮ Quantified maximum satisfiability ⋮ The QBF Gallery: behind the scenes ⋮ Unnamed Item ⋮ Relating size and width in variants of Q-resolution ⋮ A simple proof of QBF hardness ⋮ Long-distance Q-resolution with dependency schemes ⋮ A game characterisation of tree-like Q-resolution size ⋮ Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution ⋮ Towards Uniform Certification in QBF ⋮ Lower bound techniques for QBF expansion ⋮ Lower bounds for QCDCL via formula gauge ⋮ Classes of hard formulas for QBF resolution ⋮ Unnamed Item ⋮ Understanding cutting planes for QBFs ⋮ Building strategies into QBF proofs ⋮ A Game Characterisation of Tree-like Q-resolution Size ⋮ Long Distance Q-Resolution with Dependency Schemes ⋮ Unnamed Item ⋮ Unnamed Item ⋮ CAQE and QuAbS: Abstraction Based QBF Solvers ⋮ QBFFam: a tool for generating QBF families from proof complexity ⋮ Lower bounds for QCDCL via formula gauge ⋮ Proof complexity of symbolic QBF reasoning

This page was built for publication: Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving