Solving String Theories Involving Regular Membership Predicates Using SAT

DOI10.1007/978-3-031-15077-7_8MaRDI QIDQ6487302zbMATH OpenFDO

Authors Mitja Kulczynski, Kevin Lotz, Dirk Nowotka, Danny Bøgsted Poulsen

Publication date 7 December 2022

Full work available at URL https://doi.org/10.1007/978-3-031-15077-7_8

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Algorithms on strings (68W32)

Recommendations

• String theories involving regular membership predicates: from practice to theory and back
• Solving constraint satisfaction problems with SAT modulo theories
• An efficient SMT solver for string constraints
• A theory of satisfiability-preserving proofs in SAT solving
• Constraint reasoning over strings
• scientific article; zbMATH DE number 554989
• Propositional SAT solving
• Variant Satisfiability of Parameterized Strings

Cites work

• An efficient algorithm for solving word equations
• An SMT solver for regular expressions and linear arithmetic over string length
• Derivatives of Regular Expressions
• Finite automata and unary languages
• scientific article; zbMATH DE number 1223734 (Why is no real title available?)
• scientific article; zbMATH DE number 1798184 (Why is no real title available?)
• scientific article; zbMATH DE number 3062907 (Why is no real title available?)
• On solving word equations using SAT
• Periodic sets of integers
• String theories involving regular membership predicates: from practice to theory and back
• The expressibility of languages and relations by word equations

Cited in

(9)

• String theories involving regular membership predicates: from practice to theory and back
• Towards more efficient methods for solving regular-expression heavy string constraints
• A decision procedure for regular membership and length constraints over unbounded strings
• Symbolic automata constraint solving
• An efficient SMT solver for string constraints
• Unbounded model-checking with interpolation for regular language constraints
• Verified verifying: SMT-LIB for strings in Isabelle
• Solving string constraints using SAT
• Certainty in formalising SMT-LIB for strings in Isabelle

This page was built for publication: Solving String Theories Involving Regular Membership Predicates Using SAT

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