GhostQ. System description

DOI10.3233/SAT190117zbMATH Open1484.68221MaRDI QIDQ5015604FDOQ5015604

Authors: William Klieber 

Publication date: 9 December 2021

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

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

zbMATH Keywords

QBFDPLLnon-clausalPlaisted-Greenbaum encoding

Mathematics Subject Classification ID

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

Cites Work

• Solving QBF with counterexample guided refinement
• Solving QBF with counterexample guided refinement
• A non-prenex, non-clausal QBF solver with game-state learning
• Title not available (Why is that?)
• Recovering and utilizing partial duality in QBF

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)