Scaling up DPLL(T) string solvers using context-dependent simplification

DOI10.1007/978-3-319-63390-9_24MaRDI QIDQ2164248zbMATH OpenOpenAlexFDO

Authors Andrew Reynolds, Maverick Woo, Clark Barrett, David Brumley, Tianyi Liang, Cesare Tinelli

Publication date 12 August 2022

Full work available at URL https://doi.org/10.1007/978-3-319-63390-9_24

Mathematics Subject Classification ID

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

Recommendations

• An efficient SMT solver for string constraints
• Even Faster Conflicts and Lazier Reductions for String Solvers
• DPLL: the core of modern satisfiability solvers
• On the complexity of choosing the branching literal in DPLL
• Parameterized complexity of DPLL search procedures
• Parameterized Complexity of DPLL Search Procedures
• Principles and Practice of Constraint Programming – CP 2004

Cited in

(16)

• A symbolic algorithm for the case-split rule in string constraint solving
• A decision procedure for string to code point conversion
• Subsumption demodulation in first-order theorem proving
• Flexible proof production in an industrial-strength SMT solver
• Reasoning about vectors using an SMT theory of sequences
• Chain-free string constraints
• Progressive reasoning over recursively-defined strings
• scientific article; zbMATH DE number 7559472 (Why is no real title available?)
• An efficient SMT solver for string constraints
• Z3str2: an efficient solver for strings, regular expressions, and length constraints
• Reasoning about vectors: satisfiability modulo a theory of sequences
• High-level abstractions for simplifying extended string constraints in SMT
• Word equations in synergy with regular constraints
• Even Faster Conflicts and Lazier Reductions for String Solvers
• Word equations in synergy with regular constraints (extended version)
• Negated string containment is decidable

This page was built for publication: Scaling up DPLL(T) string solvers using context-dependent simplification

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