Expansion-based QBF solving on tree decompositions

DOI10.3233/FI-2019-1810zbMATH Open1415.68111OpenAlexW2948333530MaRDI QIDQ5223208FDOQ5223208

Authors: Günther Charwat, Stefan Woltran 

Publication date: 17 July 2019

Published in: Fundamenta Informaticae (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.3233/fi-2019-1810

Recommendations

• Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations
• Theory and Applications of Satisfiability Testing
• Short proofs in QBF expansion
• On expansion and resolution in CEGAR based QBF solving
• Small resolution proofs for QBF using dependency treewidth

zbMATH Keywords

dynamic programmingtreewidthexpansionQBFQSAT

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Analysis of algorithms and problem complexity (68Q25) Dynamic programming (90C39)

Cited In (9)

• ProCount: weighted projected model counting with graded project-join trees
• Exploiting Database Management Systems and Treewidth for Counting
• Nenofex: Expanding NNF for QBF Solving
• Theory and Applications of Satisfiability Testing
• Treewidth-aware reductions of normal \textsc{ASP} to \textsc{SAT} - is normal \textsc{ASP} Harder than \textsc{SAT} after all?
• Theory and Applications of Satisfiability Testing
• Title not available (Why is that?)
• Default logic and bounded treewidth
• Using decomposition-parameters for QBF: mind the prefix!

This page was built for publication: Expansion-based QBF solving on tree decompositions

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