Q-Resolution with Generalized Axioms

DOI10.1007/978-3-319-40970-2_27zbMath1475.68442arXiv1604.05994OpenAlexW3102833318MaRDI QIDQ2818032

Martina Seidl, Uwe Egly, Florian Lonsing

Publication date: 5 September 2016

Published in: Theory and Applications of Satisfiability Testing – SAT 2016 (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1604.05994

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Hardness Characterisations and Size-width Lower Bounds for QBF Resolution ⋮ Unnamed Item ⋮ A simple proof of QBF hardness ⋮ True crafted formula families for benchmarking quantified satisfiability solvers ⋮ Lower bound techniques for QBF expansion ⋮ Lower bounds for QCDCL via formula gauge ⋮ Q-Resolution with Generalized Axioms ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Lower bounds for QCDCL via formula gauge

Uses Software

• PicoSAT
• Quaffle
• Bloqqer
• QUBOS
• CAQE
• Quantor
• semprop
• RAReQS
• QESTO

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Solving QBF with counterexample guided refinement
• The QBF Gallery: behind the scenes
• Backdoor sets of quantified Boolean formulas
• Resolution for quantified Boolean formulas
• Expansion-based QBF solving versus Q-resolution
• Q-Resolution with Generalized Axioms
• On Unification of QBF Resolution-Based Calculi
• Clause Elimination for SAT and QSAT
• Failed Literal Detection for QBF
• QBF Resolution Systems and Their Proof Complexities
• A Unified Proof System for QBF Preprocessing
• QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving
• Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination
• Using SAT in QBF
• The relative efficiency of propositional proof systems
• Contributions to the Theory of Practical Quantified Boolean Formula Solving
• A Non-prenex, Non-clausal QBF Solver with Game-State Learning
• Blocked Clause Elimination for QBF
• Theory and Applications of Satisfiability Testing