Exploiting circuit representations in QBF solving

DOI10.1007/978-3-642-14186-7_29MaRDI QIDQ4930601zbMATH OpenOpenAlexFDO

Authors Alexandra Goultiaeva, Fahiem Bacchus

Publication date 29 September 2010

Published in Theory and Applications of Satisfiability Testing – SAT 2010 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-14186-7_29

Mathematics Subject Classification ID

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

Recommendations

• Beyond CNF: A Circuit-Based QBF Solver
• Circuit-based search space pruning in QBF
• Solving Quantified Boolean Formulas with Circuit Observability Don’t Cares
• Formal Methods in Computer-Aided Design
• Principles and Practice of Constraint Programming – CP 2004

Cited in

(14)

• Long distance Q-resolution with dependency schemes
• Solving QBF with counterexample guided refinement
• Quantified maximum satisfiability
• scientific article; zbMATH DE number 7447736 (Why is no real title available?)
• Circuit-based search space pruning in QBF
• Beyond CNF: A Circuit-Based QBF Solver
• Antichain-Based QBF Solving
• Recovering and utilizing partial duality in QBF
• CirQit2
• Solving Quantified Boolean Formulas with Circuit Observability Don’t Cares
• CAQE and QuAbS: Abstraction Based QBF Solvers
• Transformations into normal forms for quantified circuits
• Long-distance Q-resolution with dependency schemes
• Counterexample-Guided Model Synthesis

Describes a project that uses

Uses Software

• QUBE
• QBFLIB
• Nenofex

This page was built for publication: Exploiting circuit representations in QBF solving

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