QELL: QBF reasoning with extended clause learning and levelized SAT solving
DOI10.1007/978-3-319-24318-4_25zbMATH Open1471.68263OpenAlexW2280623821MaRDI QIDQ3453239FDOQ3453239
Authors: Kuan-Hua Tu, Tzu-Chien Hsu, Jie-Hong R. Jiang 
Publication date: 20 November 2015
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-24318-4_25
Recommendations
- Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations
- Theory and Applications of Satisfiability Testing
- Contributions to the theory of practical quantified Boolean formula solving
- On expansion and resolution in CEGAR based QBF solving
- Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation
Learning and adaptive systems in artificial intelligence (68T05) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)
Cites Work
- Theory and Applications of Satisfiability Testing
- Blocked clause elimination for QBF
- A structure-preserving clause form translation
- Resolution for quantified Boolean formulas
- Unified QBF certification and its applications
- Solving QBF with counterexample guided refinement
- Proof complexity of resolution-based QBF calculi
- Abstraction-based algorithm for 2QBF
- Using SAT in QBF
- A non-prenex, non-clausal QBF solver with game-state learning
- Logic for Programming, Artificial Intelligence, and Reasoning
- QBF Resolution Systems and Their Proof Complexities
- Recovering and utilizing partial duality in QBF
- Clause/Term resolution and learning in the evaluation of quantified Boolean formulas
- An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
- Theory and Applications of Satisfiability Testing
Cited In (18)
- Solving QBF with counterexample guided refinement
- Binary Clause Reasoning in QBF
- Title not available (Why is that?)
- Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation
- The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
- Non-prenex QBF solving using abstraction
- Beyond CNF: A Circuit-Based QBF Solver
- A non-prenex, non-clausal QBF solver with game-state learning
- Contributions to the theory of practical quantified Boolean formula solving
- Message passing algorithm for solving QBF using more reasoning
- Theory and Applications of Satisfiability Testing
- Clause/Term resolution and learning in the evaluation of quantified Boolean formulas
- Theory and Applications of Satisfiability Testing
- Using SAT in QBF
- Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations
- ALLQBF solving by computational learning
- Learning to integrate deduction and search in reasoning about quantified Boolean formulas
- Q-resolution with generalized axioms
Uses Software
This page was built for publication: QELL: QBF reasoning with extended clause learning and levelized SAT solving
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3453239)
