Moving definition variables in quantified Boolean formulas

DOI10.1007/978-3-030-99524-9_26zbMATH Open1547.68713MaRDI QIDQ6535574FDOQ6535574

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

Publication date: 23 January 2024

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

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)

Cites Work

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

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)