Expansion-based QBF solving on tree decompositions

DOI10.3233/FI-2019-1810MaRDI QIDQ5223208zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

dynamic programmingexpansionQBFQSATtreewidth

Mathematics Subject Classification ID

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

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

Cited in

(12)

• Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations
• ProCount: weighted projected model counting with graded project-join trees
• Using decomposition-parameters for QBF: mind the prefix!
• Treewidth-aware reductions of normal \textsc{ASP} to \textsc{SAT} - is normal \textsc{ASP} Harder than \textsc{SAT} after all?
• Small resolution proofs for QBF using dependency treewidth
• Nenofex: Expanding NNF for QBF Solving
• Weighted model counting on the GPU by exploiting small treewidth
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Default logic and bounded treewidth
• Exploiting Database Management Systems and Treewidth for Counting
• Reducing treewidth for SAT-related problems using simple liftings

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)