GhostQ. System description

DOI10.3233/SAT190117MaRDI QIDQ5015604zbMATH OpenFDO

Authors William Klieber

Publication date 9 December 2021

Published in Journal on Satisfiability, Boolean Modeling and Computation (Search for Journal in Brave)

zbMATH Keywords

QBFDPLLnon-clausalPlaisted-Greenbaum encoding

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Circuit-based search space pruning in QBF
• A non-prenex, non-clausal QBF solver with game-state learning
• Formal Methods in Computer-Aided Design
• Theory and Applications of Satisfiability Testing
• DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL

Cites work

• scientific article; zbMATH DE number 3313427 (Why is no real title available?)
• A non-prenex, non-clausal QBF solver with game-state learning
• Recovering and utilizing partial duality in QBF
• Solving QBF with counterexample guided refinement
• Solving QBF with counterexample guided refinement

Cited in

(2)

• GhostQ
• Dual proof generation for quantified Boolean formulas with a BDD-based solver

This page was built for publication: GhostQ. System description

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