QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving

DOI10.1007/978-3-319-24318-4_25zbMath1471.68263OpenAlexW2280623821MaRDI QIDQ3453239

Tzu-Chien Hsu, Jie-Hong R. Jiang, Kuan-Hua Tu

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)

Related Items (5)

Unnamed Item ⋮ Non-prenex QBF Solving Using Abstraction ⋮ Q-Resolution with Generalized Axioms ⋮ Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations ⋮ The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• A structure-preserving clause form translation
• An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
• Resolution for quantified Boolean formulas
• Unified QBF certification and its applications
• Solving QBF with Counterexample Guided Refinement
• Abstraction-Based Algorithm for 2QBF
• QBF Resolution Systems and Their Proof Complexities
• Using SAT in QBF
• A Non-prenex, Non-clausal QBF Solver with Game-State Learning
• Blocked Clause Elimination for QBF
• Theory and Applications of Satisfiability Testing
• Recovering and Utilizing Partial Duality in QBF
• Logic for Programming, Artificial Intelligence, and Reasoning
• Theory and Applications of Satisfiability Testing

This page was built for publication: QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving