Incremental search for conflict and unit instances of quantified formulas with E-matching

DOI10.1007/978-3-030-67067-2_24zbMath1472.68184OpenAlexW3118899654MaRDI QIDQ2234102

Jochen Hoenicke, Tanja I. Schindler

Publication date: 18 October 2021

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

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items

Incremental search for conflict and unit instances of quantified formulas with E-matching

Cites Work

• Unnamed Item
• Solving quantified linear arithmetic by counterexample-guided instantiation
• Incremental search for conflict and unit instances of quantified formulas with E-matching
• Revisiting enumerative instantiation
• Congruence Closure with Free Variables
• Solving SAT and SAT Modulo Theories
• Engineering DPLL(T) + Saturation
• Simplify: a theorem prover for program checking
• Efficient E-Matching for SMT Solvers
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Fast Decision Procedures Based on Congruence Closure
• Verification, Model Checking, and Abstract Interpretation