Moving definition variables in quantified Boolean formulas

DOI10.1007/978-3-030-99524-9_26MaRDI QIDQ6535574zbMATH OpenFDO

Authors Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant

Publication date 23 January 2024

Copyright license Creative Commons Attribution 4.0 International

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 5719280
• Contributions to the theory of practical quantified Boolean formula solving
• Dependency learning for QBF
• Blocked clause elimination for QBF
• Dependency Learning for QBF

Cites work

• A non-prenex, non-clausal QBF solver with game-state learning
• A structure-preserving clause form translation
• A unified proof system for QBF preprocessing
• Blocked clause elimination for QBF
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• Dual proof generation for quantified Boolean formulas with a BDD-based solver
• Mining definitions in Kissat with Kittens
• Resolution for quantified Boolean formulas
• Solving QBF with counterexample guided refinement
• Strong extension-free proof systems
• Theory and Applications of Satisfiability Testing

This page was built for publication: Moving definition variables in quantified Boolean formulas

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6535574)