Interpolation-based semantic gate extraction and its applications to QBF preprocessing

DOI10.1007/978-3-030-53288-8_24MaRDI QIDQ2225124zbMATH OpenOpenAlexFDO

Authors Friedrich Slivovsky

Publication date 4 February 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-53288-8_24

Mathematics Subject Classification ID

Logic in computer science (03B70) Interpolation, preservation, definability (03C40) Computational aspects of satisfiability (68R07) Pattern recognition, speech recognition (68T10) Switching theory, applications of Boolean algebras to circuits and networks (94C11)

Recommendations

• Solution validation and extraction for QBF preprocessing
• Preprocessing for DQBF
• On QBF Proofs and Preprocessing
• Blocked clause elimination for QBF
• Enhancing search-based QBF solving by dynamic blocked clause elimination

Cited in

(7)

• Certified DQBF solving by definition extraction
• DQBDD: an efficient BDD-based DQBF solver
• Mining definitions in Kissat with Kittens
• Tractable representations for Boolean functional synthesis
• Hierarchical stochastic SAT and quality assessment of logic locking
• Clausal congruence closure
• Certifying phase abstraction

This page was built for publication: Interpolation-based semantic gate extraction and its applications to QBF preprocessing

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