QELL: QBF reasoning with extended clause learning and levelized SAT solving

DOI10.1007/978-3-319-24318-4_25MaRDI QIDQ3453239zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

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

Cites work

• A non-prenex, non-clausal QBF solver with game-state learning
• A structure-preserving clause form translation
• Abstraction-based algorithm for 2QBF
• An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
• Blocked clause elimination for QBF
• Clause/Term resolution and learning in the evaluation of quantified Boolean formulas
• Logic for Programming, Artificial Intelligence, and Reasoning
• Proof complexity of resolution-based QBF calculi
• QBF Resolution Systems and Their Proof Complexities
• Recovering and utilizing partial duality in QBF
• Resolution for quantified Boolean formulas
• Solving QBF with counterexample guided refinement
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Unified QBF certification and its applications
• Using SAT in QBF

Cited in

(19)

• Q-resolution with generalized axioms
• Solving QBF with counterexample guided refinement
• scientific article; zbMATH DE number 7447736 (Why is no real title available?)
• Binary Clause Reasoning in QBF
• The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
• Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation
• 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
• Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations
• Using SAT in QBF
• Runtime vs. extracted proof size: an exponential gap for CDCL on QBFs
• ALLQBF solving by computational learning
• Learning to integrate deduction and search in reasoning about quantified Boolean formulas

Describes a project that uses

Uses Software

• RAReQS
• DepQBF
• QBFLIB
• Bloqqer
• Quaffle
• MiniSat

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)