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

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

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

(15)

• Circuit-based search space pruning in QBF
• CirQit2
• Long-distance Q-resolution with dependency schemes
• Solving QBF with counterexample guided refinement
• Quantified maximum satisfiability
• Long distance Q-resolution with dependency schemes
• Transformations into normal forms for quantified circuits
• Antichain-Based QBF Solving
• Counterexample-Guided Model Synthesis
• Solving QBF by abstraction
• Beyond CNF: A Circuit-Based QBF Solver
• CAQE and QuAbS: Abstraction Based QBF Solvers
• Recovering and utilizing partial duality in QBF
• Solving Quantified Boolean Formulas with Circuit Observability Don’t Cares
• Quantifier shifting for quantified Boolean formulas revisited

Describes a project that uses

Uses Software

• Nenofex
• QBFLIB
• QUBE

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)