Solving String Theories Involving Regular Membership Predicates Using SAT

String solvers gained a more prominent role in the formal analysis of string-heavy programs, causing an ever-growing need for efficient and reliable solving algorithms. Regular constraints play a central role in several real-world queries. To emerge this field, we present two approaches to encode regular constraints as a Boolean satisfiability problem, one making use of the inductive structure of regular expressions and one working on nondeterministic finite automata. We implement both approaches using WOORPJE, a recently developed purely SAT-based string solver, as a framework. An evaluation of our approaches shows that they are competitive to state-of-the-art string solvers and even outperform them in many cases.